Semester: winter 2022/23
Lectures: Wednesday, 15:40, S4 (Jan Kofroň)
Labs: Thursday, 10:40, S1 (Jan Kofroň)
Page in SIS: NSWI101
Grading: Credit and exam

Previous year: 2021/22



Date Title Downloads
05. 10. 2022 Introduction, LTS, Process Algebras Slides
12. 10. 2022 Model Checking Slides
19. 10. 2022 Spin Slides
26. 10. 2022 CTL Slides
02. 11. 2022 OBDDs Slides
16. 11. 2022 Symbolic CTL Model Checking Slides
23. 11. 2022 Timed Automata Slides


Date Title Downloads
06. 10. 2022 LTS, Process Algebras lab01.pdf
13. 10. 2022 LTL Exercises lab02.pdf
20. 10. 2022 Spin Exercises lab03.pdfABP examples
27. 10. 2022 More Spin Exercises lab04.pdfCoordinator election
03. 11. 2022 More Spin Exercises lab05.pdfDekker's algorithm
10. 11. 2022 CTL and OBDD Exercises lab06.pdf


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: