Xavier Leroy. Mechanized semantics for compiler verification. In APLAS 2012: Programming Languages and Systems, 10th Asian Symposium, number 7705 in LNCS, pages 386--388, Kyoto, Japan, December 2012. Springer.

The formal verification of compilers and related programming tools depends crucially on the availability of appropriate mechanized semantics for the source, intermediate and target languages. In this invited talk, I review various forms of operational semantics and their mechanization, based on my experience with the formal verification of the CompCert C compiler.

bib | DOI | Local copy | At publisher's site ] Back

This file was generated by bibtex2html 1.99.