6-Day Course on Principles of Model Checking
	University of Twente, Enschede September 29 – October 2, and October 8+9, 2009

 

 

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 6 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.

 

A overview of the buildings at the University of Twente can be found here.

Locations: LA = building Langezijds (building 17 on the map), Cu = building Cubicus (building 41 on the map)

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.

We have made some block bookings with the following hotels/pensions: (all indicated rates include breakfast)

• “De Drienerburght”, located on the UT campus

• “Logica” is fully booked now. Please choose a different accommodation.

• “De Broeierd”, located within walking distance of the UT campus

These rates are lower than the rates that typically are obtained when booking directly.

You can indicate on the registration form your needs and preferences concerning accommodation.

Registration is free, but you need to register using the form below. Registration does not include coffee breaks and lunches. Course slides will be made available via this webpage.

It is convenient if participants have a copy of the book “Principles of Model Checking” at their disposal. (The costs are 48 euro for a book of 975 pages, see www.amazon.de.) We will, however, also have some copies of the book available for usage during the course.

The following persons will assist during the exercise classes: