Aktionsplan-Informatik: Verifikation und Optimierung bei der Übersetzung höherer Programmiersprachen

• Antragstellerin: Professorin Dr. Sabine Glesner
• Fachliche Zuordnung: Softwaretechnik und Programmiersprachen
• Förderung: Förderung von 2004 bis 2015
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 5423501

Das Ziel des hier vorgestellten 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 unserer Arbeit wollen wir uns auf Prozessoren mit folgenden Merkmalen konzentrieren: Prozessoren mit sehr langen Instruktionswörtern (very long instruction words, VLIW), mit bedingten (predicated) Instruktionen und mit spekulativer Ausführung. Dabei wollen wir insbesondere untersuchen, wie wir optimierende, maschinenabhängige Transformationen mittels Graphersetzungsmethoden ausdrücken können. Des weiteren wollen wir klären, wie solche Transformationen mit Isabelle/HOL formal verifiziert werden können und wie wir mit Programmprüfung ihre korrekte Implementierung sicherstellen können.

• DFG-Verfahren: Emmy Noether-Nachwuchsgruppen (Aktionsplan Informatik)