Universitšt Karlsruhe
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.

Projektbeteiligte

Alumni
Prof. Sabine Glesner
Jan Olaf Blech
Lars Gesellensetter
Ex-Studenten
Denise Dudek
Robert Hartmann
Johannes Leitner
Steffen M√ľlling
Karsten Sperling
Login
Links