Un compilateur mathématiquement sans erreur
Développé par des équipes de plusieurs organismes de recherche français, CompCert est un compilateur de code en langage C, destiné notamment aux logiciels critiques des avions et de l’industrie nucléaire, qui certifie une compilation sans erreur. […]