Logic Model Checking, Caltech 2011, Winter Term


Course Material CS 118, TThu, 1:00-2:25pm, 107 Annenberg


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.
Towards the end of the course we will also cover model-driven verification techniques and swarm-based verification methods using grids or shared-memory machines.

Assignments: The course consists of 18 lectures, 7 assignments, and self-paced work with the Spin model checker. Some of the assignments will require significant labtime/home-work, working on finding abstractions for problems such that verification becomes tractable. The last two assignments are most important and each count for 25% of the grade. The first five assignments count for 10% of the final grade each. All assignments require individual work (there are no team assignments). The maximum score for each assignment is 100 points. If you send in your solutions late, 10 points are deducted for every 24 hour period or part thereof. (I.e., at the start of the 10th day late, zero points remain.)

A letter grade for the course is derived from the following ranges for the weighted average score on all assignments:

	95 - 100  = A+
	85 - 94   = A
	80 - 84   = B+
	70 - 80   = B
	65 - 69   = C+
	55 - 64   = C
Labtime/Homework: In the first week of the course you will be asked to download and install the latest version of Spin model checker on your preferred system. Throughout the course you are expected to experiment with it to learn in more detail about concepts explained in the lectures.
You are encouraged to try small examples to develop and fine-tune model building, abstraction, and verification skills, and to develop insight in the verification strategies that are typically used with 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 automata-theoretic verification, and the direction in which the research in this area is evolving. At this point you should be able to handle significant real-world software verification problems, especially of systems involving concurrency.

Lectures

Assignments and Exercises