L’éditeur d’outre-Rhin AbsInt, spécialiste des technologies d’analyse et de vérification de code pour applications critiques dont les produits sont distribués en France par Nexeya Services, propose en version de test ...le compilateur CompCert, un compilateur C optimisé (ISO C 99 avec quelques extensions et restrictions) et surtout vérifié de manière formelle par des méthodes mathématiques. Objectif : assurer la conformité du processus de compilation avec un niveau de confiance très élevé pour des applications embarquées dont le logiciel doit être qualifié selon un très haut niveau d’assurance qualité. En d'autres termes, le code produit par le compilateur doit se comporter exactement comme spécifié par la sémantique du programme source C, et ce sans ambiguïté, grâce à un moteur de preuve formelle.

Rappelons que CompCert est un projet d’origine française piloté par l’Inria sous la houlette de Xavier Leroy dont l'objectif est la réalisation de compilateurs certifiés formellement. Essentiellement, ce projet développe le compilateur CompCert C, écrit et prouvé avec le logiciel open source Coq. Egalement développé par des équipes françaises, ce dernier permet de manipuler des assertions de calcul, de vérifier des preuves de ces assertions, d’aider à la recherche de preuves formelles et de synthétiser des programmes certifiés à partir de preuves constructives de leurs spécifications. Le compilateur CompCert permet notamment de générer du code machine pour les architectures PowerPC, ARM et x86.