HOME | ENGLISH | IMPRESSUM | KIT

Bachelor-/Studienarbeit (abgeschlossen): Funktionale Summary-Kanten-Berechnung für PDGs

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

Veröffentlichung
Verifizierte Summary Kanten Berechnung in System Dependence Graphs

Betreuer

Wissenschaftliche Mitarbeiter
Denis Lohner
Ehemalige Mitarbeiter
Dr. rer. nat. Andreas Lochbihler