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 the software or hardware of a digital system can cause us to miss an appointment or have to retype a text. But in the worst case, our lives can depend on the correctness of the system. Examples of such mission-critical systems are: traffic lights, automated breaking systems in cars, autonomous vehicles, autopilots, and guidence systems in rockets. Therefore, various methods have been developed for verifying the correctness of software and hardware. These methods go beyond mere testing by proving not only the presence but also the absence of bugs.
This course mainly focuses on a software / hardware verification technique called model checking. Model Checking is a Turing-award winning approach for proving program correctness fully automatically. A model checker is a tool that takes another program as input together with a specification of its intended behavior. The model checker then proves correctness by exhaustively exploring the program’s behavior, i.e., its state space, and ‘checking’ that it conforms to the intended behavior, as defined in the specification.
The power of model checking crucially depends 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 the program data (the variables in the program) and the amount of parallelism (the number of threads / processes in the program). Nevertheless, extremely large state spaces can be handled by the state-of-the-art technologies based on compression, partial-order reduction, symbolic data structures and parallelism. In the course, you will study both the theory and practice of these technologies.
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 that exploit parallel program semantics, such as, Partial Order Reduction
Parallel model checking algorithms
Course objectives
The first objective is to introduce the student to the formal underpinnings of model checking. The second objective is to learn to implement the different techniques (algorithms, data structures and symbolic approaches) developed for model checking large systems.
In this second objective, the student will implement their own model checker from scrath, using an incremental approach.
At the end of the course, students are able to:
Implement a program and its scheduling semantics in a next-state function in order to verify its correctness with a model checker
Implement the relevant (search) algorithms in order to create their own model checker
Implement data structures and reduction techniques to combat the state explosion problem
Encode program semantics in BDDs and SAT/SMT in order to implement symbolic model checkers
Timetable
The most recent timetable can be found at the Computer Science (MSc) student website.
In MyTimetable, you can find all course and programme schedules, allowing you to create your personal timetable. Activities for which you have enrolled via MyStudyMap will automatically appear in your timetable.
Additionally, you can easily link MyTimetable to a calendar app on your phone, and schedule changes will be automatically updated in your calendar. You can also choose to receive email notifications about schedule changes. You can enable notifications in Settings after logging in.
Questions? Watch the video, read the instructions, or contact the ISSC helpdesk.
Note: Joint Degree students from Leiden/Delft need to combine information from both the Leiden and Delft MyTimetables to see a complete schedule. This video explains how to do it.
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.
Reading list
Baier, C., & Katoen, J. P. (2008). Principles of model checking. MIT press.
Additional materials will be distributed during the course.
Registration
As a student, you are responsible for enrolling on time through MyStudyMap.
In this short video, you can see step-by-step how to enrol for courses in MyStudyMap.
Extensive information about the operation of MyStudyMap can be found here.
There are two enrolment periods per year:
Enrolment for the fall opens in July
Enrolment for the spring opens in December
See this page for more information about deadlines and enrolling for courses and exams.
Note:
It is mandatory to enrol for all activities of a course that you are going to follow.
Your enrolment is only complete when you submit your course planning in the ‘Ready for enrolment’ tab by clicking ‘Send’.
Not being enrolled for an exam/resit means that you are not allowed to participate in the exam/resit.
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.
Software
Starting from the 2024/2025 academic year, the Faculty of Science will use the software distribution platform Academic Software. Through this platform, you can access the software needed for specific courses in your studies. For some software, your laptop must meet certain system requirements, which will be specified with the software. It is important to install the software before the start of the course. More information about the laptop requirements can be found on the student website.