Semester: winter 2025/26
Lectures: Thursday, 12:20, S10 (Jan Kofroň)
Labs: Thursday, 14:00, S10 (Jan Kofroň)
Page in SIS: NSWI101
Grading: Credit and exam

Previous year: 2024/25

News

Lectures

Date Title Downloads
02. 10. 2025 Introduction, LTS, Process Algebras Slides
09. 10. 2025 Model Checking Slides
16. 10. 2025 Spin Slides

Labs

Date Title Downloads
09. 10. 2025 LTS, Process algebra Slides
16. 10. 2025 LTL Exercises Slides

Annotation

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

Syllabus

Lab

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–12 hours of homework, the other an hour). The homeworks are to be submitted via e-mail: nswi101@d3s.mff.cuni.cz

Grading

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

References