CompCert

The formally-verified C compiler.

Overview

The CompCert C verified compiler is a compiler for a large subset of theC programming language that generates code for the PowerPC, ARM, x86 andRISC-V processors.

The distinguishing feature of CompCert is that it has been formallyverified using the Coq proof assistant: the generated assembly code isformally guaranteed to behave as prescribed by the semantics of thesource C code.

For more information on CompCert (supported platforms, supported Cfeatures, installation instructions, using the compiler, etc), pleaserefer to the Web site and especiallythe user's manual.

License

CompCert is not free software. This non-commercial release can onlybe used for evaluation, research, educational and personal purposes.A commercial version of CompCert, without this restriction and withprofessional support and extra features, can be purchased fromAbsInt. See the file LICENSE for moreinformation.

Copyright

The CompCert verified compiler is Copyright Institut National deRecherche en Informatique et en Automatique (INRIA) andAbsInt Angewandte Informatik GmbH.

Contact

General discussions on CompCert take place on thecompcert-users@inria.frmailing list.

For inquiries on the commercial version of CompCert, please contactinfo@absint.com