IA169 Model Checking

Fakulta informatiky
jaro 2026
Rozsah
2/1/0. 3 kr. (plus ukončení). Ukončení: zk.
Vyučováno kontaktně
Vyučující
prof. RNDr. Jan Strejček, Ph.D. (přednášející)
RNDr. Martin Jonáš, Ph.D. (cvičící)
Garance
prof. RNDr. Jan Strejček, Ph.D.
Katedra teorie programování – Fakulta informatiky
Dodavatelské pracoviště: Katedra teorie programování – Fakulta informatiky
Rozvrh
Út 17. 2. až Út 12. 5. Út 12:00–13:50 A319
  • Rozvrh seminárních/paralelních skupin:
IA169/01: St 18. 2. až St 13. 5. každou sudou středu 12:00–13:50 A319, M. Jonáš
Předpoklady
Some degree of abstract math reasoning.
Omezení zápisu do předmětu
Předmět je nabízen i studentům mimo mateřské obory.
Předmět si smí zapsat nejvýše 130 stud.
Momentální stav registrace a zápisu: zapsáno: 12/130, pouze zareg.: 0/130, pouze zareg. s předností (mateřské obory): 0/130
Mateřské obory/plány
předmět má 32 mateřských oborů, zobrazit
Anotace
The student will understand the fundamental and currently used model checking algorithms and techniques (except those primarily designed for software). Further, the student will be able to read and write specifications in LTL and CTL, and use relevant formalisms like Büchi automata and binary decision diagrams.
Výstupy z učení
Students will:
understand traditional model checking algorithms (LTL and CTL model checking) and current approaches (bounded model checking, k-induction, CEGAR, property-driven reachability);
be able to read and write specifications in LTL and CTL;
be aware of potential applications and inherent limitations of model checking algorithms.
Klíčová témata
  • Overview of the model checking area.
  • Kripke structure, labelled transition system, LTL, CTL, Büchi automata.
  • Automata-based LTL model checking.
  • CTL model checking.
  • Bounded model checking and k-induction.
  • Reachability in pushdown systems.
  • Abstraction and CEGAR.
  • Property directed reachability.
Studijní zdroje a literatura
  • CLARKE, E. M.; Orna GRUMBERG; Doron PELED; Daniel KROENING a Helmut VEITH. Model checking. Second edition. Cambridge, Massachusetts: MIT Press, 2018, xx, 402. ISBN 9780262038836. info
  • Handbook of model checking. Edited by E. M. Clarke - T. A. Henzinger - Helmut Veith - Roderick Bloem. Cham: Springer International Publishing AG, 2018, xxiv, 1210. ISBN 9783319105741. info
Přístupy, postupy a metody používané ve výuce
lectures, seminars
Způsob ověření výstupů z učení a požadavky na ukončení
oral exam
Vyučovací jazyk
Angličtina
Další komentáře
Předmět je vyučován každoročně.
Předmět je zařazen také v obdobích jaro 2016, jaro 2017, jaro 2018, jaro 2019, podzim 2019, podzim 2020, podzim 2021, podzim 2022, jaro 2024.
  • Statistika zápisu (nejnovější)
  • Permalink: https://is.muni.cz/predmet/fi/jaro2026/IA169