Logic Model Checking, Caltech 2017, Winter Term


Course Material CS 118, TThu, 1:00-2: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 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 widely used logic model checker Spin. The course also covers model-extraction and swarm-based 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 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.

Assignments:
A fair amount of self-paced work with the Spin model checker is expected. Grading is based on 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 tractable.

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 linux-compatible systems are recommended), plus some additional course-specific 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. Fine-tune your model building, abstraction, and verification skills by creating lots of small example verification models. Self-paced work is expected throughout the course.

Lectures

Recommended Exercises

Assignment Schedule

All assignments are posted on the Piazza website.

Instructor

Teaching Assistant

Course Website

Background material

Course Textbook

Required:

Optional:

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 follow-up to CS118:

Spin homepage