Inhalt

[ 921COENMCHK13 ] KV Model Checking

Versionsauswahl
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