HOME | ENGLISH | IMPRESSUM | KIT

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

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

Veröffentlichung
Verifizierte Berechnung von Datenabhängigkeiten

Betreuer

Wissenschaftliche Mitarbeiter
Denis Lohner

Studenten

Ehemalige Studenten
Haoqian Zheng