A structured approach to proving compiler optimizations based on dataflow analysis

Yves Bertot 1 Benjamin Grégoire 2 Xavier Leroy 3
1 MARELLE - Mathematical, Reasoning and Software
CRISAM - Inria Sophia Antipolis - Méditerranée
2 EVEREST - Environments for Verification and Security of Software
CRISAM - Inria Sophia Antipolis - Méditerranée
3 GALLIUM - Programming languages, types, compilation and proofs
Inria Paris-Rocquencourt
Abstract : This paper reports on the correctness proof of compiler optimizations based on data-flow analysis. We formulate the optimizations and analyses as instances of a general framework for data-flow analyses and transformations, and prove that the optimizations preserve the behavior of the compiled programs. This development is a part of a larger effort of certifying an optimizing compiler by proving semantic equivalence between source and compiled code.
Type de document :
Communication dans un congrès
Types for Proofs and Programs, Workshop TYPES 2004, Dec 2004, Jouy-en-Josas, France. Springer, 3839, pp.66-81, 2006, Lecture Notes in Computer Science. 〈10.1007/11617990〉
Liste complète des métadonnées

Littérature citée [7 références]  Voir  Masquer  Télécharger
https://hal.inria.fr/inria-00289549
Contributeur : Xavier Leroy <>
Soumis le : samedi 21 juin 2008 - 13:58:12
Dernière modification le : mercredi 12 septembre 2018 - 01:16:38
Document(s) archivé(s) le : vendredi 28 septembre 2012 - 16:26:05

Fichier

proofs_dataflow_optimizations....
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

INRIA | INRIA-ROCQ

Citation

Yves Bertot, Benjamin Grégoire, Xavier Leroy. A structured approach to proving compiler optimizations based on dataflow analysis. Types for Proofs and Programs, Workshop TYPES 2004, Dec 2004, Jouy-en-Josas, France. Springer, 3839, pp.66-81, 2006, Lecture Notes in Computer Science. 〈10.1007/11617990〉. 〈inria-00289549〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

340

Téléchargements de fichiers

159

Contact


archive-ouverte@inria.fr