Logic Model Checking, Caltech 2015, 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
The 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 cloud compute principles or
standard multi-core machines.
At the end of the course you should have a good 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. You should also be able
to handle real-world verification problems for software systems involving concurrency.
All course materials, including assignments and additional tools, are posted
on the following Piazza course website:
Especially in the beginning of the course a fair amount of self-paced work
with the Spin model checker is expected.
Grading is based on take-home assignments, some of which will
require significant effort, e.g., to formalize problem statements and
to define abstractions that can make tool-based logic verification tractable.
There are likely to be seven assignments (roughly one per week).
The first five assignments each count for 10% of the final grade;
the last two assignments each count for 25%.
All assignments require individual work.
You are allowed to suggest a challenging verification task yourself,
to replace some or all of the assignments (with instructor approval).
Similarly, you can suggest to build a non-trivial component of a
prototype verification environment that will be discussed in the course.
The maximum score for each assignment is 100 points.
If you send in your solution past the due date/time,
10 points are deducted for every 24 hour period
or part thereof (i.e., at the start of the 10th day late, zero points will 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
Examples of assignments and small model checking applications will be discussed
in the lectures, so you are strongly encouraged to
attend in person. It is possible that some assignments are done only
in class, which can gain you additional credits towards the final grade.
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.
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), plus some additional course-specific tools
(like the tau and buzz tools.
You should become familiar with the Promela specification language by
looking at examples, reading the textbook, and checking online Manual pages
for the language at:
Create lots of small
examples of Tau and Spin models
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.
- You are strongly encouraged to attend all the lectures, to ask questions,
to start discussions.
- The first lecture is Tuesday January 6; the last one will be Tuesday March 10.
- Lecture notes are not posted online.
Assignments and Exercises
- Assignments and exercises will be posted on the Piazza website, with their due dates.
- Solutions to the assignments must be send in by the due date, to count for the final grade.
The recommended excercises listed below 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, and not posted online.
by January 6, 2015:
- Install the most recent Spin version 6.4.3 on your system.
Download the full source distribution,
compile it (you must have gcc or equivalent on you system) and
install it on your system. Make sure you can compile the code correctly. Try
the test-cases from the Spin/Test directory to make sure.
- Install the Tau tool, available from the resources tab on Piazza.
- Install the Spin GUI called iSpin.
(To use the GIUI, you must also have a recent version of
tcl/tk and graphiz/dot installed on your system).
In case of problems, follow the online
Will be posted on the Piazza course website.
- Gerard Holzmann, gholzmann [at] acm.org
Principles of Spin,
Moti Ben-Ari, Springer Verlag, Jan. 2008.
Principles of Model Checking,
Cristel Baier, Joost-Pieter Katoen, Kim Larsen, MIT Press, May 2008.
Principles of concurrent and Distributed Programming,
Moti Ben-Ari, Addison-Wesley, 2006, 2nd Edition, based on Spin.
Ed Clarke, Orna Grumberg, and Doron Peled. MIT Press, 1999.
Systems and Software Verification: Model-Checking Techniques and Tools,
Beatrice Berard, Michel Bidoit, Alain Finkel, et al, Springer Verlag, 2001.
Logic in Computer Science: Modelling and Reasoning about Systems,
Michael Huth and Mark Ryan, Cambridge Univ. Press, 1999.
Introduction to Automata Theory, Languages, and Computation (2nd Edition),
John Hopcroft, Rajeev Motwani, Jeff Ullman, Addison-Wesley, 2000.
Verification of reactive systems,
Klaus Schneider, Springer-Verlag 2004.
Formale Modelle der Softwareentwicklung (in German),
Stephan Kleuker, Vieweg-Teubner Verlag, 2009.
Covering Spin, Uppaal, and Petri Nets.
For more on mutual exclusion algorithms, and design of distributed algorithms
in general, consider also:
The following course is recommended as either a prelude to or follow-up to CS118:
- CS116, Reasoning about program correctness.
Lecturer: Rajeev Joshi (JPL/LaRS).