Counterexamples from Proof Failures in SPARK

David Hauzar 1, 2 Claude Marché 1, 2 Yannick Moy 3
2 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 : A major issue in the activity of deductive program verification is the understanding of the reason why a proof fails. To help the user understand the problem and decide what needs to be fixed in the code or the specification, it is essential to provide means to investigate such a failure. We present our approach for the design and the implementation of counterexample generation within the SPARK 2014 environment, exhibiting values for the variables of the program where a given part of the specification fails to be validated. To produce a counterexample , we exploit the ability of SMT solvers to propose, when a proof of a formula is not found, a counter-model. Turning such a counter-model into a counterexample for the initial program is not trivial because of the many transformations leading from a given code and specification to a verification condition.
Type de document :
Communication dans un congrès
Software Engineering and Formal Methods, Jul 2016, Vienna, Austria. Springer, 2016, Software Engineering and Formal Methods
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01314885
Contributeur : Claude Marché <>
Soumis le : jeudi 12 mai 2016 - 12:08:30
Dernière modification le : vendredi 17 février 2017 - 16:10:48
Document(s) archivé(s) le : mercredi 16 novembre 2016 - 02:17:02

Fichier

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

Identifiants

  • HAL Id : hal-01314885, version 1

Citation

David Hauzar, Claude Marché, Yannick Moy. Counterexamples from Proof Failures in SPARK. Software Engineering and Formal Methods, Jul 2016, Vienna, Austria. Springer, 2016, Software Engineering and Formal Methods. 〈hal-01314885〉

Partager

Métriques

Consultations de
la notice

301

Téléchargements du document

152