Prospectus

nl en

Advances in Model Checking

Course
2019-2020

Admission requirements

Recommended prior knowledge

Students are assumed to have knowledge of mathematics and 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

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 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.

  • 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 and various reduction techniques, such as, Partial Order Reduction

  • Temporal logics for specifying the behavior of reactive systems

  • Parallel model checking (this lecture is more or less orthogonal and might be dropped)

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 (optional).

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 and data structures

Since the lab computers are not available during the COVID-19 crisis, the lab assignments are optional. Students should focus on the homework assignments instead.

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.
    These lectures will be provided online in a non-interactive setting (as video recording). Feedback and questions can be entered via the blackboard Q&A forum. Upon popular demand, we will organize an interactive session to discuss lectures, homework or lab assignments.

  • 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. These practical lab assignments are optional.

  • 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: 98:00 hrs.

Assessment method

  • The final grade is based on individual projects. Retake will be an oral exam.

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.
Skype: live:alfonslaarman

Remarks

The course is open to first- and second-year master students of all programmes of Mathematics and Computer Science.