Stud.IP Uni Oldenburg
University of Oldenburg
04.12.2021 02:31:25
inf455 - Model Checking (Complete module description)
Original version English Download as PDF
Module label Model Checking
Module code inf455
Credit points 6.0 KP
Workload 180 h
Institute directory Department of Computing Science
Applicability of the module
  • Master's Programme Computing Science (Master) > Theoretische Informatik
Responsible persons
Wehrheim, Heike (Module responsibility)
Lehrenden, Die im Modul (Module responsibility)
Skills to be acquired in this module
Model checking is a technique for the automatic verification of hardware and software systems. In the course, the students develop knowledge and skills  in requirements specification via temporal logic and the automatic algorithmic checking of systems with respect to requirements.

**Professional competence**
The students:
- name the operators in temporal logics and the differences between linear-time and branching-time logics, - specify requirements in LTL and CTL,
- translate LTL formulae to Büchi automata,
- construct BDDs for boolean functions,
- describe CTL formulae in fixpoint form,
- apply model checking algorithms to Kripke structures,

- know the expressivity of bisimulation

**Methodogical competence**
The students:
- apply formal modelling techniques,
- prove properties of temporal logics,

- use model checking tools for the verification of systems.  

**Social competence**
The students:
- work on tasks in groups and discuss solutions,

- develop system descriptions in groups and interpret results of tools.

- organize their own work for the course.
Module contents
  • temporal logics LTL and CTL
  • Büchi automata
  • explicit model checking
  • Binary decision diagrams
  • Lattices, fixpoints, CTL as transformers
  • Symbolic model checking
  • bisimulation
Reader's advisory

Christel Baier, Joost-Pieter Katoen: Principles of Model Checking, MIT Press

E. M. Clarke, Orna Grumberg, Doron Peled: Model Checking, MIT Press
Languages of instruction German, English
Duration (semesters) 1 Semester
Module frequency
Module capacity unlimited
Reference text
Useful previous knowledge: Logic
Modullevel / module level MM (Mastermodul / Master module)
Modulart / typ of module Wahlpflicht / Elective
Lehr-/Lernform / Teaching/Learning method
Vorkenntnisse / Previous knowledge
Course type Comment SWS Frequency Workload of compulsory attendance
2 SoSe oder WiSe 28
2 SoSe oder WiSe 28
Total time of attendance for the module 56 h
Examination Time of examination Type of examination
Final exam of module
Weekly homework assignments, lab assignments in a block, oral examination at the end