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

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

• You are strongly encouraged to attend the lectures, to ask questions, to start discussions.

Assignments and Exercises

• All assignments and exercises are posted here, with their due dates.
• Solutions to the assignments must be send in by the due date, and count for the final grade.
  Excercises are for you to gain experience with key concepts and need not be handed in.
• Solutions to the assignments and exercises are not posted here, but only discussed in class.