| HAL-Inria | Publications, software ... of Inria's scientists |
Conference papers
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.
Cited literature [7 references]
https://hal.inria.fr/inria-00289549
Contributor : Xavier Leroy <>
Submitted on : Saturday, June 21, 2008 - 1:58:12 PM
Last modification on : Thursday, January 7, 2021 - 3:40:05 PM
Long-term archiving on: : Friday, September 28, 2012 - 4:26:05 PM
Contributor : Xavier Leroy <>
Submitted on : Saturday, June 21, 2008 - 1:58:12 PM
Last modification on : Thursday, January 7, 2021 - 3:40:05 PM
Long-term archiving on: : Friday, September 28, 2012 - 4:26:05 PM
File
proofs_dataflow_optimizations....
Files produced by the author(s)