Inhalt
[ 921COENMCHU21 ] UE Model Checking
|
|
|
| Es ist eine neuere Version 2022W dieser LV im Curriculum Master's programme Business Informatics 2024W vorhanden. |
|
 |
| 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 2021S |
| 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 |
http://fmv.jku.at/mc
|
| 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 |
|
|
|
