direkt zum Inhalt springen

direkt zum Hauptnavigationsmenü

Sie sind hier

TU Berlin

Inhalt des Dokuments

Projekt 'Aktionsplan Informatik'

gefördert von der DFG im Rahmen des Emmy Noether-Programms

Verifikation und Optimierung bei der Übersetzung höherer Programmiersprachen

Das Gesamtziel des Forschungsprojekts ist die Entwicklung einer Methodik zur korrekten und optimierenden Codeerzeugung für neueste Formen von Prozessorarchitekturen. Übersetzer (Compiler) sind das Herzstück bei der Erstellung von Software, erlauben sie es doch, Programme in höheren Programmiersprachen zu schreiben, die dann mit Hilfe von Übersetzern in Maschinencode transformiert werden. Um zuverlässige Software zu erstellen, ist es daher unbedingt erforderlich, dass Übersetzer nachweislich korrekt arbeiten. Außerdem müssen Übersetzer die Architekturen moderner Hardwarestrukturen ausnutzen und darauf optimierten Maschinencode erzeugen, damit auch die Effizienz des erzeugten Maschinencodes gewährleistet ist. In diesem Projekt konzentrieren wir uns auf Prozessoren mit folgenden Merkmalen: Prozessoren mit sehr langen Instruktionswörtern (very long instruction words, VLIW), mit bedingten (predicated) Instruktionen und mit spekulativer Ausführung. Dabei soll insbesondere untersucht werden, wie optimierende, maschinenabhängige Transformationen mittels Graphersetzungsmethoden ausgedrückt werden können. Des weiteren soll geklärt werden, wie solche Transformationen mit Isabelle/HOL formal verifiziert werden können und wie ihre korrekte Implementierung mit Programmprüfung sichergestellt werden kann.

Zusatzinformationen / Extras

Direktzugang

Schnellnavigation zur Seite über Nummerneingabe