VERIFIKATION
 | ||
|
Diese Stammvorlesung richtet sich an Studierende im Bachelor oder Master Informatik, Bio-Informatik, CuK oder Computerlinguistik. Studierende im Bachelor müssen die Grundvorlesung Programmierung 1 erfolgreich absolviert haben. Die Vorlesungen Mathematik 1 und 2, Programmierung 2, sowie Theoretische Informatik sind empfohlen.
Inhalt
Dieser Kurs führt in das Thema Model Checking ein. Dies ist ein automatischer Ansatz zur Programmverifikation. Für mehr Details siehe die englische Version.
Termine
Das Modul wird im Wintersemester 2006/07 angeboten. Vorlesungen gibt es Dienstags und Donnerstags von 14:00 bis 16:00, Übungen gibt es einmal wöchentlich, und zwar Mittwochs entweder 14:00 Uhr bis 16:00 Uhr oder 16:00 Uhr bis 18:00 Uhr.
Wir beginnen vorraussichtlich am 17.10.2006 und enden am 15.02.2007
mit einer Klausur. Am 21.12.2006 gibt es vorraussichtlich eine Zwischenklausur, und zwischen 15.01.07 - 21.01.07 gibt es eine praktische Aufgabe, fuer die die Bearbeitungszeit etwa 20 Stunden beträgt.
Die Vorlesungen werden auf englisch gehalten; es gibt englische und deutsche Übungsgruppen. Alle Details finden sich in unserem CMS.
Bitte melden Sie sich im CMS an, um weitere Informationen zu erhalten!
Dozent
 | Prof. Dr.-Ing. Holger Hermanns |
Assistenten
| Dipl.-Inf. Lijun Zhang |
| Dipl.-Inf. Sven Johr |
Übungsleiter
| Wasilli Anastasatos |
| Christian Eisentraut |
| Patrick Wischnewski |
Literatur
Wir werden uns am Manuskript des Buches 'Principles of Model Checking' von C. Baier und J.-P. Katoen orientieren. Die letzen Versionen dieses Manuskriptes sind nicht elektronisch verfügbar. Es ist aber eine aktuelle Version zum Kopieren verfügbar (z.Zt. Kapitel 1-6). Ein weiteres Kopierexemplar wird sich auch in der CIAM finden. Wenn Sie (Tipp)fehler finden, bitte auf dieser Seite eintragen.
Zusätzliche relevante Literatur:
M. Huth and M.D. Ryan:
Logic in Computer Science -- Modelling and Reasoning about Systems, Cambridge University Press, 2nd edition, 2004
K. Schneider:
Verification of Reactive Systems, Springer-Verlag, Texts in Theoretical Computer Science. An EATCS Series, 2004
E.M. Clarke, O. Grumberg, D.A. Peled:
Model Checking, MIT Press, 1999
K.L. McMillan:
Symbolic Model Checking, Kluwer Academic, 1993
J.-P. Katoen:
Concepts, Algorithms and Tools for Model Checking,
Erlangen: Institut für Mathematische Maschinen und Datenverarbeitung, 1999
Siehe auch:
infobib.cs.uni-sb.de/frames/vorlesungen/verifikation.html