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 software systems. 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:

Assignments:
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%.
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.

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 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:

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.
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.

Lectures

Assignments and Exercises

Exercises

  • by January 6, 2015:

    Assignments

    Will be posted on the Piazza course website.

    Instructor

    Teaching Assistant

    Course Websites

    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