VERIFIKATION
Publikum

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 und andere automatische Ansätze zur Programmverifikation ein. Für mehr Details siehe die englische Version oder unser dCMS.


Dozent

Prof. Dr.-Ing. Holger Hermanns

Assistenten

Yulyia Butkova, BSc
Alexander Graf-Brill, MSc
Arnd Hartmanns, MSc

Übungsleiter

Felix Freiberger

Literatur

Wir werden uns am 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

  • J.-P. Katoen:

    Concepts, Algorithms and Tools for Model Checking,

    Erlangen: Institut für Mathematische Maschinen und Datenverarbeitung, 1999

Siehe auch:

www.infomath-bib.de/tmp/vorlesungen/info-core_verification.html