Semester: winter 2020/21
Lectures: Wednesday, 10:40, Zoom (Jan KofroňFrantišek Plášil)
Labs: Monday, 10:40, Zoom (Jan Kofroň)
Page in SIS: NSWI101
Grading: Credit and exam

Previous year: 2019/20

News

Lectures

Date Title Downloads
30. 09. 2020 LTS, Process Algebras lecture01.pdf
05. 10. 2020 The Spin model checker lecture02.pdf
07. 10. 2020 Kripke structures, model checking, LTL lecture03.pdf
14. 10. 2020 LTL explicit model checking lecture04.pdf
21. 10. 2020 CTL, explicit CTL model checking, fairness constraints lecture05.pdf
04. 11. 2020 Ordered binary decision diagrams, fixpoints lecture06.pdf
11. 11. 2020 Symbolic CTL model checking, partial order reduction lecture07.pdf
18. 11. 2020 Timed automata lecture08.pdf
25. 11. 2020 Bounded MC, infinite state MC, compositional reasoning lecture09.pdf
02. 12. 2020 Symetries, abstractions
09. 12. 2020 TLA+
16. 12. 2020 TLA+
06. 01. 2021 Probabilistic model checking

Labs

Date Title Downloads
12. 10. 2020 Spin exercises slidesexamples
19. 10. 2020 Spin exercises II slidesexamples
26. 10. 2020 Spin exercises III examples
02. 11. 2020 CTL model checking slides
09. 11. 2020 OBDD exercises slides
16. 11. 2020 NuXMV system 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 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