Mechanized Semantics for Compiler Verification

Xavier Leroy 1, *
* Auteur correspondant
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.
Type de document :
Communication dans un congrès
APLAS 2012 - 10th Asian Symposium on Programming Languages and Systems, Dec 2012, Kyoto, Japan. 7705, pp.386-388, 2012, Lecture Notes in Computer Science. <10.1007/978-3-642-35182-2_27>
Liste complète des métadonnées


https://hal.inria.fr/hal-01079337
Contributeur : Xavier Leroy <>
Soumis le : vendredi 31 octobre 2014 - 23:06:17
Dernière modification le : lundi 5 octobre 2015 - 17:00:49
Document(s) archivé(s) le : lundi 2 février 2015 - 16:52:28

Fichier

mechanized-semantics-aplas-cpp...
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Xavier Leroy. Mechanized Semantics for Compiler Verification. APLAS 2012 - 10th Asian Symposium on Programming Languages and Systems, Dec 2012, Kyoto, Japan. 7705, pp.386-388, 2012, Lecture Notes in Computer Science. <10.1007/978-3-642-35182-2_27>. <hal-01079337>

Partager

Métriques

Consultations de
la notice

95

Téléchargements du document

76