Bachelor Thesis

Isabelle/HOL ist ein generischer Theorembeweiser, der sich hervorragend für Spezifikation und Verifikation funktionaler Programme eignet. Mittels Codegenerierung können aus Spezifikationen unmittelbar Prototypen in einer funktionalen Programmiersprache erzeugt werden, z.B. in ML, in Haskell, oder in (einer Teilmenge von) Scala.

Um die Effizienz dieser Prototypen zu steigern, sind effiziente Datenstrukturen erforderlich. Bekannte Beispiele hierfür sind balancierende Suchbäume (z.B. 2-3-Bäume); es gibt aber noch viel mehr Kandidaten. Eine Auswahl hiervon soll als Isabelle-Theorie implementiert und gegen eine naive Referenzimplementierung verifiziert werden.

Arbeitsumgebung:
Isabelle, Linux
Nützliche Vorkenntnisse:
Funktionales Programmieren, Logik, Isabelle
Betreuer:
Lukas Bulwahn, Raum FMI 00.11.055, email {haftmann} AT [in.tum.de]
Aufgabensteller:
Prof. Tobias Nipkow, Raum FMI 01.11.058, email {nipkow} AT [in.tum.de]