Counterexamples from proof failures in the SPARK program verifier

David Hauzar 1, 2 Claude Marché 1, 2 Yannick Moy 3
1 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
Résumé : Un défi important de l’activité de vérification déductive de programmes est la compréhension de la raison pour laquelle une certaine preuve échoue. Pour aider l’utilisateur à comprendre le problème et à décider quoi modifier dans son code ou bien sa spécification, il est essentiel de fournir des moyens d’analyser l’échec de preuve. À cette fin, nous proposons une technique de génération de contre-exemples, qui exhibent des valeurs pour les variables du programme pour lesquelles une certaine partie de la spécification ne peut pas être prouvée. Pour produire un tel contre-exemple, nous exploitons la capacité des solveurs SMT (Satisfiability Modulo Theories) de proposer, quand une formule n’est pas prouvée, un contre-modèle. Transformer un tel contre-modèle en un contre-exemple pour le programme de départ n’est pas une tâche facile à cause des multiples transformations qui conduisent du code et de la spécification de départ vers une obligation de preuve. Nous présentons l’approche que nous avons suivie pour la conception et l’implémentation de la génération de contre-exemples dans le cadre de l’environnement SPARK 2014 pour le développement de programmes Ada critiques
Type de document :
Rapport
[Research Report] RR-8854, Inria. 2016, pp.22
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01271174
Contributeur : Claude Marché <>
Soumis le : lundi 8 février 2016 - 18:51:59
Dernière modification le : vendredi 17 février 2017 - 16:10:49
Document(s) archivé(s) le : samedi 12 novembre 2016 - 14:15:07

Fichier

RR-8854.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01271174, version 1

Citation

David Hauzar, Claude Marché, Yannick Moy. Counterexamples from proof failures in the SPARK program verifier. [Research Report] RR-8854, Inria. 2016, pp.22. 〈hal-01271174〉

Partager

Métriques

Consultations de
la notice

247

Téléchargements du document

252