Logic Model Checking, Caltech 201819, Winter Term
Course Material CS 118, TThu, 1:002:25pm, 106 Annenberg
Logic Model Checking
An introduction to the theory and practice of logic model
checking as an aid in the formal verification of concurrent or distributed systems,
and specifically of multithreaded software.
The focus is on the automatatheoretic verification
method, the formalization of properties in linear temporal logic, and the use
of the popular logic model checker Spin.
Towards the end of the course we will also cover modelextraction
techniques and the use of cloud computing in formal verification.
The course covers a broad range of fundamental computer science topics,
including the use of hashing, search methods, graph theory, automata theory,
nondeterminism,
omegaregular properties, concurrent algorithms, storage methods, Bloom filters,
the use of logic, user interfaces, language design, parsers, etc.
At the end of the course you should have a good insight into the
theory of logic model checking based on automatatheoretic verification, and the
direction in which the research in this area is evolving. At that point
you will also be able to tackle complex realworld verification problems for
software systems involving concurrency.
Course materials, including assignments and additional tools, will be posted on Piazza.
Assignments:
A fair amount of selfpaced work
with the Spin model checker is expected.
Grading is based on takehome assignments, some of which
require the correct formalization of problem statements and
the identification of logic abstractions that can render toolbased
formal verification tractable.

All assignments require individual work.

You may suggest a challenging formal verification task
to replace any assignment.
Similarly, you may suggest to design and build nontrivial components of alternative verification systems.
 The first lecture is Tuesday January 8; the last will be Tuesday March 12.
 Additional materials will be posted on Piazza.
Lectures
 You are expected to attend all lectures, ask questions, start discussions, suggest problems.
Recommended Preparation
 Install the most recent version of Spin on your system (6.4.8).
Download the full source distribution,
compile it (requires gcc or equivalent) and
install it on your system. Make sure you can compile the code correctly. Try
the testcases from the Spin/Test directory to make sure.
 Download and install iSpin, the Spin GUI.
(To use the GUI, you must have a current version of
tcl/tk and graphiz/dot installed on your system).
In case of problems, follow the online
instructions.
Instructor
 Gerard J. Holzmann, gholzmann [at] acm.org, homepage
Teaching Assistant
 Tung M. Phan, tmphan [at] caltech.edu, office hours tbd.
Course Website
Background material
Course Textbook
Required:
Optional:

Principles of Spin,
Moti BenAri, Springer Verlag, Jan. 2008.

Principles of Model Checking,
Cristel Baier, JoostPieter Katoen, Kim Larsen, MIT Press, May 2008.

Principles of concurrent and Distributed Programming,
Moti BenAri, AddisonWesley, 2006, 2nd Edition, based on Spin.

Model Checking,
Ed Clarke, Orna Grumberg, and Doron Peled. MIT Press, 1999.

Systems and Software Verification: ModelChecking 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, AddisonWesley, 2000.

Verification of reactive systems,
Klaus Schneider, SpringerVerlag 2004.

Formale Modelle der Softwareentwicklung (in German),
Stephan Kleuker, ViewegTeubner Verlag, 2009.
Covering Spin, Uppaal, and Petri Nets.
For more on mutual exclusion algorithms, and design of distributed algorithms
in general, consider also:
Spin homepage