 |
| Detailed information |
| Original study plan |
Master's programme Computer Science 2025W |
| Learning Outcomes |
Competences |
| 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.
|
|
| Skills |
Knowledge |
Students can:
- Read and write formal specifications (K2, K3, K4, K5)
- Translate implementations of small software and hardware systems in a representation that can be verified (K2, K3, K4, K5)
- Understand the complexity of verification tasks and the importance of abstraction (K4, K5)
- Write simple (symbolic) encodings (K6)
- Understand and employ verification algorithms (K2, K3, K4, K5)
|
- 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 |
This lecture and the associated exercise course form an inseparable didactic unit. The learning outcomes presented here are achieved through the close interaction of the two courses.
|
| Corresponding lecture |
in collaboration with 921COENMCHK21: UE Model Checking (1.5 ECTS) equivalent to
921COENMCHK13: KV Model Checking (4.5 ECTS)
|
|
