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


Date Title Downloads


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: