The Compcert verified compiler

[FORTAINE Guillaume]

Misses, Misters,

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

http://compcert.inria.fr/

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,

GF