Homepage
Sitemap
Kontakt




Universität Bremen Universität Bremen Fachbereich 3 Informatik
Home « Service « Veranstaltungen
Flyer für die Veranstaltung

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

Dr. Sabine Glesner


Datum: 2004-05-12
Uhrzeit: 17.00 Uhr c.t.
Ort: Bremen, Uni Bremen
Treffpunkt: Raum 52 10, MZH


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.



Link zu externer SeiteAnsprechpartner: Prof. Dr. Rolf Drechsler



zurück



English









Zum Seitenanfang Zur Homepage
Zur Sitemap
Kontakt