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.

Dieser Kurs führt vor allem in das Thema Model Checking ein. Dies ist ein automatischer Ansatz zur Programmverifikation. Ausserdem werden andere Verifikationsverfahren eingeführt. Für mehr Details siehe die englische Version.

Das Modul wird im Wintersemester 2008/09 angeboten. Vorlesungen gibt es Dienstags und Donnerstags von 14:15 bis 15:55 in HS 1 in E1 3. Übungen gibt es einmal wöchentlich, und zwar Montags entweder 12:00 Uhr bis 14:00 Uhr oder 16:00 Uhr bis 18:00 Uhr.

Wir beginnen am Do, 23.10.2008 (nicht am Di, 21.10.), und enden vorraussichtlich am Do, 12.02.2009 mit einer Klausur. Am Do, 18.12.2008 gibt es vorraussichtlich eine Zwischenklausur, und im Zeitraum 10.01.2009 - 19.01.2009 gibt es eine praktische Aufgabe, für die die Bearbeitungszeit etwa 15 Stunden beträgt.

Die Vorlesungen werden auf englisch gehalten; es gibt englische und deutsche Übungsgruppen. Alle Details finden sich in unserem CMS.

Prof. Dr.-Ing. Holger Hermanns

Reza Pulungan, Msc

Wir werden uns an dem grandiosen Buch 'Principles of Model Checking' von C. Baier und J.-P. Katoen orientieren.

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

Siehe auch:

infobib.cs.uni-sb.de/frames/vorlesungen/verifikation.html