Máte zapnutý náhled celé osnovy, zpět na běžné zobrazení.
Načítání a prohlížení osnovy může být v závislosti na množství obsahu pomalejší.
Učitel doporučuje studovat od 19. 2. 2024 do 25. 2. 2024.
Učitel doporučuje studovat od 26. 2. 2024 do 17. 3. 2024.
Učitel doporučuje studovat od 18. 3. 2024 do 24. 3. 2024.
Učitel doporučuje studovat od 25. 3. 2024 do 31. 3. 2024.
Učitel doporučuje studovat od 1. 4. 2024 do 7. 4. 2024.
Učitel doporučuje studovat od 15. 4. 2024 do 21. 4. 2024.
Učitel doporučuje studovat od 22. 4. 2024 do 5. 5. 2024.
Učitel doporučuje studovat od 6. 5. 2024 do 12. 5. 2024.
Teaching, Literature, Examination
Teaching
- The lectures take place in A318 every Thursday at 16:00 (except April 11).
- Seminars are also in A318 every second Thursday starting on March 7 at 18:00.
Literature
- E. M. Clarke, O. Grumberg, D. Kroening, D. Peled, and H. Veith: Model Checking (second edition), MIT Press, 2018.
-
E. M. Clarke, T. A. Henzinger, H. Veith, and R. Bloem: Handbook of Model Checking, Springer, 2018.
- Ch. Baier and J.-P. Katoen: Principles of Model Checking, MIT Press, 2008.
Examination
- no intrasemestral tests, no mandatory homeworks
- oral exam at the end
Introduction
Automata-based LTL model checking
CTL model checking
Symbolic model checking for CTL
Slides above do not cover the whole lecture and we used the slides below for the second half. The slidesabove will be evenatually completed and updated to cover the whole lecture.
Bounded model checking and k-induction
Reachability in pushdown systems
The part about LTL model checking is a bonus (not presented and not a subject of the exam). There is a recording from spring 2021:
Abstraction and CEGAR
Chyba: Odkazovaný objekt neexistuje nebo nemáte právo jej číst.
https://is.muni.cz/el/fi/jaro2023/IA159/um/videos/06_abs_part1.m4v
Chyba: Odkazovaný objekt neexistuje nebo nemáte právo jej číst.
https://is.muni.cz/el/fi/jaro2023/IA159/um/videos/06_abs_part2.m4v