The Compcert verified compiler

FORTAINE Guillaume gui.fortaine at
Sun Mar 16 18:02:05 PDT 2008

Misses, Misters,

I would greatly appreciate to have your comments on this research 
project, if possible, please :

The CompCert project investigates the formal verification of realistic 
compilers usable for critical embedded software. Such verified compilers 
come with a mathematical, machine-checked proof that the generated 
executable code behaves exactly as prescribed by the semantics of the 
source program. By ruling out the possibility of compiler-introduced 
bugs, verified compilers strengthen the guarantees that can be obtained 
by applying formal methods to source programs.

I look forward to your answer,

Best Regards,


More information about the TUNES mailing list