4-Day Course on Principles of Model Checking
	University of Twente, Enschede September 5, 12, 26 and October 3, 2012

 

 

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.

In 2008, the ACM awarded the prestigious Turing Award - the Nobel Prize in Computer Science - to the pioneers of Model Checking: Ed Clarke, Allen Emerson, and Joseph Sifakis.

 

Why? Because model checking has evolved in the last twenty-five years into a widely used verification and debugging technique for both software and hardware.

 

It is used (and further developed) by companies and institutes such as IBM, Intel, NASA, Cadence, Microsoft, and Siemens, to mention a few, and has culminated in a series of mostly freely downloadable software tools that allow the automated verification of, for instance, C#-programs or combinational hardware circuits.

Subtle errors, for instance due to multi-threading, that remain undiscovered using simulation or peer reviewing can potentially be revealed using model checking.  Model checking is thus an effective technique to expose potential design errors and improve software and hardware reliability.

 

But how does it work, that is, what are its underlying principles?

That's exactly the focus of this 4 day course!

 

We will show that model checking is based on well-known paradigms from automata theory, graph algorithms, logic, and data structures.  Its complexity is analyzed using standard techniques from complexity theory.

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

September 5:
08:45-10:30 Transition Systems & Linear-Time Properties (Ch. 2+3)
13:45-15:30 Verifying Regular Linear-Time Properties (Ch. 4)

September 12:
10:45-12:30 Linear Temporal Logic (Ch. 5)
13:45-15:30 Computation Tree Logic (Ch. 6)

September 26:
10:45-12:30 Abstraction, Part 1 (Ch. 7)
13:45-15:30 Abstraction, Part 2 (Ch. 7)

October 3:
10:45-12:30 Partial-Order Reduction (Ch. 8)
13:45-15:30 Probabilistic Model Checking (Ch. 10)

 

The lectures in the morning take place in Ravelijn Room RA 3336;
the afternoon lectures take place in Ravelijn RA 2334.

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

The following persons will assist during the exercise classes: