Certification of a chain for deductive program verification - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2010

Certification of a chain for deductive program verification

Résumé

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.
Fichier non déposé

Dates et versions

inria-00535640 , version 1 (12-11-2010)

Identifiants

  • HAL Id : inria-00535640 , version 1

Citer

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

Partager

Gmail Facebook X LinkedIn More