Yves Bertot, Benjamin Grégoire, and Xavier Leroy. A structured approach to proving compiler optimizations based on dataflow analysis. In TYPES 2004: Types for Proofs and Programs, number 3839 in LNCS, pages 66--81. Springer, 2006.

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.

[ bib | DOI | Local copy | At publisher's site ] Back

This file was generated by bibtex2html 1.99.