direkt zum Inhalt springen

direkt zum Hauptnavigationsmenü

Sie sind hier

TU Berlin

Inhalt des Dokuments


Formal Verification of Dead Code Elimination in Isabelle/HOL
Zitatschlüssel BGGsept2005
Autor Jan Olaf Blech and Lars Gesellensetter and Sabine Glesner
Buchtitel Proceedings of the 3rd IEEE International Conference on Software Engineering and Formal Methods
Seiten 200-209
Jahr 2005
Adresse Koblenz, Germany
Verlag IEEE Computer Society Press
Organisation IEEE
Zusammenfassung 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.
Typ der Publikation Conference Article
Download Bibtex Eintrag

Zusatzinformationen / Extras


Schnellnavigation zur Seite über Nummerneingabe