Programmabhängigkeitsgraphen sind die Grundlage unseres Analysetools
Joana. Um mit diesen effiziente Analysen durchführen zu können, müssen diese mit zusätzlichen Summary-Kanten ergänzt werden.
Im Rahmen des
Quis-Custodiet-Projekts wird eine verifizierte, funktionale Implementierung benötigt, die in einen Programmabhängigkeitsgraphen die nötigen Summary-Kanten einfügt. Als Implementierungsprogrammiersprache und Beweistool wird der Beweisassistent
Isabelle/HOL verwendet.
Aufgabe:
- Einarbeitung in Isabelle/HOL
- Implementierung der Berechnung der Summary-Kanten
- 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
- Programmabhängigkeitsgraphen mit Summary-Kanten:
-
Jeanne Ferrante, Karl J. Ottenstein und Joe D. Warren.
The program dependence graph and its use in optimization.
ACM Trans. Program. Lang. Syst. 9, 3 (July 1987), 319-349.
-
Susan Horwitz, Thomas Reps und David Binkley.
Interprocedural Slicing Using Dependence Graphs.
ACM Trans. Prog. Lang. Syst. 12 1 (1990). 26-60
.
- Berechnung der Summary-Kanten:
Thomas Reps, Susan Horwitz, Mooly Sagiv und Genevieve Rosay.
Speeding up slicing.
SIGSOFT Softw. Eng. Notes 19, 5 (December 1994), 11-20.
Veröffentlichungen
Betreuer
