For inquiries about Compcert, please contact the project leader or the industrial partner AbsInt.
Authors
Xavier Leroy is the architect and lead developer of the CompCert C verified compiler. The other developers are Sandrine Blazy, Zaynah Dargaye, Jacques-Henri Jourdan, Michael Schmidt, Bernhard Schommer, and Jean-Baptiste Tristan.
The following scientists contributed ideas, code, or feedback: Andrew Appel, Ricardo Bedin França, Lennart Beringer, Frédéric Besson, Sylvie Boldo, Timothy Bourke, Yves Bertot, Christoph Cullmann, Rob Dockins, Damien Doligez, Denis Favre-Felix, Benjamin Grégoire, Robbert Krebbers, Guillaume Melquiond, Thomas Moniot, Prashanth Mundkur, Alexandre Pilkiewicz, Tahina Ramananandro, Laurence Rideau, Silvain Rideau, Benoît Robillard, Valentin Robert, Gordon Stewart, Bernard Paul Serpette, Jean Souyris, Joseph Tassarotti, Andrew Tolmach.
Industrial partner
AbsInt Angewandte Informatik GmbH sells an industrial-strength version of CompCert with more features, technical support, and unlimited licensing. AbsInt participates in the development and evolution of CompCert.
Grants
The CompCert project has been supported by the following grants:
- ANR CompCert (grant number ANR-05-SSIA-0019), 2005-2008. Participants: INRIA Paris-Rocquencourt, team Gallium (coordinator); INRIA Sophia-Antipolis, team Marelle; CEDRIC, a laboratory of CNAM and ENSIIE; PPS, a laboratory of CNRS and University Paris Diderot).
- ANR U3CAT (grant number ANR--08-SEGI-021), 2009-2012, coordinated by Virgile Prevosto at CEA LIST.
- FNRAE ASCERT, 2009-2011, coordinated by David Pichardie at IRISA, team Celtique.
- Digiteo Hisseo, 2008-2011, coordinated by Pascal Cuoq at CEA LIST.
- BGLE CEEC, 2012-2015, coordinated by Prove & Run.
- ANR Verasco (grant number ANR-11-INSE-003), 2012-2016, coordinated by Xavier Leroy at INRIA Paris-Rocquencourt, team Gallium.
- ITEA3 ASSUME, 2015-2018, coordinated by Udo Gleich and Wolfgang Köpf at Daimler AG, Germany.
Related projects
- Velus, by Timothy Bourke and others at Inria Paris.
- DeepSpec: the science of deep specification, led by Andrew Appel at Princeton University.
- Verified Software Toolchain, led by Andrew Appel at Princeton University.
- Formal verification of runtime system components, led by Andrew Tolmach at Portland State University.
- CompCert TSO at Cambridge University.