Skip to Main content Skip to Navigation
Conference papers

Certification of a chain for deductive program verification

Paolo Herms 1, 2, 3, * 
* Corresponding author
1 PROVAL - Proof of Programs
UP11 - Université Paris-Sud - Paris 11, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR
Abstract : Frama-C1 is an extensible platform dedicated to source-code analysis of C software. It is organised with a plug-in architecture based on a common kernel and the common formal annotation language ACSL (ANSI/ISO C Specication Language)[1], able to express a wide range of functional properties of the C code. The Jessie plug-in aims to formally prove such ACSL properties. Based on the Why platform designed for program verication[3], it transforms annotated C programs into equivalent programs in the Why intermediate language. The Why tool then processes a Hoare-style weakest-precondition (WP) calculus obtaining a set of verication conditions (VCs). The validation of these generated VCs deductively implies the correctness of the C program with respect to its annotations. The purpose of this work is to formalise and certify this chain in the Coq Proof Assistant. At the end, we want to obtain a formalisation of a suciently large subset of C with ACSL to interface with Compcert's C-light[2], a formalisation of the Why language and its WP calculus and a certied compilation from the former to the latter.
Document type :
Conference papers
Complete list of metadata
Contributor : Claude Marché Connect in order to contact the contributor
Submitted on : Friday, November 12, 2010 - 10:53:08 AM
Last modification on : Sunday, June 26, 2022 - 11:52:35 AM


  • HAL Id : inria-00535640, version 1



Paolo Herms. Certification of a chain for deductive program verification. 2nd Coq Workshop, satellite of ITP'10, Jul 2010, Edinburgh, United Kingdom. ⟨inria-00535640⟩



Record views