CompCert est un compilateur C, formellement vérifié. Il est destiné à la compilation de logiciels sécuritaires critiques ou les missions sensibles, nécessitant un haut niveau de confiance.
CompCert est le seul compilateur celui-ci est certifié être sans erreurs de compilation. Toutes les propriétés de sécurité verifiées sur le code source (par exemple avec Astrée) sont garantis aussi pour le code binaire généré.
CompCert prend en charge la majorité du langage ISO C99, avec quelques exceptions et extensions spécifiques. Il génère du code machine pour les architectures PowerPC, x86, ARM, AArch64, AURIX et RISC-V.
Références clients :
Pour de plus amples informations, veuillez voir la page anglaise ou bien contactez nos distributeurs officiels :
- en France : ISIT, Plaisance du Touch, contact@isit.fr, 05 61 30 69 00
- au Canada : Joral Technologies, Kemptville, ON, robert.campbell@joraltechnologies.com, 613–215–3252
- au Benelux : Indes, Culemborg, Pays-Bas, sales@indes.com, +31 (0)3 45 54 55 35