Semester: winter 2021/22
Lectures: Wednesday, 10:40, S1 (Jan KofroňFrantišek Plášil)
Labs: Wednesday, 12:20, S8 (Jan Kofroň)
Page in SIS: NSWI101
Grading: Credit and exam

Previous year: 2020/21



Date Title Downloads
29. 09. 2021 LTS, Process Algebras lecture01.pdfrecording
06. 10. 2021 Kripke Structure, Model Checking, LTL lecture02.pdf
13. 10. 2021 LTL Explicit Model Checking Algorithm lecture03.pdfrecording
20. 10. 2021 CTL, explicit CTL model checking lecture04.pdf
27. 10. 2021 Binary Decision Diagrams, Lattices, Fixpoints lecture05.pdfrecording
03. 11. 2021 Symbolic CTL Model Checking, Partial Order Reduction lecture06.pdfrecording
10. 11. 2021 Timed Automata lecture07.pdfrecording
24. 11. 2021 Infinte/Bounded Model Checking, Compositional Reasoning lecture08.pdfrecording
01. 12. 2021 Abstractions, Symmetries lecture09.pdfrecording


Date Title Downloads
06. 10. 2021 Spin spin.pdfrecording
13. 10. 2021 Spin Exercises
20. 10. 2021 Spin Exercises II
27. 10. 2021 Spin Exercises III
03. 11. 2021 CTL Model Checking, OBDD Exercises lab05.pdf
24. 11. 2021 NuXMV lab07.pdflab07.ziprecording
01. 12. 2021 NuXMV Exercises


Basic concepts of behavior description of parallel and distributed systems. Equivalence checking and model checking — techniques and tools.



The purpose of the lab is to provide students with a hand-on experience with verification tools (SPIN, SMV, UPPAAL), higher-level behavior specification languages (process algebra, behavior protocols), and temporal logics (LTL, CTL).

There will be two assignments (one taking approximately 8 hours of homework, the other an hour). The homeworks are to be submitted via e-mail:

Note: 10% of your score will be deduced for every calendar day your assignment is late. This implies that no assignment will be accepted after 10 calendar days past its due date.


Final grades will be determined by the quality of homework and the result of the final exam in the following ratio: