Mechanized Semantics for Compiler Verification - Archive ouverte HAL Access content directly
Conference Papers Year : 2012

Mechanized Semantics for Compiler Verification

(1)
1

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.
Fichier principal
Vignette du fichier
mechanized-semantics-aplas-cpp-2012.pdf (122.29 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

hal-01079337 , version 1 (31-10-2014)

Identifiers

Cite

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⟩

Collections

INRIA INRIA2 ANR
105 View
119 Download

Altmetric

Share

Gmail Facebook Twitter LinkedIn More