Admission requirements
The course is open to first- and second-year master students of all programs of Mathematics and Computer Science.
The course assumes basic knowledge of mathematics and computer science at the bachelor level.
Knowledge of Logics, Algorithmics and Data Structures on a Bachelor level is mandatory.
A Bachelor-level course on verification or testing is an optional requirement (e.g., Programmeren & Correctheid, Theory of Concurrency, and Testing Object-Oriented Software).
Description
Model Checking is a Turing-Award winning approach for software verification. The method proves program correctness fully automatically, taking only the program itself and a specification of its intended behavior as inputs. The correctness check is done by exhaustively exploring the program’s behavior, i.e., its state space, and ‘checking’ that it conforms to the intended behavior defined in the specification.
The power of model checking depends crucially on the ability to handle large state spaces. In the worst case, the number of states of a given program is exponential in both its data (the variables in the program) and its parallism (number of threads / processes). Nonetheless, extremely large state spaces can be handled by the state-of-the-art technologies that we will study theory and practice:
State compression
Representing states symbolically in Binary Decision Diagrams (BDDs)
Translating the model checking problem to SAT/SMT
Exploring a subset of the program’s parallel behavior using Partial-Order Reduction / Transaction Reduction / Symmetry Reduction
Exploring coarser behavior through abstraction combined with on-demand refinement (CEGAR)
Guiding the abstracted search to the relevant behavior using Property Directed Reachability (PDR/IC3)
Course objectives
Using an incremental approach, the student will learn how to implement a model checker from scratch. Sub-objectives include:
Learn how to realize automatic program verification through model checking
Learn how to handle combinatorial problems using BDDs and SAT/SMT
Learn how to implement relevant algorithms and data structures
Timetable
The most recent timetable can be found at the students' website.
Mode of instruction
The theoretical part consists of a series of lectures about advanced model checking methods.
In the practical part of the course, the student will have the opportunity to implement and extend the discussed techniques in a model checking framework. This framework hides all uninteresting details of a model checker, so we can focus on the core algorithms and data structures used for implementing these techniques.
The student will receive a series of home work exercises that can be completed in groups of two.
Assessment method
1 exam (50%)
1 project based on the home work exercises (50%)
The grade of the project part will depend on both the assessment of the results handed in and an oral assessment at the end of the course.
Registration
You have to sign up for courses and exams (including retakes) in uSis. Check this link for information about how to register for courses.
Please also register for the course in Blackboard.
Due to limited capacity, external students can only register after consultation with the programme coordinator/study advisor (mailto:mastercs@liacs.leideuniv.nl).
Reading list
To be announced.
Contact
Lecturer: dr. Alfons Laarman.