Course Material, Caltech 2008, CS 118


Logic Model Checking

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.

Lecture Notes

Announcement

Assignments and Exercises

Teaching Assistant

Some Background material

for more on mutual exclusion algorithms, and design of distributed algorithms in general, consider:

Course Textbook


Spin homepage