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 soundness. 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. © 2009 Springer Science+Business Media B.V.
CITATION STYLE
Leroy, X. (2009). A formally verified compiler back-end. Journal of Automated Reasoning, 43(4), 363–446. https://doi.org/10.1007/s10817-009-9155-4
Mendeley helps you to discover research relevant for your work.