Kies de Nederlandse taal
Course module: 192135320
Modeling and Analysis of Concurrent Systems 2
Course info
Course module192135320
Credits (ECTS)5
Course typeCourse
Language of instructionEnglish
Contact personprof.dr. J.C. van de Pol
Contactperson for the course
prof.dr. J.C. van de Pol
prof.dr. J.C. van de Pol
Academic year2016
Starting block
Application procedureYou apply via OSIRIS Student
Registration using OSIRISYes
Learning goals
To understand the machinery of state-of-the-art model checkers.
"Looking under the hood of model checkers".

The central theme of this course is model checking algorithms for the automated analysis of concurrent software. Besides the basic algorithmic principles, considerable attention will be devoted to optimization techniques that make model checking a verification approach of industrial relevance. 
The objective of the course is to understand the algorithms for model checking and to be able to design and implement model checkers in an efficient way. The course will focus on the following areas of model checking:
  1. Symbolic model checking. We will discuss Binary Decision Diagrams (BDDs), a popular datastructure to store a set of states. The BDD operations needed for model checking will be discussed.
  2. Algorithms and implemenation techniques for model checking, like partial order reduction, state compression and bit state hashing.
  3. Distributed and multi-core model checking. To scale model checking even further, one can use a cluster of computers for model checking. Several techniques to parallelize algorithms for model checking will be discussed.

Besides the lectures that explain the theory of the model checking algorithms, a large part of the course is devoted to a practical project, where the students will design and implement an actual model checker.

The student must also present a research paper on one of the course topics.

model checking algorithms, LTL, partial order reduction, (bitstate) hashing, symbolic model checking, BDDs, distributed model checking.
Assumed previous knowledge
Voorkennis noodzakelijk: Vertalerbouw (192110352),Algorithms, Datastructures and Complextiy (192140200); Gewenst: System Validation (192140122), Formele Methoden voor Software Engineering(192135201)
Required materials
Course material
Handouts and research papers will be distributed via Blackboard
Recommended materials
Instructional modes



Exam + practical assignm. + presentation

Test weight: exam 2/5, assignment 2/5, presentation 1/5; the exam must be sufficient

Kies de Nederlandse taal