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.


References in zbMATH (referenced in 23 articles , 2 standard articles )

Showing results 1 to 20 of 23.
Sorted by year (citations)

1 2 next

  1. Boldo, Sylvie; Jourdan, Jacques-Henri; Leroy, Xavier; Melquiond, Guillaume: Verified compilation of floating-point computations (2015)
  2. Stewart, Gordon; Beringer, Lennart; Cuellar, Santiago; Appel, Andrew W.: Compositional CompCert (2015)
  3. Théry, Laurent (ed.); Wiedijk, Freek (ed.): Foreword to the special focus on formal proofs for mathematics and computer science (2015)
  4. Appel, Andrew W.; Dockins, Robert; Hobor, Aquinas; Beringer, Lennart; Dodds, Josiah; Stewart, Gordon; Blazy, Sandrine; Leroy, Xavier: Program logics for certified compilers (2014)
  5. 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)
  6. Krebbers, Robbert: An operational and axiomatic semantics for non-determinism and sequence points in C (2014)
  7. Krebbers, Robbert; Leroy, Xavier; Wiedijk, Freek: Formal C semantics: CompCert and the C standard (2014)
  8. Gonthier, Georges; Ziliani, Beta; Nanevski, Aleksandar; Dreyer, Derek: How to make ad hoc proof automation less ad hoc (2013)
  9. Hirschowitz, Tom: Full abstraction for fair testing in CCS (2013)
  10. Krebbers, Robbert; Wiedijk, Freek: Separation logic for non-local control flow and block scope variables (2013)
  11. Monin, Jean-François; Shi, Xiaomu: Handcrafted inversions made operational on operational semantics (2013)
  12. Ševčík, Jaroslav; Vafeiadis, Viktor; Zappa Nardelli, Francesco; Jagannathan, Suresh; Sewell, Peter: CompCertTSO: a verified compiler for relaxed-memory concurrency (2013)
  13. Campbell, Brian: An executable semantics for compcert C (2012)
  14. Carlier, Matthieu; Dubois, Catherine; Gotlieb, Arnaud: A first step in the design of a formally verified constraint-based testing tool: FocalTest (2012)
  15. Leroy, Xavier: Mechanized semantics for compiler verification (2012)
  16. Miculan, Marino; Paviotti, Marco: Synthesis of distributed mobile programs using monadic types in Coq (2012)
  17. Strub, Pierre-Yves; Swamy, Nikhil; Fournet, Cedric; Chen, Juan: Self-certification: bootstrapping certified typecheckers in F$^\ast$ with Coq (2012)
  18. Ridge, Tom: Simple, functional, sound and complete parsing for all context-free grammars (2011)
  19. Koprowski, Adam; Binsztok, Henri: TRX: a formally verified parser interpreter (2010)
  20. Sutcliffe, Geoff; Benzmüller, Christoph: Automated reasoning in higher-order logic using the TPTP THF infrastructure (2010)

1 2 next


Further publications can be found at: http://compcert.inria.fr/publi.html