CompCert is a project to create officially verified compilers. Within the framework of the project, the CompCert C compiler was developed for the C language (ISO C90 / ANSI C standards with some minor restrictions and individual extensions, inspired by the subsequent standards), and the Coq verification system was completely written and demonstrated. The main developer is Xavier Leroy . This compiler has a machine check that the generated code behaves the same as the source code. The compiler allows you to generate machine code for PowerPC , ARM, and x86 processor architectures .
| Compcert | |
|---|---|
| Type of | Compiler |
| Author | Xavier Leroy , INRIA |
| Written on | Caml , Coq |
| First edition | April 3, 2008 |
| Hardware platform | Cross-platform software |
| Latest version | 2.7.1 (June 2016) |
| License | free for non-commercial use [1] ; commercial licenses from AbsInt |
| Website | compcert.inria.fr |
Content
- 1 Motivation
- 2 Implementation
- 3 See also
- 4 notes
- 5 Links
Motivation
Since compilers are very complex software, they often suffer from a large number of bugs [2] . For example, they cannot generate code corresponding to the source code. These bugs can lead to very serious consequences in critical areas. Thus, the goal of CompCert is to create a formally verified compiler with mathematical guarantees.
Implementation
The code generated by CompCert is about twice as fast as the code generated by GCC without optimization and slightly slower than the code generated with higher levels of optimization. [3]
See also
- Formal verification
- Formal methods