ETH Zuerich - Homepage
Information Security

Model Checking

Master in Information Security

For more information about the Information Security Master Track visit:


Lecturer: Felix Klaedtke

Classes: Mon 10-12, IFW A 34

Exercises: Mon 14-16, IFW B 42 (Christian Dax) NEW TIME!

Credits: 5

Exam: oral, 20 min, end of semester


Some familiarity with propositional logic, basic computational complexity theory, and basic graph algorithms is assumed. For example, you should know what a tautology is, what NP stands for, and how to find the strongly connected components of a finite graph.

Language: English


As our daily lives depend increasingly on digital systems, the reliability of these systems becomes a concern of overwhelming importance, and as the complexity of the systems grows, their reliability can no longer be sufficiently controlled by the traditional approaches of testing and simulation. Model checking concerns the use of methods for automatically verifying whether hardware or software systems meet their specifications. Over the last two decades, model checking has made enormous progress and is nowadays used in large-scale industrial applications. This course offers an introduction to the theory and practice of model checking. In particular, the course introduces temporal logics (like the branching time temporal logic CTL and the IEEE standardized temporal logic PSL) for specifying properties of concurrent systems and it will present the algorithmic core techniques of model checking (BDD-based, SAT-based, and explicit-state model checking). The course will also teach methods for coping with the state-space explosion problem (e.g., partial-order reduction and counterexample-guided-abstraction refinement). Furthermore, the course will discuss state-of-the-art tools for model checking (like SPIN and NuSMV), which will also be used in the accompanying exercise sessions.




Wichtiger Hinweis:
Diese Website wird in älteren Versionen von Netscape ohne graphische Elemente dargestellt. Die Funktionalität der Website ist aber trotzdem gewährleistet. Wenn Sie diese Website regelmässig benutzen, empfehlen wir Ihnen, auf Ihrem Computer einen aktuellen Browser zu installieren. Weitere Informationen finden Sie auf
folgender Seite.

Important Note:
The content in this site is accessible to any browser or Internet device, however, some graphics will display correctly only in the newer versions of Netscape. To get the most out of our site we suggest you upgrade to a newer browser.
More information

© 2011 ETH Zurich | Imprint | Disclaimer | 15 May 2010