This course offers an introduction to the theory and practice of logic model
checking as an aid in the formal verification of concurrent and multi-threaded
software systems. The specific focus is on the automata-theoretic verification
method, on the formalization of properties in linear temporal logic, and the use
of the SPIN model checker.
This year we will also cover model-driven
verification techniques using abstraction, and distributed model checking
algorithms (the use of large shared memory machines with multicore cpus to
verify models of multi-threaded software systems).
Course Assignments: The course consists of roughly 18 lectures, a series of take-home assignments, and self-paced work with the model checker. Some of the assignments will require significant labtime/home-work with the model checker.
Labtime/Homework: In the first week of the course you will be asked to install Spin on your preferred system, and throughout the course you're expected to experiment with the model checker to learn in more detail about all concepts explained in the course. Try small examples to develop and fine-tune model building and model verification skills, and to develop insight in the primary verification strategies using model checkers. Self-paced lab work is required and all students are encouraged and expected to ask questions about this work in class throughout the course.
At the end of the course you should have a good fundamental insight into the theory of logic model checking based on the automata-theoretic method, and the direction in which the research in this area is evolving, and you should be able to handle significant real-world software verification problems, especially of systems involving concurrency.
All lecture notes and assignments will be posted on this website.
for more on mutual exclusion algorithms, and design of distributed algorithms in general, consider:
Michel Raynal, Algorithms for Mutual Exclusion, MIT Press, 1986. Michel Raynal, Distributed Algorithms and Protocols, Wiley&Sons, 1988. Gerard Tel, Topics in Distributed Algorithms, Cambridge Univ. Press, 1991.
Required: The Spin Model Checker: Primer and Reference Manual. Gerard J. Holzmann. Addison-Wesley, 2004.Optional:
Principles of Spin, M. Ben-Ari, Springer Verlag, Jan. 2008.Principles of Model Checking, C. Baier and J-P. Katoen. MIT Press, Spring 2008 (to appear).
Principles of concurrent and Distributed Programming (the 2nd Edition, which is based on Spin), Ben-Ari, Addison-Wesley, 2006.
Model Checking, Ed Clarke, Orna Grumberg, and Doron Peled. MIT Press, 1999.