CompCert
CompCert is a formally verified optimizing compiler for a large subset of the C99 programming language which currently targets PowerPC, ARM and 32-bit x86 architectures. This project, led by Xavier Leroy, started officially in 2005, funded by the French institutes ANR and INRIA. The compiler is specified, programmed and proved in Coq. It aims to be used for programming embedded systems requiring reliability. The performance of its generated code is often close to that of GCC (version 3) at optimization level -O1, and always better than that of GCC without optimizations.
CompCert
CompCert is a formally verified optimizing compiler for a large subset of the C99 programming language which currently targets PowerPC, ARM and 32-bit x86 architectures. This project, led by Xavier Leroy, started officially in 2005, funded by the French institutes ANR and INRIA. The compiler is specified, programmed and proved in Coq. It aims to be used for programming embedded systems requiring reliability. The performance of its generated code is often close to that of GCC (version 3) at optimization level -O1, and always better than that of GCC without optimizations.
has abstract
CompCert est un projet dont l' ...... rocesseur PowerPC, ARM et x86.
@fr
CompCert is a formally verifi ...... o the advancement of the tool.
@en
genre
latest release version
Link from a Wikipage to an external page
Wikipage page ID
27,309,180
Wikipage revision ID
740,476,217
latest release date
license
free for noncommercial use
comment
CompCert est un projet dont l' ...... rocesseur PowerPC, ARM et x86.
@fr
CompCert is a formally verifi ...... of GCC without optimizations.
@en
label
CompCert
@en
CompCert
@fr
wasDerivedFrom
homepage
isPrimaryTopicOf
name
CompCert
@en