A Certified Multi-prover Verification Condition Generator

Paolo Herms 1, 2, 3 Claude Marché 1, 2 Benjamin Monate 3
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 outils de vérification de programme basés sur la preuve ont atteint un nouveau de maturité permettant leur utilisation dans un contexte industriel où un haut niveau de confiance est requis. Cela soulève la question du niveau de confiance que l'on peut mettre dans les outils eux-mêmes. Nous décrivons une implémentation certifiée d'un générateur d'obligations de preuve. Une originalité est sa généricité vis-à-vis du contexte logique, permettant de générer des obligations pour une grande famille de prouveurs. Cette implémentation est réalisée avec l'assistant à la preuve Coq, et est conçue dans l'optique d'en extraire un exécutable indépendant de Coq, garantit correct, ce qui est un autre originalité.
Type de document :
Rapport
[Research Report] RR-7793, INRIA. 2011, pp.22
Liste complète des métadonnées

https://hal.inria.fr/hal-00639977
Contributeur : Claude Marché <>
Soumis le : jeudi 10 novembre 2011 - 12:51:42
Dernière modification le : jeudi 9 février 2017 - 15:56:49
Document(s) archivé(s) le : jeudi 15 novembre 2012 - 11:40:56

Fichier

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

Identifiants

  • HAL Id : hal-00639977, version 1

Collections

Citation

Paolo Herms, Claude Marché, Benjamin Monate. A Certified Multi-prover Verification Condition Generator. [Research Report] RR-7793, INRIA. 2011, pp.22. <hal-00639977>

Partager

Métriques

Consultations de
la notice

304

Téléchargements du document

196