Logic Model Checking, Caltech 2013, Winter Term

Course Material CS 118, TThu, 1:00-2:25pm, 314 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. The course also covers automated model-extraction and swarm-based verification techniques using grid networks, the cloud, and standard multi-core machines.

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 that point you should be able to handle significant real-world software verification problems, especially of systems involving concurrency.

Assignments:
There are seven take-home assignment, roughly one per week, and especially in the beginning a fair amount of self-paced work with Spin is expected. Some of the assignments will require significant effort, formalizing problems and finding abstractions to make verification tractable.

• All assignments require individual work (there are no team assignments).
• Don't plan on being able to to complete assignments in a single late-night session, the day before it is due.
• You are allowed to suggest a challenging verification task yourself, to replace the final two assignments
  (prior instructor approval required of course).

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:
At the start of the course you are expected to download and install the latest version of Spin model checker on your preferred system (linux recommended). Throughout the course you are further expected to take the initiative to experiment on your own with the tool to learn in more detail about concepts explained in the lectures, and to ask questions based on these experiments.
You are strongly encouraged to try small examples to develop and fine-tune your model building, abstraction, and verification skills, and to develop insight in the verification strategies that are typically used with logic model checkers. Self-paced work is expected throughout the course.

Lectures

• You are strongly encouraged to attend all the lectures, to ask questions, to start discussions.
• The first lecture is Tuesday January 8; the last one will be Tuesday March 12.
• No lecture Tuesday February 12.

Assignments and Exercises

• All assignments and exercises will be posted here, with their due dates (but no lecture notes).
• Solutions to the assignments must be send in by the due date, to count for the final grade.
  The recommended excercises are for you to gain experience with key concepts and need not be handed in.
• Solutions to the assignments and exercises are discussed only in class, once all responses have been received.

Exercises