3c4bfcc3d7
The CompCert C verified compiler is a compiler for a large subset of the C programming language that generates code for the PowerPC, ARM and x86 processors. The distinguishing feature of CompCert is that it has been formally verified using the Coq proof assistant: the generated assembly code is formally guaranteed to behave as prescribed by the semantics of the source C code. CompCert is not free software. This non-commercial release can only be used for evaluation, research, educational and personal purposes.
15 lines
681 B
Plaintext
15 lines
681 B
Plaintext
The CompCert C verified compiler is a compiler for a large subset
|
|
of the C programming language that generates code for the PowerPC,
|
|
ARM and x86 processors.
|
|
|
|
The distinguishing feature of CompCert is that it has been formally
|
|
verified using the Coq proof assistant: the generated assembly code
|
|
is formally guaranteed to behave as prescribed by the semantics of
|
|
the source C code.
|
|
|
|
CompCert is not free software. This non-commercial release can only
|
|
be used for evaluation, research, educational and personal purposes.
|
|
A commercial version of CompCert, without this restriction and with
|
|
professional support, can be purchased from AbsInt. See the file
|
|
LICENSE for more information.
|