×

CompCert

swMATH ID: 9737
Software Authors: Leroy, X.
Description: 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.
Homepage: http://compcert.inria.fr/
Related Software: Coq; Isabelle/HOL; z3; CakeML; cminor; Isabelle; HOL Light; OCaml; HOL; CompCertTSO; Automath; Haskell; seL4; GitHub; Flyspeck; ACL2; Mizar; PVS; Toolchain; VCC
Cited in: 51 Publications
Further Publications: http://compcert.inria.fr/publi.html

Standard Articles

3 Publications describing the Software, including 2 Publications in zbMATH Year
CompCertS: a memory-aware verified C compiler using pointer as integer semantics. Zbl 1468.68063
Besson, Frédéric; Blazy, Sandrine; Wilke, Pierre
2017
Compositional CompCert. Zbl 1346.68056
Stewart, Gordon; Beringer, Lennart; Cuellar, Santiago; Appel, Andrew W.
2015
Formal C semantics: CompCert and the C standard
Krebbers, Robbert; Leroy, Xavier; Wiedijk, Freek
2014
all top 5

Cited by 126 Authors

4 Krebbers, Robbert
4 Leroy, Xavier
3 Appel, Andrew W.
3 Blazy, Sandrine
2 Beringer, Lennart
2 Besson, Frédéric
2 Dodds, Josiah
2 Kumar, Ramana
2 McCreight, Andrew
2 Monin, Jean-François
2 Myreen, Magnus O.
2 Stewart, Gordon
2 Wiedijk, Freek
2 Wilke, Pierre
1 Ariola, Zena M.
1 Bell, Christian J.
1 Benzmüller, Christoph Ewald
1 Binsztok, Henri
1 Bobot, François
1 Bodin, Martin
1 Boldo, Sylvie
1 Bouillaguet, Quentin
1 Bowen, Jonathan P.
1 Carlier, Matthieu
1 Chakravarty, Manuel M. T.
1 Charguéraud, Arthur
1 Chatzikyriakidis, Stergios
1 Chen, Hao
1 Chen, Juan
1 Chevalier, Tim
1 Coughlin, Nicholas
1 Cuellar, Santiago
1 Czajka, Łukasz
1 Das, Ankush
1 Dockins, Robert
1 Dong, JinSong
1 Downen, Paul
1 Dragomir, Iulia
1 Dreyer, Derek R.
1 Dubois, Catherine
1 Farka, František
1 Filaretti, Daniele
1 Fournet, Cédric
1 Fox, Anthony C. J.
1 Gamboa, Ruben A.
1 Gardner, Philippa Anne
1 Gonthier, Georges
1 Gotlieb, Arnaud
1 Grall, Hervé
1 Gu, Ronghui
1 Hayes, Ian J.
1 He, Jifeng
1 Hirschowitz, Tom
1 Hoa, Koh Chuen
1 Hobor, Aquinas
1 Hoffmann, Jan-Philipp
1 Hou, Zhe
1 Jagannathan, Suresh
1 Jourdan, Jacques-Henri
1 Keller, Gabriele Cornelia
1 Klein, Gerwin
1 Koprowski, Adam
1 Krijnen, Jacco O. G.
1 Larchey-Wendling, Dominique
1 Li, Pengfei
1 Liu, Yang
1 Liu, Yezhou
1 Lockerman, Joshua
1 Luo, Zhaohui
1 Maffeis, Sergio
1 Melquiond, Guillaume
1 Miculan, Marino
1 Mullen, Eric
1 Murray, Toby
1 Mutilin, V. S.
1 Nakata, Keiko
1 Namjoshi, Kedar S.
1 Nanevski, Aleksandar
1 Naudziuniene, Daiva
1 Nicolescu, Radu
1 Norrish, Michael
1 Oliveira, Bruno C.d. S.
1 Owens, Scott
1 Paviotti, Marco
1 Preoteasa, Viorel
1 Ridge, Thomas
1 Sanán, David
1 Schmitt, Alan
1 Schrijvers, Tom
1 Ševčík, Jaroslav
1 Sewell, Peter
1 Shao, Zhong
1 Sheng, Feng
1 Shi, Xiaomu
1 Sighireanu, Mihaela
1 Smith, Gareth David
1 Strub, Pierre-Yves
1 Sun, Jing
1 Sutcliffe, Geoff
1 Swamy, Nikhil
...and 26 more Authors

Citations by Year