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, Yves Bertot, 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 commercial licenses and technical support for CompCert, and participates in its development and evolution.

Grants

The CompCert project has been supported by the following grants:

Related projects