Das Praktikum gliedert sich in zwei (etwa gleich große) Teile:
Im ersten Teil sind Verifikationsaufgaben in wöchentlichem Turnus individuell zu lösen. Dabei handelt es sich im Wesentlichen um diverse Sortieralgorithmen, deren Korrektheit jeweils zu verifizieren ist.
Im zweiten Teil arbeiten die Studenten in Gruppen. Jede Gruppe arbeitet an einer eigenen Fallstudie, d. h. an einem umfangreicheren Verifikationsproblem, das bislang noch nicht mit VeriFun bearbeitet wurde. Beispiele für Fallstudien, die in früheren Praktika bearbeitet wurden:
- Unentscheidbarkeit des Halteproblems
- Korrektheit des RSA Verschlüsselungsverfahrens
- Korrektheit eines Matching Algorithmus
- Korrektheit des Dijkstra-Algorithmus zum Finden von kürzesten Wegen in Graphen
- Korrektheit eines String-Searching-Algorithmus
- Korrektheitsnachweis für eine Implementierung von AVL-Bäumen
- Korrektheitsnachweis für einen Parser nach dem Prinzip des rekursiven Abstiegs
Lernziele
Formale Modellierung von Korrektheitsaussagen für Programme sowie Beweisführung mittels eines Verifikationswerkzeugs.
Voraussetzungen
Kenntnisse aus Formale Grundlagen der Informatik I–III bzw. Allgemeine Algebra/Logik
Hinweis: Entgegen der Ankündigung im Vorlesungsverzeichnis ist ein Bachelor-Abschluss weder formal noch inhaltlich erforderlich.
Ablauf und Betreuung
Zur Bearbeitung der Aufgaben und Fallstudien stehen Rechner des Fachgebiets zur Verfügung. Alternativ können auch eigene PCs verwendet werden.
In wöchentlichen Treffen stellen die Teilnehmer ihre Lösungen für die in der Vorwoche ausgegebenen Verifikationsaufgaben vor bzw. berichten über ihre Arbeiten an den Fallstudien. Diese Treffen dienen darüber hinaus zur Diskussion von Problemen, die bei den Arbeiten auftreten. Außerhalb dieser Treffen können die Betreuer jederzeit per E-Mail angesprochen werden, auch um – falls erforderlich – individuelle Betreuungstermine zu vereinbaren.
Anmeldung
Sie können sich ab sofort bei Nathan Wasser anmelden.
Vorbesprechung
Dienstag, 13.10.2009, 18:00–19:00 Uhr in Raum S2|02/A213
In der Vorbesprechung werden wir u. a. den Termin für die wöchentlichen Treffen festlegen.
