CompCert
CompCert 3.14
El compilador C verificado formalmente.
El compilador verificado de CompCert C es un compilador para un subconjunto grande del lenguaje de programación C que genera código para los procesadores PowerPC, ARM, X86 y RISC-V.
La característica distintiva de CompCert es que se ha verificado formalmente utilizando el Asistente de prueba de CoQ: el código de ensamblaje generado está garantizado formalmente que se comporte según lo prescrito por la semántica del código C.
Para obtener más información sobre CompCert (plataformas compatibles, características de C compatibles, instrucciones de instalación, utilizando el compilador, etc.), consulte el sitio web y especialmente el manual del usuario.
CompCert no es un software gratuito. Esta liberación no comercial solo se puede utilizar para evaluación, investigación, fines educativos y personales. Se puede comprar una versión comercial de CompCert, sin esta restricción y con soporte profesional y características adicionales, de ABSINT. Consulte la LICENSE de archivo para obtener más información.
El compilador verificado de CompCert es el Instituto de Copyright National De Recherche en Informatique et Automatique (INRIA) y ABSINT Angewandte Informatik GmbH.
Las discusiones generales sobre CompCert tienen lugar en la lista de correo de CompCert- [email protected].
Para consultas sobre la versión comercial de CompCert, comuníquese con [email protected]
