CompCert

CompCert es un compilador optimizador formalmente verificado para un gran subconjunto de un dialecto del lenguaje de programación C , llamado C99 y conocido como Clight. A partir de 2018CompCert admite las arquitecturas de procesador ARM , PowerPC , RISC-V , x86 y x86-64 . ^{[ 3 ] [ 4 ]} El proyecto, liderado por Xavier Leroy , comenzó oficialmente en 2005, financiado por los institutos franceses Agence nationale de la recherche (ANR) y French Institute for Research in Computer Science and Automation (INRIA). El compilador se especifica, programa y prueba en el software asistente de pruebas llamado Rocq . CompCert se utiliza para programar sistemas embebidos que requieren fiabilidad . El rendimiento de su código generado suele ser similar al de GNU Compiler Collection (GCC) versión 3, con nivel de optimización -O1, y siempre superior al de GCC sin optimizaciones. ^{[ 5 ]}

Desde 2015, AbsInt ofrece licencias comerciales, ^{[ 6 ]} proporciona soporte y mantenimiento, y contribuye al avance de la herramienta. CompCert se publica bajo una licencia no comercial y, por lo tanto, no es software libre , aunque algunos de sus archivos fuente tienen una licencia dual con la Licencia Pública General Reducida de GNU versión 2.1 o posterior, o están disponibles bajo los términos de otras licencias. ^{[ 2 ]}

Por el desarrollo de CompCert, el primer compilador optimizador prácticamente útil que apunta a múltiples arquitecturas comerciales y que cuenta con una prueba completa y verificada mecánicamente de su corrección, Xavier Leroy y el equipo de desarrollo de CompCert recibieron el premio ACM Software System Award 2021 .

• Sitio web oficial
• CompCert en GitHub
• Verificación formal de un compilador realista
• Premio al Sistema de Software — Premios ACM