Mechanized Semantics for Compiler Verification

Xavier Leroy 1, *
* Corresponding author
Abstract : 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.
Document type :
Conference papers
Complete list of metadatas

Cited literature [16 references]  Display  Hide  Download

https://hal.inria.fr/hal-01079337
Contributor : Xavier Leroy <>
Submitted on : Friday, October 31, 2014 - 11:06:17 PM
Last modification on : Friday, May 25, 2018 - 12:02:07 PM
Long-term archiving on : Monday, February 2, 2015 - 4:52:28 PM

File

mechanized-semantics-aplas-cpp...
Files produced by the author(s)

Identifiers

Collections

Citation

Xavier Leroy. Mechanized Semantics for Compiler Verification. APLAS 2012 - 10th Asian Symposium on Programming Languages and Systems, Dec 2012, Kyoto, Japan. pp.386-388, ⟨10.1007/978-3-642-35182-2_27⟩. ⟨hal-01079337⟩

Share

Metrics

Record views

178

Files downloads

158