|
Albert-Ludwigs-Universität Freiburg |
| Institut für mathematische Logik und Grundlagen der Mathematik |
Zeit: Do 14-16
Ort: SR 318 Eckerstr. 1
Model Checking ist ein modelltheoretisches Verfahren zur Analyse
von Computerprogrammen
und Hardware-Systemen. Bei diesem Verfahren wird das Systemdesign formal spezifiziert und in
eine endliche logische Struktur übersetzt; Korrektheits- und Sicherheitseigenschaften werden als
Sätze einer geeigneten Sprache, zum
Beispiel einer Zeitlogik, formuliert. Der Modelchecker prüft
automatisch, ob diese Sätze in der Struktur gelten. Entscheidend
für den praktischen Nutzen des
Verfahrens sind die Berechnungskomplexität von Anfragen als Funktion der Strukturgröße, die
Wahl
geeigneter Spezifikations- und Anfragesprachen und die Suche nach Datenstrukturen und Algorithmen
zur Darstellung und Behandlung großer Strukturen.
In diesem Seminar beschäftigen wir uns sowohl mit den logischen,
automatentheoretischen und
komplexitätstheoretischen Aspekten
von Modelchecking, als auch mit problemspezifischen Sprachen
und
mit Werkzeugen, welche die industrielle Anwendung des Verfahrens
erlauben.
Das Seminar wendet sich an Studierende der Mathematik und der
Informatik. Voraussetzung sind gute
Kenntnisse aus der mathematischen Logik und/oder der theoretischen Informatik. Interessenten mögen
sich an einen der Veranstalter wenden.
Eine Vorbespre
chung findet statt am 8.2.1999 um 13.15 Uhr im SR 318, Eckerstraße 1.
genaueres bei der Informatik
