CompCert
projet pour la réalisation de compilateurs vérifiés formellement
From Wikipedia, the free encyclopedia
CompCert est un projet dont l'objectif est la réalisation de compilateurs certifiés formellement. Ce projet développe essentiellement un compilateur, CompCert C, pour le langage C (ISO C99 avec quelques limitations mineures et plusieurs extensions inspirées de la norme ISO C2011[2]) entièrement écrit et prouvé avec le logiciel Rocq.
Cet article est une ébauche concernant l’informatique.
| Développé par | Xavier Leroy, Sandrine Blazy, INRIA |
|---|---|
| Fichier exécutable | ccomp |
| Première version | |
| Dernière version | 3.17 ()[1] |
| Dépôt | https://github.com/AbsInt/CompCert |
| Écrit en | OCaml, Rocq |
| Environnement | Multiplate-forme |
| Type | Compilateur |
| Licence | INRIA Non-Commercial License Agreement |
| Site web | compcert.org/compcert-C.html |
Le développeur principal est Xavier Leroy. Sandrine Blazy, Zaynah Dargaye, Jacques-Henri Jourdan, Michael Schmidt, Bernhard Schommer, et Jean-Baptiste Tristan participent activement en tant que développeurs à ce projet.
Ce compilateur possède une preuve vérifiée par machine que le code généré se comporte de la même manière que le code source. Il permet de générer du code machine pour les architectures de processeur PowerPC, ARM, RISC-V, x86 et x86-64.
Motivation
Les compilateurs étant des logiciels très complexes, ils souffrent souvent de très nombreux bugs[3]. Par exemple, ils peuvent générer du code ne correspondant pas au code source. Ces bugs peuvent mener à des conséquences graves dans les domaines critiques. Par conséquent, l'objectif de CompCert est de produire un compilateur formellement vérifié avec une garantie mathématique de sa correction.
Performances
Récompenses
CompCert a été récompensé par l'Association for computing machinery avec le Prix ACM Software System en 2021 notamment[5].
