CompCert
CompCert 3.14
O compilador C formalmente verificado.
O compilador verificado da Compcert C é um compilador para um grande subconjunto da linguagem de programação C que gera código para os processadores PowerPC, ARM, X86 e RISC-V.
O recurso distintivo do Compcert é que ele foi formalmente verificado usando o Assistente de Prova de Coq: o código de montagem gerado é formalmente garantido para se comportar conforme prescrito pela semântica do código C.
Para obter mais informações sobre o Compcert (plataformas suportadas, recursos C suportados, instruções de instalação, usando o compilador etc.), consulte o site e, especialmente, o manual do usuário.
Compcert não é um software livre. Essa liberação não comercial só pode ser usada para avaliação, pesquisa, fins educacionais e pessoais. Uma versão comercial do Compcert, sem essa restrição e com suporte profissional e recursos extras, pode ser adquirida da ABSINT. Consulte a LICENSE do arquivo para obter mais informações.
O compilador verificado da Compcert é o Institut National de Recherche em Informatique et en Automatique (INRIA) e o ABSINT ANGEWANDTE ENFORMATIK GmbH.
As discussões gerais sobre o Compcert ocorrem na lista de discussão [email protected].
Para obter perguntas sobre a versão comercial do Compcert, entre em contato com [email protected]
