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.