Xavier Leroy. Mechanized semantics for compiler verification. In Ranjit Jhala and Atsushi Igarashi, editors, Programming Languages and Systems, 10th Asian Symposium, APLAS 2012, volume 7705 of Lecture Notes in Computer Science, pages 386-388. Springer, 2012. Abstract of invited talk.

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 | Local copy | At publisher's ] Back

This file was generated by bibtex2html 1.97.