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, non-determinism, 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.

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.

Lectures

Recommended Preparation

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:


Spin homepage