Master Thesis

Isabelle/Imperative-HOL ist eine einfache imperativ-funktionale Sprache in Isabelle/HOL. Ziel der Arbeit ist es eine einfache imperative Datenstruktur (Skip Lists oder Hash Maps) in Imperative-HOL zu implementieren und zu verifizieren.

Isabelle/HOL bietet automatische Codegenerierung von funktional-imperativer Spezifikationen. Um effizienten Code zu erzeugen, werden effiziente Implementierungen von einfachen Datenstrukturen, wie z.B. Maps, benötigt. Diese Datenstrukturen müssen in Isabelle implementiert und spezifiziert werden und die Korrektheit der Operationen muss mit Hilfe des Theorembeweisers bewiesen werden.

Aufgaben:
Einarbeitung in den Theorembeweiser Isabelle und die Sprache Imperative-HOL, Implementierung effizienter Datenstrukturen in Isabelle/HOL und Evaluation der Performanz, Verifikation der Operationen in Isabelle
Nützliche Vorkenntnisse:
gute Kenntnisse einer funktionalen Programmiersprache (z.B. ML, OCaml oder Haskell), Kenntnisse von algebraischen Spezifikationen, Kenntnisse in Logik und Beweisverfahren
Betreuer:
Peter Lammich, Raum MI 00.09.065, email {lammich} AT [in.tum.de]
Aufgabensteller:
Prof. Tobias Nipkow, Raum MI 00.09.055, email {nipkow} AT [in.tum.de]