Inhalt
[ 921COENMCHK13 ] KV Model Checking
|
|
|
| Es ist eine neuere Version 2021S dieser LV im Curriculum Master's programme Computer Science 2021S vorhanden. |
|
| (*) Unfortunately this information is not available in english. |
 |
| Workload |
Education level |
Study areas |
Responsible person |
Hours per week |
Coordinating university |
| 4,5 ECTS |
M1 - Master's programme 1. year |
Computer Science |
Armin Biere |
3 hpw |
Johannes Kepler University Linz |
|
|
|
| Detailed information |
| Original study plan |
Master's programme Computer Science 2016W |
| Objectives |
The course focuses on understanding algorithms and data structures to analyze state-based formal models and their implementation.
|
| Subject |
Verification vs Synthesis, Simulation of Automata, Abstraction and Refinement, Bisimulation, Automata Minimization, Explicit State Reachability Analysis, State Hashing, Partial Order Reduction, Fair Cycle Detection, Binary Decisions Diagrams (BDDs), And-Inverter Graphs (AIGs).
|
| Criteria for evaluation |
Written exam plus regular lab assignments
|
| Methods |
Slide presentation with case studies on the blackboard
|
| Language |
English |
| Study material |
See web page of the institute and announcements at the start of the semester
|
| Changing subject? |
No |
| Corresponding lecture |
(*)INMIPVOMCHK: VO Model Checking (3 ECTS) + INMIPUEMCHK: UE Model Checking (1,5 ECTS) bzw.
INBVAVOSTH1: VO Systemtheorie 1 (3 ECTS) + INBVAUESTH1: UE Systemtheorie 1 (1,5 ECTS)
|
|
|
|
| On-site course |
| Maximum number of participants |
- |
| Assignment procedure |
Direct assignment |
|
|
|
