HOME | ENGLISH | IMPRESSUM | KIT

Studienarbeit (abgeschlossen): Verifizierte Implementierung von Patricia-Bäumen

Patricia-Bäume sind eine effiziente Baum-Datenstruktur für Maps mit ganzzahligen Schlüsseln und Mengen von ganzen Zahlen. Die Haskell-Standardbibliothek implementiert Patricia-Bäume in Data.IntMap. Patricia-Bäume haben gegenüber gewöhnlichen Suchbämen wie AVL- oder Rot-Schwarz-Bäumen den Vorteil, dass sie auch die Vereinigung von Bäumen effizient unterstützen.

Aufgabe:

Ziel der Arbeit ist es, Big Endian Patricia-Bäume und die Standard-Operationen lookup, Einfügen und Vereinigung in Isabelle/HOL zu formalisieren und als korrekt nachzuweisen. Ggf. kann man weitere Operationen wie Löschen oder Traversion auch noch hinzufügen. Die formalisierten Operationen sollen mittels Isabelles Code Generator ausführbar sein. Für die implementierten Operationen soll die Laufzeit des generierten Codes mit anderen Datenstrukturen in Isabelle (z.B. Rot-Schwarz-Bäume) verglichen werden. Das Herausfordernde an der Arbeit wird sein, die nötigen Invarianten für die Bäume zu finden.

Voraussetzungen

  • Kenntnisse in funktionaler Programmierung
  • Analytisches Denkvermögen
  • Freude an formal korrektem Arbeiten

Literatur

  • Einführung in Isabelle/HOL: Tutorial und Praktikum
  • D. R. Morrison: PATRICIA - practical algorithm to retrieve information coded in alphanumeric. J. ACM 15,4 (1968), pp. 514-534.
  • Chris Okasaki and Andrew Gill: Fast Mergeable Integer Maps. In: Workshop on ML, 1998, pp. 77-86.


Veröffentlichungen

Veröffentlichung
Verifizierte Implementierung von Patricia-Bäumen

Betreuer

Wissenschaftliche Mitarbeiter
Denis Lohner
Ehemalige Mitarbeiter
Dr. rer. nat. Andreas Lochbihler

Studenten

Ehemalige Studenten
Tim Habermaas