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

News

Lectures

Date Title Downloads
29. 09. 2021 LTS, Process Algebras lecture01.pdfrecording
06. 10. 2021 Kripke Structure, Model Checking, LTL lecture02.pdf
13. 10. 2021 LTL Explicit Model Checking Algorithm lecture03.pdfrecording
20. 10. 2021 CTL, explicit CTL model checking lecture04.pdf
27. 10. 2021 Binary Decision Diagrams, Lattices, Fixpoints lecture05.pdfrecording
03. 11. 2021 Symbolic CTL Model Checking, Partial Order Reduction lecture06.pdfrecording
10. 11. 2021 Timed Automata lecture07.pdfrecording
24. 11. 2021 Infinte/Bounded Model Checking, Compositional Reasoning lecture08.pdfrecording
01. 12. 2021 Abstractions, Symmetries lecture09.pdfrecording
08. 12. 2021 TLA+ lecture10.pdflecture10.zip
15. 12. 2021 TLA+
22. 12. 2021 Stochastic Model Checking lecture12.pdfrecording

Labs

Date Title Downloads
06. 10. 2021 Spin spin.pdfrecording
13. 10. 2021 Spin Exercises lab02.pdflab02.zip
20. 10. 2021 Spin Exercises II lab03.pdflab03.zip
27. 10. 2021 Spin Exercises III lab04.pdflab04.zip
03. 11. 2021 CTL Model Checking, OBDD Exercises lab05.pdf
24. 11. 2021 NuXMV lab07.pdflab07.ziprecording
01. 12. 2021 NuXMV Exercises lab08.zip

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