Kontrollabhängigkeiten beschreiben, welche Anweisungen eines Programms über die Ausführung anderer Anweisungen entscheiden, z. B. kontrolliert ein
if die Anweisungen im
then- bzw.
else-Zweig. Für Sprachen mit
gotos lassen sich diese Abhängigkeiten nicht mehr direkt am Sourcecode ablesen, dafür braucht es eine entsprechende Analyse.
Im Rahmen des
Quis-Custodiet-Projekts wird eine verifizierte, funktionale Implementierung zur Berechnung der Kontrollabhängigkeiten benötigt. Als Implementierungsprogrammiersprache und Beweistool wird der Beweisassistent
Isabelle/HOL verwendet.
Aufgabe:
- Einarbeitung in Isabelle/HOL
- Implementierung der Berechnung der Kontrollabhängigkeiten mittels Postdominatoren
- Korrektheitsbeweis für die Implementierung
Voraussetzungen
- Kenntnisse in funktionaler Programmierung
- Gute Fertigkeiten im mathematischen Beweisen
- Freude an formal korrektem Arbeiten
- Grundkenntnisse im Compilerbau sind vorteilhaft, aber nicht notwendig
Literatur
- Einführung in Isabelle/HOL:
Tutorial
und
Praktikum
- Berechnung der Postdominatoren und Kontrollabhängigkeiten:
- Keith D. Cooper, Timothy J. Harvey und Ken Kennedy.
A Simple, Fast Dominance Algorithm.
-
J. Ferrante, K. J. Ottenstein und J. D. Warren.
The program dependence graph and its use in optimization.
ACM Transactions on Programming Languages and Systems,
9(3):319--349, July 1987.
-
Vorlesung:
Kapitel über Datenflussanalysen
Veröffentlichungen
Betreuer
Studenten
