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
Abstract : Deduction-based software verification tools have reached a maturity allowing them to be used in industrial context where a very high level of assurance is required. This raises the question of the level of confidence we can grant to the tools themselves. We present a certified implementation of a verification condition generator. An originality is its genericity with respect to the logical context, which allows us to produce proof obligations for a large class of theorem provers. This implementation is conducted within the Coq proof assistant, and is crafted so that it can be extracted into a standalone executable, independent of Coq, which is another originality.
Document type :
Reports
[Research Report] RR-7793, INRIA. 2011, pp.22
Liste complète des métadonnées


https://hal.inria.fr/hal-00639977
Contributor : Claude Marché <>
Submitted on : Thursday, November 10, 2011 - 12:51:42 PM
Last modification on : Thursday, February 9, 2017 - 3:56:49 PM
Document(s) archivé(s) le : Thursday, November 15, 2012 - 11:40:56 AM

File

RR-7793.pdf
Files produced by the author(s)

Identifiers

  • 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>

Share

Metrics

Record views

352

Document downloads

204