Logic Model Checking, Caltech 2018-19, Winter Term
Course Material CS 118, TThu, 1:00-2: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 multi-threaded software.
The focus is on the automata-theoretic 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 model-extraction
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,
omega-regular 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 automata-theoretic verification, and the
direction in which the research in this area is evolving. At that point
you will also be able to tackle complex real-world verification problems for
software systems involving concurrency.
Course materials, including assignments and additional tools, will be posted on Piazza.
If you're registered for the class, you'll receive an invitation to join.
A fair amount of self-paced work
with the Spin and Buzz model checkers and related tools (e.g., Tau and iSpin,
and possibly also Modex), is expected.
Grading is based on in-class quizzes and take-home assignments, some of which
require the correct formalization of problem statements and
the identification of logic abstractions that can render tool-based
formal verification feasible and 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 non-trivial components of alternative verification systems.
- The first lecture is Tuesday January 8; the last will be Tuesday March 12.
- Additional materials are posted on Piazza.
- You are expected to attend all lectures, ask questions, start discussions, suggest problems.
- Part of the course credit is based on your class participation.
- Install the most recent version of Spin on your system (6.4.9).
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 test-cases 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
- Gerard J. Holzmann, gholzmann [at] acm.org, homepage
- Tung M. Phan, tmphan [at] caltech.edu.
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: