Section: Application Domains

Formal methods

We develop techniques and tools for the formal verification of critical software:

• program logics based on CFML and Iris for the deductive verification of software, including concurrency and algorithmic complexity aspects;

• verified development tools such as the CompCert verified C compiler, which extends properties established by formal verification at the source level all the way to the final executable code.

Some of these techniques have already been used in the nuclear industry (MTU Friedrichshafen uses CompCert to develop emergency diesel generators) and are under evaluation in the aerospace industry.