Can you trust your compiler? — With CompCert, you can!
The decision on the right embedded compiler for the development of safety-critical software can have a significant influence on the effort and success of a product development.
To avoid unpleasant surprises, the correctness of the code generation should be validated by using compiler bug lists.
A much higher degree of confidence in the correctness of the compiler than a normal compiler validation offers a formal, mathematically strict proof that the generated code is free from miscompilation errors. It ensures that the generated code is proven to have the same semantics as the source code fed into the compiler.
The effort of monitoring compiler bug lists can be eliminated, and duplicate testing effort between host and target can be avoided.
In this webinar, you'll learn how formal verified compilation combined with test automation can reduce the time and effort required to achieve compliance with industry regulations such as ISO 26262.
Agenda:
Terminology: compiler validation vs. compiler verification
Introduction to formal compiler verification
Benefits of formally verified compilation
Experimental evaluation of CompCert performance
Tool qualification strategy
