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.
Document type :
Conference papers
Complete list of metadatas

Cited literature [7 references]  Display  Hide  Download
https://hal.inria.fr/inria-00289549
Contributor : Xavier Leroy <>
Submitted on : Saturday, June 21, 2008 - 1:58:12 PM
Last modification on : Wednesday, September 12, 2018 - 1:16:38 AM
Long-term archiving on : Friday, September 28, 2012 - 4:26:05 PM

File

proofs_dataflow_optimizations....
Files produced by the author(s)

Identifiers

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. pp.66-81, ⟨10.1007/11617990⟩. ⟨inria-00289549⟩

Export

BibTeX TEI DC DCterms EndNote

Share

Metrics

Record views

380

Files downloads

235

Contact


archive-ouverte@inria.fr