Skip to Main content Skip to Navigation
New interface
Reports (Research report)

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)
Complete list of metadata

Cited literature [25 references]  Display  Hide  Download
Contributor : Claude Marché Connect in order to contact the contributor
Submitted on : Thursday, November 10, 2011 - 12:51:42 PM
Last modification on : Friday, October 28, 2022 - 3:28:39 AM
Long-term archiving on: : Thursday, November 15, 2012 - 11:40:56 AM


Files produced by the author(s)


  • HAL Id : hal-00639977, version 1


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



Record views


Files downloads