Logic Model Checking, Caltech 2017, Winter Term
Course Material CS 118, TThu, 1:002:25pm, 106 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 systems
and multithreaded software.
The focus is on the automatatheoretic verification
method, the formalization of properties in linear temporal logic, and the use
of the widely used logic model checker Spin.
The course also covers modelextraction and
swarmbased verification techniques using cloud computing.
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 one of the final two assignments, with approval from the instructor.
Similarly, you may suggest to build a nontrivial component of an alternative
prototype verification system that will be provided.
There will 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%.
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 that your submission is late.
This means that 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
Examples of assignments and model checking applications are discussed
in class, so you are strongly encouraged to attend all lectures.
It is possible that some assignments will be done
in class, which can gain you additional credits towards the final grade.
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 or linuxcompatible systems are recommended),
plus some additional coursespecific tools
(such as tau and buzz).
We will discuss the formal specification language in the early lectures,
but you are encouraged to look at examples, read the textbook, and
to become familiar with the online manual pages at:
Throughout the course you are encouraged to
experiment on your own to learn in more detail about
concepts covered in the lectures, and to ask questions based on these experiments.
Finetune your model building, abstraction, and verification skills by
creating lots of small example verification models.
Selfpaced work is expected throughout the course.
Lectures
 You are encouraged to attend all lectures, ask questions, and start discussions.
 The first lecture was Thursday January 5; the last will be Tuesday March 9.
 Excerpts from some lectures are posted on Piazza (send an email if you're
registed but didn't receive an invite yet)
Recommended Exercises
 Install the most recent version of Spin on your system (6.4.6).
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.
 Optionally: install the Tau tool, available from spinroot homepage.
Assignment Schedule
 by January 17, 2017:
 Read at least upto Chapter 3 in the course textbook.
 Complete exercises 1a through 1h from:
exercises
(selfpaced; no need to submit)
 Assignment 1, is due no later than noon Jan 19
 Assignment 2. is posted Jan 19, and due noon Jan 26
 Assignment 3. is posted Jan 26, and due noon Feb 2
 Assignment 4. is posted Feb 2, and due noon Feb 9
 Assignment 5. is posted Feb 9, and due noon Feb 16
 Assignment 6. is posted Feb 16, and due noon Feb 23
 Assignment 7. is posted Feb 23, and due noon March 10
Solutions to assignments will be discussed in class, once all
solutions have been received.
They will not be posted online.
Instructor
 Gerard Holzmann, gholzmann [at] acm.org
Teaching Assistant
 Sumanth Dathathri
office hours Tuesdays 57pm, SFL 229, on weeks when homework is due.
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:
Related Course
The following course is recommended as either a prelude to or followup to CS118:
 CS116, Reasoning about program correctness.
Lecturer: Rajeev Joshi (JPL/LaRS).
Spin homepage