Certification of a chain for deductive program verification

Paolo Herms 1, 2, 3, *
* Auteur correspondant
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.
Type de document :
Communication dans un congrès
Yves Bertot. 2nd Coq Workshop, satellite of ITP'10, Jul 2010, Edinburgh, United Kingdom. 2010
Liste complète des métadonnées

https://hal.inria.fr/inria-00535640
Contributeur : Claude Marché <>
Soumis le : vendredi 12 novembre 2010 - 10:53:08
Dernière modification le : jeudi 5 avril 2018 - 12:30:08

Identifiants

  • HAL Id : inria-00535640, version 1

Collections

Citation

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

Partager

Métriques

Consultations de la notice

132