Third IEEE International Conference on Software Engineering and Formal Methods (SEFM'05) (2005)
Sept. 7, 2005 to Sept. 9, 2005
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/SEFM.2005.20
Jan Olaf Blech , University of Karlsruhe, Karlsruhe, Germany
Lars Gesellensetter , University of Karlsruhe, Karlsruhe, Germany
Sabine Glesner , University of Karlsruhe, Karlsruhe, Germany
Correct compilers are a vital precondition to ensure software correctness. Optimizations are the most error-prone phases in compilers. In this paper, we formally verify dead code elimination (DCE) within the theorem prover Isabelle/ HOL. DCE is a popular optimization in compilers which is typically performed on the intermediate representation. In our work, we reformulate the algorithm for DCE so that it is applicable to static single assignment (SSA) form which is a state of the art intermediate representation in modern compilers, thereby showing that DCE is significantly simpler on SSA form than on classical intermediate representations. Moreover, we formally prove our algorithm correct within the theorem prover Isabelle/HOL. Our program equivalence criterion used in this proof is based on bisimulation and, hence, captures also the case of nontermination adequately. Finally we report on our implementation of this verified DCE algorithm in the industrialstrength Scale compiler system.
J. O. Blech, S. Glesner and L. Gesellensetter, "Formal Verification of Dead Code Elimination in Isabelle/HOL," Third IEEE International Conference on Software Engineering and Formal Methods(SEFM), Koblenz, 2005, pp. 200-209.