Course: Principles of Model Checking

University of Twente, Enschede,
September 5, 12, 26 and October 3, 2012

Content

A prominent verification technique that has emerged in the last thirty years is model checking, that systematically checks whether a model of a given system satisfies a property such as deadlock freedom, invariants, or request-response. This automated technique for verification and debugging has developed into a mature and widely-used industrial approach with many applications in software and hardware.

This course provides an introduction to the theory of model checking and its theoretical complexity. We introduce transition systems, safety, liveness and fairness properties, as well as omega-regular automata. We then cover the temporal logics LTL, CTL and CTL*, compare them, and treat their model-checking algorithms. Techniques to combat the state-space explosion problem are at the heart of the success of model checking. We provide an overview of an important class of such techniques, namely abstraction. Finally, we consider model checking of timed automata and of probabilistic automata. The course consists of lectures and active involvement in exercise classes.

Prerequisites

Basic knowledge of algorithms and data structures, complexity theory, and mathematical logic at bachelor level.

Course Planning

Two lectures take place per day. Dates are fixed, but content may slightly change per day. Exact times will be communicated later.

5 September: Transition Systems (Chapter 2) Linear-Time Properties (Chapter 3+4)
12 September: Linear Temporal Logic (Chapter 5) Computation Tree Logic (Chapter 6)
26 September: Abstraction (Bi)simulation and stutter variants thereof (Chapter 7)
3 October: Partial-Order Reduction (Chapter 8) Symbolic Model Checking (Chapter 6)

About Joost-Pieter Katoen

Joost-Pieter Katoen is a professor at the RWTH Aachen University (since 2004) and is associated as part-time professor to the University of Twente. His research interests are concurrency theory, model checking, timed and probabilistic systems, and semantics. He co-authored more than 170 journal and conference papers, and a comprehensive book (with Christel Baier) on Principles of Model Checking (MIT Press) which provides the basis for this course.

Registration

One can register by sending an email to Timmer ‘at’ cs ‘dot’ utwente ‘dot’ nl with subject IPA Registration for PMC. Include your affiliation details in the message body. Registration closes on August 25, 2012. Admission to the course is free of charge for IPA PhD students.