Admission requirements
Recommended prior knowledge
Students are assumed to have knowledge of computer science at a BSc level (logics, algorithmics and data structures) and basic programming skills (in any programming language). A BSc level course on verification or testing is recommended background knowledge (e.g. Programmeren & Correctheid, Theory of Concurrency).
Description
Digital systems have become so ubiquitous, that many of our daily activities depend on them. A glitch in a system can cause us to miss an appointment or have to retype a text. But in the worst case, our lives can also depend on the correctness of the system. Examples of such critical systems are: traffic lights, automated breaking systems in cars, autonomous vehicles, autopilots, and guidence systems in rockets. Therefore, various ways have been developed for guaranteeing the correctness of software and hardware. In this course, we mainly focus on model checking.
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. Even for a finite-state program (without recursion and memory allocation) the state space is exponential in both its data (the variables in the program) and its parallelism (number of threads / processes). Nevertheless, extremely large state spaces can be handled by the state-of-the-art technologies, which we will study in theory and practice.
The course follows the textbook Principles of Model Checking by Christel Baier and Joost-Pieter Katoen for the formal underpinning of model checking, i.e.:
Formalisms for speciying software and hardware systems
Temporal logics for specifying the behavior of reactive systems
Model-theoretic methods to verify that a system description adheres to its specification
Furthermore, the course puts an emphasis on algorithms and data structures for handling large state spaces. For this purpose, additional reading materials and lab exercises are provided. These techniques include:
Symbolic model checking with Binary Decision Diagrams (BDDs)
Symbolic model checking with SAT/SMT (Bounded Model Checking and Property Directed Reachability)
Enumerative model checking with state compression
State space reduction techniques, such as, Partial Order Reduction
Parallel model checking
Course objectives
The main objective is to introduce the student to the formal underpinnings of model checking. The secondary objectives are to learn the different techniques (algorithms, data structures and symbolic approaches) developed for model checking large systems and to implement them in a model checker.
Using an incremental approach, the student will learn how to implement a model checker from scratch. Sub-objectives include:
Implementing program and scheduler semantics in a next-state function
Encoding program semantics in BDDs and SAT/SMT
Implementing relevant (search) algorithms, data structures and reduction techniques
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 techniques discussed in a model checking framework. This framework hides all uninteresting details of a model checker, so the student can focus on core algorithms and data structures.
The student will receive a series of home work exercises that can be completed alone or in groups of two.
Course load
Total hours of study: 168 hrs. (= 6 EC)
Lectures: 30:00 hrs.
Labs: 40:00 hrs.
Examination: 4:00 hrs.
Self-study: 94:00 hrs.
Assessment method
One exam (75%)
Practical exercises (25%)
The teacher will inform the students how the inspection of and follow-up discussion of the exams will take place.
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 Brightspace.
Due to limited capacity, external students can only register after consultation with the programme coordinator/study advisor (mailto:mastercs@liacs.leideuniv.nl).
Reading list
Baier, C., & Katoen, J. P. (2008). Principles of model checking. MIT press.
Additional materials will be distributed during the course.
Contact
Lecturer: dr. Alfons Laarman.
Remarks
The course is open to first- and second-year master students of all programmes of Mathematics and Computer Science.