2014 · 97 citations · 21 references
ComputingComputer EngineeringComputer ScienceCompilersComputer ArchitectureProgramming LanguagesAbstract Syntax TreesCode GenerationCompiler ConstructionControl-flow AnalysisRegister AllocationCompilation UnitsCompiler DesignFramesInvariantsLinkingSeparate CompilationSimulation RelationsVerified Compilation
This paper reports on the development of Compositional CompCert, the first verified separate compiler for C.
21
Formal verification of a realistic compiler
Xavier Leroy · Communications of the ACM · 2009 · 1.1K citations
Jaroslav Ševčík, Viktor Vafeiadis, Francesco Zappa Nardelli et al. · Journal of the ACM · 2013 · 174 citations
Biorthogonality, step-indexing and compiler correctness
Nick Benton, Chung-Kil Hur · 2009 · 120 citations
A verified compiler for an impure functional language
Adam Chlipala · 2010 · 101 citations