Ein Kontrollflussgraph (CFG) bildet die Grundlage für alle graph-basierten Programmanalysen. Er beschreibt den Ablauf eines Programms, ohne sich um die konkreten Werte der Variablen zu kümmern.
Im Rahmen des
Quis-Custodiet-Projekts wird eine verifizierte, funktionale Implementierung der Kontrollflussgraphenkonstruktion für verschiedene Programmiersprachen benötigt. Als Implementierungsprogrammiersprache und Beweistool wird der Beweisassistent
Isabelle/HOL verwendet.
Aufgabe:
- Einarbeitung in Isabelle/HOL und Kontrollflussgraphen
- Funktionale Implementierung einer Graph-Datenstruktur in Isabelle/HOL
mit Korrektheitsnachweis
- Funktionale Implementierung der Kontrollflussgraphenkonstruktion in Isabelle/HOL für Jinja Bytecode und While
Voraussetzungen
- Kenntnisse in funktionaler Programmierung
- Gute Fertigkeiten im mathematischen Beweisen
- Freude an formal korrektem Arbeiten
Literatur
Veröffentlichungen
Betreuer
