Advances in Model Checking

Course description Advances in Model Checking
Year: 2017-2018
Catalog number:
Teacher(s):
  • A.W. Laarman
Language: English
Blackboard: Yes
EC: 6.0
Level: 500
Period: Semester 2
  • No Elective choice
  • No Contractonderwijs
  • No Exchange
  • No Study Abroad
  • No Evening course
  • No A la Carte
  • No Honours Class

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

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.

Course Load

6EC

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.

Blackboard

blackboard

Reading list

Optional literature:
Baier, Christel, Joost-Pieter Katoen, and Kim Guldstrand Larsen. Principles of model checking. MIT press, 2008.

Other literature will be provided during the course.

Contact

Programme Co-ordinator: ms. Riet Derogee

Languages