Binary Heaps Formally Verified in Why3

Asma Tafat 1 Claude Marché 1, 2
2 PROVAL - Proof of Programs
UP11 - Université Paris-Sud - Paris 11, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR
Résumé : Les benchmarks VACID-0 forment une collection de petits programmes qui posent des défis pour la vérification formelle de leur comportement fonctionnel. Ce rapport présente la vérification formelle de l'un de ces exemples: les tas binaires. La solution présentée utilise l'environnement pour la vérification Why3. Le comportement attendu est spécifié dans la logique de Why3, de façon structurée grâce aux constructions hiérarchiques de théories proposées par Why3. Les preuves sont effectuées de façon largement automatiques, car les prouveurs SMT disponibles en sortie de Why3 résolvent un pourcentage significatif des obligations de preuves engendrées, le reste étant prouvé interactivement avec l'assistant de preuve Coq. La motivation de cette étude de cas est de démontrer l'utilisabilité et l'efficacité à la fois du langage de spécification de Why3 et des outils associés, qui fournissent un langage puissant de spécification tout en permettant une automatisation importante des preuves.
Type de document :
Rapport
[Research Report] RR-7780, INRIA. 2011, pp.33
Liste complète des métadonnées

https://hal.inria.fr/inria-00636083
Contributeur : Claude Marché <>
Soumis le : mercredi 26 octobre 2011 - 16:33:18
Dernière modification le : jeudi 9 février 2017 - 15:58:27
Document(s) archivé(s) le : jeudi 15 novembre 2012 - 10:36:03

Fichier

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

Identifiants

  • HAL Id : inria-00636083, version 1

Citation

Asma Tafat, Claude Marché. Binary Heaps Formally Verified in Why3. [Research Report] RR-7780, INRIA. 2011, pp.33. <inria-00636083>

Partager

Métriques

Consultations de
la notice

733

Téléchargements du document

441