Optimierende Übersetzer:
Vertrauen ist gut, Verfikation ist besser!

Auch wenn korrekte Übersetzer ein Muss für die Erstellung korrekter Software sind, treten häufig Übersetzungsfehler auf, vor allem bei der Erzeugung von effizientem Maschinencode, der fehleranfälligsten Phase im Übersetzungsprozess. Diese Fehler können nur durch Verifikation vollständig beseitigt werden. Technisch gesehen stellt die Tatsache, dass die dabei nötigen Optimierungen keine Verfeinerungen sind, eine besondere Herausforderung dar.

In meiner Forschung untersuche ich die Verifikation von Optimierungen und Codeerzeugungsverfahren, die aus Zwischenrepräsentationen mit statischer Einmalzuweisung (SSA=static single assignment) ausführbaren Maschinencode für neueste Prozessorarchitekturen (Itanium, ARM, TriMedia) erzeugen. Neben der Beschreibung der Spezifikation und Verifikation dieser optimierenden Codeerzeugung mit Hilfe des Theorembeweisers Isabelle/HOL stelle ich dar, wie die Implementierungskorrektheit solcher Optimierungsverfahren mit Programmprüfung sichergestellt werden kann. Dabei beschreibe ich auch einen Programmprüfer, den wir für einen Codegenerator in einem industriellen Projekt erstellt haben.

Ansprechpartner: Prof. Dr. Rolf Drechsler