CompCert
CompCert 3.14
Le compilateur C officiellement vérifié.
Le compilateur COMPCERT C Vérifié est un compilateur pour un grand sous-ensemble du langage de programmation C qui génère du code pour les processeurs PowerPC, ARM, X86 et RISC-V.
La caractéristique distinctive de CompCert est qu'elle a été officiellement vérifiée à l'aide de l'assistant d'épreuve CoQ: le code d'assemblage généré est officiellement garanti pour se comporter comme prescrit par la sémantique du code C source.
Pour plus d'informations sur CompCert (plates-formes prises en charge, fonctionnalités C prise en charge, instructions d'installation, en utilisant le compilateur, etc.), veuillez vous référer au site Web et en particulier au manuel de l'utilisateur.
CompCert n'est pas un logiciel libre. Cette version non commerciale ne peut être utilisée que pour l'évaluation, la recherche, les fins éducatives et personnelles. Une version commerciale de CompCert, sans cette restriction et avec un support professionnel et des fonctionnalités supplémentaires, peut être achetée auprès de l'absint. Voir la LICENSE de fichier pour plus d'informations.
Le compilateur vérifié CompCert est le Copyright Institut National de Recherche en informatique et l'automatique (INRIA) et l'absitrement Angewandte Informatik GmbH.
Les discussions générales sur CompCert ont lieu sur la liste de diffusion [email protected].
Pour des demandes de renseignements sur la version commerciale de CompCert, veuillez contacter [email protected]
