Universitńt Karlsruhe
Project Aktionsplan Informatik

funded by DFG within the "Emmy Noether-Programm"

Verification and Optimization during the Compilation of Higher Programming Languages

-- Sorry, project description only available in german
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.

Participants

Alumni
Prof. Sabine Glesner
Jan Olaf Blech
Lars Gesellensetter
Former Students
Denise Dudek
Robert Hartmann
Johannes Leitner
Steffen M├╝lling
Karsten Sperling
Login
Links