CloseHelpPrint
Kies de Nederlandse taal
Course module: 192135320
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
E-mailj.c.vandepol@utwente.nl
Lecturer(s)
Contactperson for the course
prof.dr. J.C. van de Pol
Lecturer
prof.dr. J.C. van de Pol
Academic year2016
Starting block
2B
Application procedureYou apply via OSIRIS Student
Registration using OSIRISYes
Learning goals
To understand the machinery of state-of-the-art model checkers.
Content
"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.

Content
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)
PARTICIPATING STUDY
M-CSC
Required materials
Course material
Handouts and research papers will be distributed via Blackboard
Recommended materials
-
Instructional modes
Lecture

Project

Tutorial

Tests
Exam + practical assignm. + presentation

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

CloseHelpPrint
Kies de Nederlandse taal