[ 921COENMCHU21 ] UE Model Checking

Workload Education level Study areas Responsible person Hours per week Coordinating university
1,5 ECTS M1 - Master's programme 1. year Computer Science Martina Seidl 1 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.
Subject Same as corresponding lecture:

  • 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 lecture).
Methods Student projects.
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 921COENMCHV21: VL Model Checking (3 ECTS) equivalent to
921COENMCHK13: KV Model Checking (4.5 ECTS)
On-site course
Maximum number of participants 35
Assignment procedure Direct assignment