HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
Conference papers

Formal Verification of a C Compiler Front-end

Abstract : This paper presents the formal verification of a compiler front-end that translates a subset of the C language into the Cminor intermediate language. The semantics of the source and target languages as well as the translation between them have been written in the specification language of the Coq proof assistant. The proof of observational semantic equivalence between the source and generated code has been machine-checked using Coq. An executable compiler was obtained by automatic extraction of executable Caml code from the Coq specification of the translator, combined with a certified compiler back-end generating PowerPC assembly code from Cminor, described in previous work.
Document type :
Conference papers
Complete list of metadata

Cited literature [12 references]  Display  Hide  Download

Contributor : Sandrine Blazy Connect in order to contact the contributor
Submitted on : Monday, October 16, 2006 - 10:14:34 AM
Last modification on : Monday, February 21, 2022 - 3:38:08 PM
Long-term archiving on: : Thursday, September 20, 2012 - 11:55:18 AM




Sandrine Blazy, Zaynah Dargaye, Xavier Leroy. Formal Verification of a C Compiler Front-end. FM'06: 14th Symposium on Formal Methods, Aug 2006, Hamilton, Canada. pp.460-475, ⟨10.1007/11813040_31⟩. ⟨inria-00106401⟩



Record views


Files downloads