IA169 Model Checking

Fakulta informatiky
jaro 2024
Rozsah
2/1/0. 3 kr. (plus ukončení). Ukončení: zk.
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
Po 19. 2. až Čt 9. 5. Čt 16:00–17:50 A318
  • Rozvrh seminárních/paralelních skupin:
IA169/01: Po 19. 2. až Čt 9. 5. každý sudý čtvrtek 18:00–19:50 A318, 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: 13/130, pouze zareg.: 0/130, pouze zareg. s předností (mateřské obory): 0/130
Mateřské obory/plány
předmět má 33 mateřských oborů, zobrazit
Cíle předmětu
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.
Osnova
  • 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.
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
Výukové metody
lectures, seminars
Metody hodnocení
oral exam
Vyučovací jazyk
Angličtina
Další komentáře
Studijní materiály
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.
  • Statistika zápisu (nejnovější)
  • Permalink: https://is.muni.cz/predmet/fi/jaro2024/IA169