HOME | ENGLISH | IMPRESSUM | KIT

Bachelor-/Studienarbeit (abgeschlossen): Verifizierte Berechnung von Kontrollabhängigkeiten

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

Veröffentlichung
Verified Computation of Control Dependencies in a Control Flow Graph

Betreuer

Wissenschaftliche Mitarbeiter
Denis Lohner

Studenten

Ehemalige Studenten
Maximilian Wagner