• From Mechanized Semantics to V...

Treffer: From Mechanized Semantics to Verified Compilation: the Clight Semantics of CompCert

Title:
From Mechanized Semantics to Verified Compilation: the Clight Semantics of CompCert
Authors:
Blazy, Sandrine
Contributors:
Analyse sémantique et compilation pour la sécurité des environnements d'exécution (EPICURE), Inria Rennes – Bretagne Atlantique, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-LANGAGE ET GÉNIE LOGICIEL (IRISA-D4), Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA), Université de Rennes (UR)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-IMT Atlantique (IMT Atlantique), Institut Mines-Télécom Paris (IMT)-Institut Mines-Télécom Paris (IMT)-Université de Rennes (UR)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut Mines-Télécom Paris (IMT)-Institut Mines-Télécom Paris (IMT)-Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-IMT Atlantique (IMT Atlantique), Institut Mines-Télécom Paris (IMT)-Institut Mines-Télécom Paris (IMT)
Source:
Lecture Notes in Computer Science ; FASE 2024 - 27th International Conference on Fundamental Approaches to Software Engineering ; https://inria.hal.science/hal-04553834 ; FASE 2024 - 27th International Conference on Fundamental Approaches to Software Engineering, Apr 2024, Luxembourg, Luxembourg. pp.1-21, ⟨10.1007/978-3-031-57259-3_1⟩
Publisher Information:
HAL CCSD
Springer Nature Switzerland
Publication Year:
2024
Collection:
Université de Rennes 1: Publications scientifiques (HAL)
Subject Terms:
operational semantics of programming languages, verified compilation, machine-checked proofs, [INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL]
Subject Geographic:
Luxembourg
Document Type:
Konferenz conference object
Language:
English
DOI:
10.1007/978-3-031-57259-3_1
Availability:
https://inria.hal.science/hal-04553834
https://inria.hal.science/hal-04553834/document
https://inria.hal.science/hal-04553834/file/paper.pdf
https://doi.org/10.1007/978-3-031-57259-3_1
Rights:
http://creativecommons.org/licenses/by/ ; info:eu-repo/semantics/OpenAccess
Accession Number:
edsbas.A3C4F981
Database:
BASE

Weitere Informationen

International audience ; CompCert is a formally verified compiler for C that is specified, programmed and proved correct with the Coq proof assistant. CompCert was used in industry to compile critical embedded software. Its correctness proof states that the compiler does not introduce bugs. This semantic preservation property involves the formal semantics of the source and target languages of the compiler. Reasoning on C semantics to prove compiler correctness is challenging, as C is a real language that was not designed with semantics in mind. This paper presents the operational style that was designed for the C semantics of CompCert in order to facilitate the mechanized reasoning on terminating and diverging programs, and details the semantics of the Clight source language of CompCert.