Formal verification of a realistic compiler

Xavier Leroy
[doi] [Google Scholar] [DBLP] [Citeseer]

Communications of the ACM 52(7)
Pages 107-115
2009
Note(s): translation validation, Coq theorem prover, CompCert compiler, verified compilers

Notes related to Formal verification of a realistic compiler