Master in Information Security
For more information about the Information Security Master Track visit: http://www.infsecmaster.ethz.ch
Lecturers: Felix Klaedtke
Classes: Mon 10-12, CAB G 59
Exercises: Mon 13-15, CAB G 59 (Eugen Zalinescu)
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.
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.
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
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.