- Are you developing a safety-critical application?
- Do you have to certify according to DO178B/C or IEC 60880?
- Do you disable compiler optimizations for safety reasons, running into resource problems as a result?
- Do you wish to reduce your testing effort at the executable object level?
If your answer to any of these is “yes”, the CompCert compiler might be of interest to you.
What is CompCert?
CompCert is the only production compiler that is formally verified, using machine-assisted mathematical proofs, to be free of miscompilation issues. The code it produces is proved to behave exactly as specified by the semantics of the original source C program.
The code optimizations are formally verified as well. You can now significantly improve your application’s performance, as you no longer have to switch off optimizations for safety reasons.
The testing effort at the binary-executable level can be reduced, as any safety properties verified on the source code automatically hold for the generated executable.
In November 2017, CompCert was successfully qualified according to IEC 60880, category A, and IEC 61508-3:2010, SCL 3 for a certification project in the nuclear energy domain.
If you have any questions before trying a demo or would like to schedule an ONLINE tool demonstration, please let us know.
1-877-380-3366 Ext 101. 613-851-2155