CompCert
The CompCert project investigates the formal verification of realistic compilers usable for critical embedded software. Such verified compilers come with a mathematical, machine-checked proof that the generated executable code behaves exactly as prescribed by the semantics of the source program. By ruling out the possibility of compiler-introduced bugs, verified compilers strengthen the guarantees that can be obtained by applying formal methods to source programs. The main result of the project is the CompCert C verified compiler, a high-assurance compiler for almost all of the ISO C90 / ANSI C language, generating efficient code for the PowerPC, ARM and x86 processors.
Keywords for this software
References in zbMATH (referenced in 28 articles , 3 standard articles )
Showing results 1 to 20 of 28.
Sorted by year (- Besson, Frédéric; Blazy, Sandrine; Wilke, Pierre: Compcerts: a memory-aware verified C compiler using pointer as integer semantics (2017)
- Hoffmann, Jan; Das, Ankush; Weng, Shu-Chun: Towards automatic resource bound analysis for OCaml (2017)
- Leroy, Xavier: Formally verifying a compiler: what does it mean, exactly? (invited talk) (2016)
- Boldo, Sylvie; Jourdan, Jacques-Henri; Leroy, Xavier; Melquiond, Guillaume: Verified compilation of floating-point computations (2015)
- Stewart, Gordon; Beringer, Lennart; Cuellar, Santiago; Appel, Andrew W.: Compositional CompCert (2015)
- Théry, Laurent (ed.); Wiedijk, Freek (ed.): Foreword to the special focus on formal proofs for mathematics and computer science (2015)
- Appel, Andrew W.; Dockins, Robert; Hobor, Aquinas; Beringer, Lennart; Dodds, Josiah; Stewart, Gordon; Blazy, Sandrine; Leroy, Xavier: Program logics for certified compilers (2014)
- Klein, Gerwin (ed.); Gamboa, Ruben (ed.): Interactive theorem proving. 5th international conference, ITP 2014, held as part of the Vienna summer of logic, VSL 2014, Vienna, Austria, July 14--17, 2014. Proceedings (2014)
- Krebbers, Robbert: An operational and axiomatic semantics for non-determinism and sequence points in C (2014)
- Krebbers, Robbert; Leroy, Xavier; Wiedijk, Freek: Formal C semantics: CompCert and the C standard (2014)
- Gonthier, Georges; Ziliani, Beta; Nanevski, Aleksandar; Dreyer, Derek: How to make ad hoc proof automation less ad hoc (2013)
- Hirschowitz, Tom: Full abstraction for fair testing in CCS (2013)
- Krebbers, Robbert; Wiedijk, Freek: Separation logic for non-local control flow and block scope variables (2013)
- Monin, Jean-François; Shi, Xiaomu: Handcrafted inversions made operational on operational semantics (2013)
- Ševčík, Jaroslav; Vafeiadis, Viktor; Zappa Nardelli, Francesco; Jagannathan, Suresh; Sewell, Peter: CompCertTSO: a verified compiler for relaxed-memory concurrency (2013)
- Campbell, Brian: An executable semantics for compcert C (2012)
- Carlier, Matthieu; Dubois, Catherine; Gotlieb, Arnaud: A first step in the design of a formally verified constraint-based testing tool: FocalTest (2012)
- Leroy, Xavier: Mechanized semantics for compiler verification (2012)
- Miculan, Marino; Paviotti, Marco: Synthesis of distributed mobile programs using monadic types in Coq (2012)
- Strub, Pierre-Yves; Swamy, Nikhil; Fournet, Cedric; Chen, Juan: Self-certification: bootstrapping certified typecheckers in F$^\ast$ with Coq (2012)
Further publications can be found at: http://compcert.inria.fr/publi.html