A structured approach to proving compiler optimizations based on dataflow analysis

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; Types for Proofs and Programs International Workshop, TYPES 2004, Revised Selected Papers. <10.1007/11617990>
Liste complète des métadonnées


https://hal.inria.fr/inria-00289549
Contributeur : Xavier Leroy <>
Soumis le : samedi 21 juin 2008 - 13:58:12
Dernière modification le : lundi 5 octobre 2015 - 16:58:39
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

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; Types for Proofs and Programs International Workshop, TYPES 2004, Revised Selected Papers. <10.1007/11617990>. <inria-00289549>

Partager

Métriques

Consultations de
la notice

276

Téléchargements du document

124