Inhalt
[ 921COENMCHK13 ] KV Model Checking
|
|
|
|
 |
| Workload |
Ausbildungslevel |
Studienfachbereich |
VerantwortlicheR |
Semesterstunden |
Anbietende Uni |
| 4,5 ECTS |
M1 - Master 1. Jahr |
Informatik |
Armin Biere |
3 SSt |
Johannes Kepler Universität Linz |
|
|
|
| Detailinformationen |
| Quellcurriculum |
Masterstudium Computer Science 2021S |
| Ziele |
Command of algorithms and data structures to analyze state-based formal models and their implementation.
|
| Lehrinhalte |
- 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).
|
| Beurteilungskriterien |
Written exam plus regular lab assignments
|
| Lehrmethoden |
Slide presentation with case studies on the blackboard
|
| Abhaltungssprache |
Englisch |
| Literatur |
Handbook of Model Checking, Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, Roderick Bloem editors, Springer 2018.
Model Checking (2nd edition). E. Clarke, O. Grumberg, D. Kröning, D. Peled, H. Veith. MIT press, 2018.
|
| Lehrinhalte wechselnd? |
Nein |
| Sonstige Informationen |
http://fmv.jku.at/mc
|
| Äquivalenzen |
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)
|
|
|
|
| Präsenzlehrveranstaltung |
| Teilungsziffer |
- |
| Zuteilungsverfahren |
Direktzuteilung |
|
|
|
