The CompCert compiler has been awarded from the prestigious Association for computing machinery (ACM), for the second time
CompCert is the first multi-architecture optimising compiler used in industry with a mathematical proof of correctness verified by computer.
Developed by several researchers*, including Sandrine Blazy, Professor at the Université de Rennes, Deputy Director of IRISA and member of the Epicure research team, this compiler was awarded the ACM Software System Award (june 2022) and the ACM SIGPLAN Programming Languages Software Award (january 2023).
"CompCert is a fully verified compiler for C that is actually usable on real source code and that produces decent target code on real-world architectures. It seeded a new age of formal verification by dispelling the myth that formal methods could only be done on toy programs in the lab. As a shared artifact it has enabled the software systems verification community to work together, in the same way that GCC or LLVM has done in earlier generations, putting real-world C programs on a solid formal foundation. It currently targets PowerPC, ARM, RISC-V, and x86, supporting all of ISO C99 except unstructured switch statements, longjmp, and variable-length array types. CompCert is today available under commercial and noncommercial open-source licenses, and used in the real world for security-critical control software for emergency power generators and for flight control and navigation algorithms, by companies including Airbus France. It remains an important shared infrastructure for ongoing research."ACM SIGPLAN Programming Languages Software Award
Sandrine Blazy, Professeure à l’Université de Rennes et directrice adjointe de l’IRISA et ses collègues collègues Xavier Leroy, Collège de France; Zaynah Dargaye, Nomadic Labs; Jacques-Henri Jourdan, CNRS, Laboratoire Méthodes Formelles; Michael Schmidt, AbsInt Angewandte Informatik; Bernhard Schommer, Saarland University, and AbsInt Angewandte Informatik GmbH; and Jean-Baptiste Tristan, Boston College