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 specific 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 grid networks, the cloud, and standard multi-core machines.
At the end of the course you should have a good fundamental 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 should be able to handle significant real-world software verification problems, especially of systems involving concurrency.
Assignments:
There are seven take-home assignment, roughly one per week, and especially
in the beginning a fair amount of self-paced work with Spin is expected.
Some of the assignments will require significant effort, formalizing
problems and finding abstractions to make 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 during each lecture, so you are strongly encouraged to attend in person. It is possible that some assignments are done only in class this year, 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: