A Formally Verified Compiler Back-end

By Xavier Leroy. Journal of automated reasoning, 2009

653 citations recorded by the source corpus.

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.

Subfields: Artificial Intelligence, Computational Theory and Mathematics

View Paper: https://www.semanticscholar.org/paper/cf38e244e4f6ff4f31ab46f002fb2869e215ca15

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Artificial Intelligence

In Computational Theory and Mathematics

Citations in the corpus

Formal verification of a realistic compiler (2009, background): “A detailed description of Clight can be found in [5]; of the compiler front-end in [4]; and of the compiler back-end in [11, 13].”
Compiler validation via equivalence modulo inputs (2014, methodology): “Compiler Testing The most directly related is compiler testing, which remains the dominant technique for validating production compilers in practice.”
Using Crash Hoare logic for certifying the FSCQ file system (2015, methodology): “Our first approach, influenced by CompCert [46], organized the system as a number of abstraction layers (such as blocks, inodes, directories, and pathnames), each with its own domain-specific language.”