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.
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), 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:
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: