A formally verified compiler back-end

Xavier Leroy 1, 2, *
Abstract : This article describes the development and formal verification (proof of semantic preservation) of a compiler back-end from Cminor (a simple imperative intermediate language) to PowerPC assembly code, using the Coq proof assistant both for programming the compiler and for proving its correctness. Such a verified compiler is useful in the context of formal methods applied to the certification of critical software: the verification of the compiler guarantees that the safety properties proved on the source code hold for the executable compiled code as well.
Complete list of metadatas

Cited literature [92 references]  Display  Hide  Download

https://hal.inria.fr/inria-00360768
Contributor : Xavier Leroy <>
Submitted on : Saturday, November 14, 2009 - 9:50:59 AM
Last modification on : Friday, May 25, 2018 - 12:02:07 PM
Long-term archiving on : Thursday, September 23, 2010 - 5:45:04 PM

Files

paper2.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

Xavier Leroy. A formally verified compiler back-end. Journal of Automated Reasoning, Springer Verlag, 2009, 43 (4), pp.363-446. ⟨10.1007/s10817-009-9155-4⟩. ⟨inria-00360768v3⟩

Share

Metrics

Record views

601

Files downloads

482