direkt zum Inhalt springen

direkt zum Hauptnavigationsmenü

Sie sind hier

TU Berlin

Page Content


Formal Verification of Dead Code Elimination in Isabelle/HOL
Citation key BGGsept2005
Author Jan Olaf Blech and Lars Gesellensetter and Sabine Glesner
Title of Book Proceedings of the 3rd IEEE International Conference on Software Engineering and Formal Methods
Pages 200-209
Year 2005
Address Koblenz, Germany
Publisher IEEE Computer Society Press
Organization IEEE
Abstract 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.
Bibtex Type of Publication Conference Article
Download Bibtex entry

Zusatzinformationen / Extras

Quick Access:

Schnellnavigation zur Seite über Nummerneingabe

Auxiliary Functions