Institut für Rechnerarchitektur
und Parallelrechner
Hauptseite
Projektübersicht
Ziel des Projektes war die formale Code-Level Verifikation eines Compilers für die C-ähnliche Sprache C0. Der Korrektheitsbeweis besteht aus zwei Teilen:
  1. Formale Spezifikation der Code-Generierung im Theorembeweiser Isabelle/HOL.
    Für den funktionalen Code-Generator haben wir beweisen, dass die Ausführung des generierten Assemblercodes für ein bestimmtes C0 Programm auf der abstrakten Assemblermaschine des VAMP-Prozessors eine Simulation der Ausführung des ursprünglichen C0-Programms auf einer abstrakten C0-Maschine darstellt.
  2. Im zweiten Teil implementieren wir den C0-Compiler in C0 und zeigen, dass die Compiler-Implementierung in C0 und die Compiler-Spezifikation in Isabelle/HOL den gleichen Assemblercode erzeugen.
 
Projektstatus
Das Projekt ist abgeschlossen. Die formalen Artefakte sind über das Verisoft Repository verfügbar.
 
Projektmitarbeiter
M. Sc. Abdul Qadar Kara
Dr. Dirk Leinenbach
Dr. Hristo Pentchev
Dr. Elena Petrova
Verena Kremer