Formal Verification of an SSA-based Middle-end for CompCert

Gilles Barthe 1 Delphine Demange 2 David Pichardie 2
2 CELTIQUE - Software certification with semantic analysis
Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL
Abstract : CompCert is a formally verified compiler that generates compact and efficient code for a large subset of the C language. However, CompCert foregoes using SSA, an intermediate representation employed by many compilers that enables writing simpler, faster optimizers. In fact, it has remained an open problem to verify formally an SSA-based compiler. We report on a formally verified, SSA-based middle-end for CompCert. In addition to providing a formally verified SSA-based middle-end, we address two problems raised by Leroy in [2009]: giving an intuitive formal semantics to SSA, and leveraging its global properties to reason locally about program optimizations.
Type de document :
Article dans une revue
ACM Transactions on Programming Languages and Systems (TOPLAS), ACM, 2014, 36 (1), pp.35. 〈10.1145/2579080〉
Liste complète des métadonnées

https://hal.inria.fr/hal-01097677
Contributeur : Delphine Demange <>
Soumis le : samedi 20 décembre 2014 - 21:48:03
Dernière modification le : mercredi 16 mai 2018 - 11:23:28

Lien texte intégral

Identifiants

Citation

Gilles Barthe, Delphine Demange, David Pichardie. Formal Verification of an SSA-based Middle-end for CompCert. ACM Transactions on Programming Languages and Systems (TOPLAS), ACM, 2014, 36 (1), pp.35. 〈10.1145/2579080〉. 〈hal-01097677〉

Partager

Métriques

Consultations de la notice

800