Room 206 (2nd floor, badged access)
24 March 2022 - 14h00
The trusted computing base of the CompCert verified compiler
by David Monniaux from VERIMAG
Abstract: (ESOP 2022 talk)
CompCert is the first realistic formally verified compiler: it provides a machine-checked mathematical proof that the code it generates matches the source code.
But what do these impressive claims mean exactly?
We comprehensively analyze aspects of CompCert where errors could lead to incorrect code being generated.
Possible issues range from the modeling of the source and the target languages to some techniques used to call external algorithms from within the compiler.
