Certification of a chain for deductive program verification

International audienceFrama-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