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.
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.
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 = CExamples 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).
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.
You are strongly encouraged to try small
examples 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.
Optional:
For more on mutual exclusion algorithms, and design of distributed algorithms in general, consider also:
The following course is recommended as either a prelude to or follow-up to CS118: