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.68063Besson, Frédéric; Blazy, Sandrine; Wilke, Pierre 2017 Compositional CompCert. Zbl 1346.68056Stewart, 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 all top 5 Cited in 12 Serials 6 Journal of Automated Reasoning 2 Journal of Functional Programming 1 Programming and Computer Software 1 Information and Computation 1 Formal Aspects of Computing 1 Formal Methods in System Design 1 Journal of the ACM 1 Lecture Notes in Computer Science 1 Mathematics in Computer Science 1 Logical Methods in Computer Science 1 Journal of Formalized Reasoning 1 Journal of Membrane Computing Cited in 4 Fields 50 Computer science (68-XX) 8 Mathematical logic and foundations (03-XX) 2 General and overarching topics; collections (00-XX) 1 Numerical analysis (65-XX) Citations by Year