FI:IA169 Model Checking - Informace o předmětu

IA169 Model Checking

Předmět se v období jaro 2025 nevypisuje.

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

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: 0/130, pouze zareg.: 2/130, pouze zareg. s předností (mateřské obory): 0/130

Mateřské obory/plány

• Analýza a zpracování obrazu (program FI, N-VIZ)
• Bioinformatika a systémová biologie (program FI, N-UIZD)
• Computer Games Development (program FI, N-VIZ_A)
• Computer Graphics and Visualisation (program FI, N-VIZ_A)
• Computer Networks and Communications (program FI, N-PSKB_A)
• Cybersecurity Management (program FI, N-RSSS_A)
• Diskrétní algoritmy a modely (program FI, N-TEI)
• Formální analýza počítačových systémů (program FI, N-TEI)
• Grafický design (program FI, N-VIZ)
• Graphic Design (program FI, N-VIZ_A)
• Hardware Systems (program FI, N-PSKB_A)
• Hardwarové systémy (program FI, N-PSKB)
• Image Processing and Analysis (program FI, N-VIZ_A)
• Informační bezpečnost (program FI, N-PSKB)
• Information Security (program FI, N-PSKB_A)
• Kvantové a jiné neklasické výpočetní modely (program FI, N-TEI)
• Počítačová grafika a vizualizace (program FI, N-VIZ)
• Počítačové sítě a komunikace (program FI, N-PSKB)
• Principy programovacích jazyků (program FI, N-TEI)
• Řízení kyberbezpečnosti (program FI, N-RSSS)
• Řízení vývoje služeb (program FI, N-RSSS)
• Řízení vývoje softwarových systémů (program FI, N-RSSS)
• Services Development Management (program FI, N-RSSS_A)
• Software Systems Development Management (program FI, N-RSSS_A)
• Software Systems (program FI, N-PSKB_A)
• Softwarové systémy (program FI, N-PSKB)
• Strojové učení a umělá inteligence (program FI, N-UIZD)
• Vývoj počítačových her (program FI, N-VIZ)
• Zpracování a analýza rozsáhlých dat (program FI, N-UIZD)
• Zpracování přirozeného jazyka (program FI, N-UIZD)

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ě.
Výuka probíhá každý týden.

• Statistika zápisu (jaro 2025, nejnovější)
  
• Permalink: https://is.muni.cz/predmet/fi/jaro2025/IA169