Abstract:
 
In 2008, the ACM awarded the prestigious Turing Award to the pioneers
of model checking, Ed Clarke, Allen Emerson, and Joseph Sifakis. Model
checking has evolved in the last twenty-five years into a widely used
verification and debugging technique for both software and hardware.
Model checking is based on exhaustively checking whether a model of a
program or hardware circuit satisfies a property, such as the absence of
deadlocks, or the validity of invariants.  Properties are typically described
using a temporal or modal logic.
This course provides an introduction to the theoretical underpinnings of
model checking.  It covers the temporal logics LTL and CTL, compares
them, and covers algorithms for model checking these logics. 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, i.e., abstraction.  Finally, we discuss verification
techniques for probabilistic models such as Markov chains, and Markov
decision processes.  Such models are used in, e.g., communication
protocols, biological systems, and hardware circuits.
Lecture #1: LTL Model Checking
Lecture #2: CTL Model Checking
Lecture #3: Abstraction
Lecture #4+#5: Probabilistic Model Checking
The course is based on the new textbook "Principles of Model Checking",
that is co-authored with Prof. Christel Baier (TU Dresden), and which
just appeared at MIT Press.
=====================================================================
Short CV:
 
Joost-Pieter Katoen is a full professor at the RWTH Aachen University in
Germany and heads the group on Software Modeling and Verification.
He is also affiliated to the Formal Methods and Tools group of the Dutch
University of Twente. His research interests are in formal verification,
concurrency theory, pointer analysis, semantics, timed and probabilistic
systems. He co-authored about 100 papers in journals and international
conferences, is member of the ETAPS steering commitee, and editorial
board member of the Journal of Software.