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.