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 certification of a compiler back-end, or: programming a compiler with a proof assistant

Abstract : This paper reports on the development and formal certification (proof of semantic preservation) of a compiler from Cminor (a C-like imperative language) to PowerPC assembly code, using the Coq proof assistant both for programming the compiler and for proving its correctness. Such a certified compiler is useful in the context of formal methods applied to the certification of critical software: the certification of the compiler guarantees that the safety properties proved on the source code hold for the executable compiled code as well.
Complete list of metadata

Cited literature [34 references]  Display  Hide  Download

https://hal.inria.fr/inria-00000963
Contributor : Xavier Leroy Connect in order to contact the contributor
Submitted on : Friday, January 6, 2006 - 10:02:21 AM
Last modification on : Friday, February 4, 2022 - 3:07:27 AM
Long-term archiving on: : Friday, September 14, 2012 - 4:50:42 PM

Identifiers

Collections

Citation

Xavier Leroy. Formal certification of a compiler back-end, or: programming a compiler with a proof assistant. 33rd Symposium Principles of Programming Languages (POPL 2006), Jan 2006, Charleston, SC, United States. pp.42--54, ⟨10.1145/1111037.1111042⟩. ⟨inria-00000963⟩

Share

Metrics

Record views

239

Files downloads

748