| Titel | Spezifikation und Verifikation |
| Semester | Wintersemester 2015/16 |
| Modul | Master-Praktikum (IN2106) |
| TUMonline | Modul auf TUMonline |
| Voraussetzungen | Grundlegende Kenntnisse in Isabelle (z.B. Semantik (IN2055), Interactive Software Verification (IN3350)) |
| ECTS | 10 |
| Organisation | Lars Hupel, Tobias Nipkow |
Das Praktikum ist semesterbegleitend. Es wird von den Teilnehmern selbstständig ein Projekt mittels des Theorembeweisers Isabelle bearbeitet.
Die Anmeldung und Platzvergabe läuft regulär über das Matchingsystem. Eine Vorbesprechung findet nicht statt. Melden Sie sich bitte stattdessen vorher unbedingt bei Lars Hupel per Mail, wobei Sie kurz erläutern sollen, ob und woher Sie Isabelle-Kenntnisse haben (z.B. durch Besuch einer der obigen Vorlesungen). Wenn Sie vorab Fragen zum Ablauf, den Themen oder anderen Aspekten haben, können Sie gern auch eine Mail schreiben.
Die Themen werden vor Beginn des Praktikums mit den Teilnehmern abgestimmt. Es besteht die Möglichkeit, Themen aus verschiedenen Bereichen zu bearbeiten, z.B. formale Mathematik, Formalisierung von Softwaresystemen, ...