Universität Karlsruhe
Formal Verification of Dead Code Elimination in Isabelle/HOL


[BGGsept2005]Jan Olaf Blech, Lars Gesellensetter, Sabine Glesner, Formal Verification of Dead Code Elimination in Isabelle/HOL, Proceedings of the 3rd IEEE International Conference on Software Engineering and Formal Methods, IEEE, IEEE Computer Society Press, september 2005.


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 non-termination adequately. Finally we report on our implementation of this verified DCE algorithm in the industrial-strength Scale compiler system.

[Erzeuge bibTeX Eintrag]


Prof. Sabine Glesner
Jan Olaf Blech
Lars Gesellensetter