[ 921COENMCHV21 ] VL Model Checking

Workload Education level Study areas Responsible person Hours per week Coordinating university
3 ECTS M1 - Master's programme 1. year Computer Science Martina Seidl 2 hpw Johannes Kepler University Linz
Detailed information
Original study plan Master's programme Computer Science 2022W
Objectives The students understand the fundamental concepts of explicit and symbolic model checking techniques and know how to apply them for verification tasks. They are familiar with the algorithmic aspects of explicit model checking and are able to implement basic model checking approaches.
  • formal models in computer science
  • finite state machines
  • equivalence checking
  • conformance checking
  • predicate abstraction
  • (bi-)simulation
  • automata minimization
  • explicit vs. symbolic representation of systems
  • reachability analysis
  • optimizing search with hashing
  • partial order reduction
  • liveness and fairness
  • combinatorial logic
  • AIGs
  • BDDs
Criteria for evaluation Exam plus practical projects (together with exercise class).
Methods Slide-based presentation, tool demos, practical exercises.
Language English
Study material Slides. Handbook of Model Checking, Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, Roderick Bloem editors, Springer 2018.
Changing subject? No
Further information
Corresponding lecture in collaboration with 921COENMCHK21: UE Model Checking (1.5 ECTS) equivalent to
921COENMCHK13: KV Model Checking (4.5 ECTS)
On-site course
Maximum number of participants -
Assignment procedure Direct assignment