Homepage Sitemap Contact




Home « Service « Events
Flyer für die Veranstaltung

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

Dr. Sabine Glesner


Date: 2004-05-12
Time: 17.00 Uhr c.t.
Place: Bremen, Uni Bremen
Meetingpoint: 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 tp external SiteContact Person: Prof. Dr. Rolf Drechsler



zurück



Deutsch









Sitemap Kontakt

ISMVL2014 DUHDE