Formal certification of a compiler back-end or: programming a compiler with a proof assistant

By Xavier Leroy. ACM-SIGACT Symposium on Principles of Programming Languages, 2006

847 citations recorded by the source corpus.

Subfields: Artificial Intelligence, Computational Theory and Mathematics

View Paper: https://www.semanticscholar.org/paper/3369e43abcb499eea4d208f2239df00551b8d2dd

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

seL4: Formal Veriﬁcation of an OS Kernel (2009, methodology): “Leroy veriﬁed an optimising C compiler [44] for the PowerPC architecture.”
A FORMAL PROOF OF THE KEPLER CONJECTURE (2015, neutral): “The Flyspeck project has roughly similar size and complexity as other major formalization projects such as the Feit–Thompson odd order theorem [9], the CompCert project giving a verified C compiler [31], and the seL4 project that verified an operating system microkernel [28].”
Formal certification of code-based cryptographic proofs (2009, methodology): “The correctness of optim is proved using a mixture of the techniques of [10] and [11, 26]: we express the validity of th e information contained in the analysis domain using a predic ate Valid(δ, m) that states the agreement between the compile time abstract values inδ and the runtime memory m.”
A Formally Verified Compiler Back-end (2009, methodology): “In practice, careful decomposition of the proofs in separate lemmas enabled us to reuse large parts of the development even in the face of major changes in the semantics, such as switching from the “mixed-step” semantics described in [57] to the small-step transition semantics described in this pape”
Comprehensive formal verification of an OS microkernel (2014, methodology): “To reach a guarantee, some comparison would have to be done between the semantics of the C code in the Coq CompCert and Isabelle/HOL models.”
seL4: formal verification of an OS kernel (2009, methodology): “Leroy verified an optimising C compiler [44] for the PowerPC architecture.”
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.”
The New C Standard (Excerpted material) An Economic and Cultural Commentary (2008, neutral): “Researchers continue to increase the size of the language subsets for which translators have been proved correct.[ 7 , 9, 11] They have also looked at proving some of the components of an existing translator, gcc, correct.[8]”
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].”