Modul 63077 Masterseminar Modellierung und Verifikation
Modulinformationen
In vielen Anwendungsfällen möchte man sicher sein, dass ein Programm korrekt ist, also die gewünschten Eigenschaften hat. Besonders wenn Fehler extrem teuer oder gar lebensbedrohlich sein können, ist die Risikobereitschaft beim Einsatz von Software naturgemäß gering. Testen ist für solch sicherheitskritische Software unzureichend, denn Tests können nur bestehende Fehler aufdecken, aber nicht die Fehlerfreiheit attestieren. Daher wäre es wünschenswert, ein allgemeines Verifikationsverfahren zu haben, um die Korrektheit eines Programms zu beweisen. Der Satz von Rice stellt hier allerdings eine natürliche Grenze dar, dernach das Verifikationsproblem im Allgemeinen unentscheidbar ist. In diesem Seminar werden wir verschiedene Techniken betrachten, die es ermöglichen, das Verifikationsproblem - jedenfalls in gewissen Fällen - zu lösen. Behandelt werden unter anderem die Themen Verhaltensäquivalenzen, Model Checking und Abstrakte Interpretation.
| ECTS | 10 |
|---|---|
| Arbeitsaufwand | Es sind zu erstellen: Eine Ausarbeitung, eine Übungsaufgabe für die übrigen Seminarteilnehmer samt Musterlösung und ein Vortrag (empfohlen: mit unterstützenden Folien) |
| Dauer des Moduls | ein Semester |
| Häufigkeit des Moduls | in jedem Semester |
| Anmerkung | Für die Teilnahme an einem Seminar ist ein gesondertes Anmeldeverfahren im Vorsemester über folgenden Link erforderlich:
|
| Inhaltliche Voraussetzung | Es wird empfohlen, eine einführende Lehrveranstaltug in die Theoretische Informatik im Vorfeld zu besuchen. |
Prüfungsinformation
| M.Sc. Data Science | |
|---|---|
| Art der Prüfungsleistung | benotete Seminarteilnahme: Ausarbeitung (soll 5-10 Seiten umfassen) und Vortrag |
| Voraussetzung | keine |
| Stellenwert der Note | 1/12 |
| Formale Voraussetzungen | mindestens drei Pflichtmodulprüfungen sind bestanden |
| M.Sc. Wirtschaftsinformatik | |
| Art der Prüfungsleistung | benotete Seminarteilnahme: Ausarbeitung (soll 5-10 Seiten umfassen) und Vortrag |
| Voraussetzung | keine |
| Stellenwert der Note | s. PO |
| Formale Voraussetzungen | mindestens drei Wahlmodulprüfungen müssen bestanden sein |
Download
Ansprechpersonen
Dr. Sebastian Küpper
mathinf.webteam
| 26.09.2024
