Static versus Dynamic Verification in Why3, Frama-C and SPARK 2014

Nikolai Kosmatov 1 Claude Marché 2, 3 Yannick Moy 4 Julien Signoles 1
1 LSL - Laboratoire Sûreté des Logiciels
LIST - Laboratoire d'Intégration des Systèmes et des Technologies : DRT/LIST
3 TOCCATA - Certified Programs, Certified Tools, Certified Floating-Point Computations
LRI - Laboratoire de Recherche en Informatique, UP11 - Université Paris-Sud - Paris 11, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR8623
Abstract : Why3 is an environment for static verification, generic in the sense that it is used as an intermediate tool by different front-ends for the verification of Java, C or Ada programs. Yet, the choices made when designing the specification languages provided by those front-ends differ significantly, in particular with respect to the executability of specifications. We review these differences and the issues that result from these choices. We emphasize the specific feature of ghost code which turns out to be extremely useful for both static and dynamic verification. We also present techniques, combining static and dynamic features, that help users understand why static verification fails.
Type de document :
Communication dans un congrès
7th International Symposium on Leveraging Applications, Oct 2016, Corfu, Greece. Springer, pp.16, 2016, 7th International Symposium on Leveraging Applications
Liste complète des métadonnées

Littérature citée [43 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01344110
Contributeur : Claude Marché <>
Soumis le : lundi 11 juillet 2016 - 13:14:55
Dernière modification le : vendredi 17 février 2017 - 16:10:37

Fichier

paper063.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01344110, version 1

Citation

Nikolai Kosmatov, Claude Marché, Yannick Moy, Julien Signoles. Static versus Dynamic Verification in Why3, Frama-C and SPARK 2014. 7th International Symposium on Leveraging Applications, Oct 2016, Corfu, Greece. Springer, pp.16, 2016, 7th International Symposium on Leveraging Applications. 〈hal-01344110〉

Partager

Métriques

Consultations de
la notice

644

Téléchargements du document

439