To understand the machinery of state-of-the-art model checkers.
"Looking under the hood of model checkers".
The central theme of this course is model checking algorithms for the automated analysis of concurrent software. Besides the basic algorithmic principles, considerable attention will be devoted to optimization techniques that make model checking a verification approach of industrial relevance.
The objective of the course is to understand the algorithms for model checking and to be able to design and implement model checkers in an efficient way. The course will focus on the following areas of model checking:
- Symbolic model checking. We will discuss Binary Decision Diagrams (BDDs), a popular datastructure to store a set of states. The BDD operations needed for model checking will be discussed.
- Algorithms and implemenation techniques for model checking, like partial order reduction, state compression and bit state hashing.
- Distributed and multi-core model checking. To scale model checking even further, one can use a cluster of computers for model checking. Several techniques to parallelize algorithms for model checking will be discussed.
Besides the lectures that explain the theory of the model checking algorithms, a large part of the course is devoted to a practical project, where the students will design and implement an actual model checker.
The student must also present a research paper on one of the course topics.
model checking algorithms, LTL, partial order reduction, (bitstate) hashing, symbolic model checking, BDDs, distributed model checking.
Assumed previous knowledge
|Voorkennis noodzakelijk: Vertalerbouw (192110352),Algorithms, Datastructures and Complextiy (192140200); Gewenst: System Validation (192140122), Formele Methoden voor Software Engineering(192135201)||Required materials|
Recommended materials-Instructional modesTests
|Course materialHandouts and research papers will be distributed via Blackboard|
|Exam + practical assignm. + presentation|
RemarkTest weight: exam 2/5, assignment 2/5, presentation 1/5; the exam must be sufficient