Semester: winter 2023/24
Lectures: Wednesday, 10:40, S10 (Jan Kofroň)
Labs: Thursday, 9:00, S7 (Jan Kofroň)
Page in SIS: NSWI101
Grading: Credit and exam

Previous year: 2022/23

News

Lectures

Date Title Downloads
04. 10. 2023 Introduction, LTS, Process Algebras Slides
11. 10. 2023 Model Checking Slides
18. 10. 2023 Spin Model Checker Slides
25. 10. 2023 Computational Tree Logic Slides
01. 11. 2023 OBDD, Lattices, Fixpoints Slides
08. 11. 2023 Symbolic CTL Model Checking Slides
15. 11. 2023 Timed Automata Slides
22. 11. 2023 Bounded Model Checking, Infinite-State Model Checking, Compositional Reasoning Slides
29. 11. 2023 Abstractions and Symmetries Slides
6. 12. 2023 Stochastic Model Checking Slides
13. 12. 2023 Unbounded Model Checking Slides
20. 12. 2023 Counter-Example Guided Abstraction Refinement Slides

Labs

Date Title Downloads
12. 10. 2023 LTS, Process algebra Slides
19. 10. 2023 Spin Exercises ABP models
26. 10. 2023 Spin Exercises ModelsSlides
09. 11. 2023 More Spin Exercises Dekker's algorithmSlides
16. 11. 2023 UPPAAL and CTL Exercises SlidesProducer-consumer example
23. 11. 2023 NuXMV and OBDD Exercises SlidesModels
07. 12. 2023 NuXMV Exercises Models

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

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.

Grading

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

References