Skip to Main content Skip to Navigation
Conference papers

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 metadata

Cited literature [16 references]  Display  Hide  Download
Contributor : Xavier Leroy Connect in order to contact the contributor
Submitted on : Friday, October 31, 2014 - 11:06:17 PM
Last modification on : Friday, January 21, 2022 - 3:19:23 AM
Long-term archiving on: : Monday, February 2, 2015 - 4:52:28 PM


Files produced by the author(s)




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⟩



Les métriques sont temporairement indisponibles