Datenabhängigkeiten beschreiben, von welchen Anweisungen eines Programms eine andere Anweisung die dort verarbeiteten Daten bezieht. Compiler und Programmanalysen verwenden diese Abhängigkeiten, um Optimierungen durchzuführen bzw. Programmeigenschaften herzuleiten.
Im Rahmen des
Quis-Custodiet-Projekts wird eine verifizierte, funktionale Implementierung zur Berechnung der Datenabhängigkeiten benötigt. Als Implementierungsprogrammiersprache und Beweistool wird der Beweisassistent
Isabelle/HOL verwendet.
Aufgabe:
- Einarbeitung in Isabelle/HOL
- Implementierung der Berechnung der Datenabhängigkeiten mittels einer Gen-/Kill-Datenflussanalsye
- 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 Datenabhängigkeiten mittels Datenflussanalysen:
Vorlesung:
Kapitel über Datenflussanalysen
Veröffentlichungen
Betreuer
Studenten
