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 37 articles , 3 standard articles )
Showing results 1 to 20 of 37.
Sorted by year (- Besson, Frédéric; Blazy, Sandrine; Wilke, Pierre: A verified CompCert front-end for a memory model supporting pointer arithmetic and uninitialised data (2019)
- Bouillaguet, Quentin; Bobot, François; Sighireanu, Mihaela; Yakobowski, Boris: Exploiting pointer analysis in memory models for deductive verification (2019)
- Kiam Tan, Yong; Myreen, Magnus O.; Kumar, Ramana; Fox, Anthony; Owens, Scott; Norrish, Michael: The verified CakeML compiler backend (2019)
- Alex A. Alemi, Francois Chollet, Niklas Een, Geoffrey Irving, Christian Szegedy, Josef Urban: DeepMath - Deep Sequence Models for Premise Selection (2018) arXiv
- Chen, Hao; Wu, Xiongnan; Shao, Zhong; Lockerman, Joshua; Gu, Ronghui: Toward compositional verification of interruptible OS kernels and device drivers (2018)
- Kumar, Ramana; Mullen, Eric; Tatlock, Zachary; Myreen, Magnus O.: Software verification with ITPs should use binary code extraction to reduce the TCB (short paper) (2018)
- Zhao, Jinxu; Oliveira, Bruno C. d. S.; Schrijvers, Tom: Formalization of a polymorphic subtyping algorithm (2018)
- 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)
- Krebbers, Robbert: A formal C memory model for separation logic (2016)
- Boldo, Sylvie; Jourdan, Jacques-Henri; Leroy, Xavier; Melquiond, Guillaume: Verified compilation of floating-point computations (2015)
- Chatzikyriakidis, Stergios; Luo, Zhaohui: Individuation criteria, dot-types and copredication: a view from modern type theories (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)
- Besson, Frédéric; Blazy, Sandrine; Wilke, Pierre: A precise and abstract memory model for C using symbolic values (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) ioport
- Gonthier, Georges; Ziliani, Beta; Nanevski, Aleksandar; Dreyer, Derek: How to make ad hoc proof automation less ad hoc (2013)
Further publications can be found at: http://compcert.inria.fr/publi.html