Lectures: Wednesday, 10:40, S8 (Jan KofroňFrantišek Plášil)
Labs: Monday, 9:00, S11 (Jan Kofroň)
Page in SIS: NSWI101
Grading: Credit and exam

News

Lectures

Date Title Downloads
07. 10. 2019 Spin model checker lecture02.pdf
09. 10. 2019 LTS, Process Algebras lecture01.pdf
16. 10. 2019 Kripke Structures, model checking, LTL lecture03.pdf
23. 10. 2019 LTL Explicit Model Checking lecture04.pdf
30. 10. 2019 CTL, Explicit CTL Model Checking lecture05.pdf
06. 11. 2019 Ordered Binary Decision Diagrams lecture06.pdf
13. 11. 2019 Symbolic CTL Model Checking lecture07.pdf
20. 11. 2019 Partial Order Reduction lecture08.pdf
27. 11. 2019 Timed Automata lecture09.pdf
04. 12. 2019 Infinte-State Model Checking, Bounded Model Checking
11. 12. 2019 Abstractions, Symmetries
18. 12. 2019 Stochastic Model Checking
08. 01. 2020 Assume-guarantee

Labs

Date Title Downloads
14. 10. 2019 Spin II. Lab01.zip
21. 10. 2019 Spin III + LTS, CCS. Lab01.pdfLab02.pdf
04. 11. 2019 Spin IV Distributed consensus I.Distributed consensus II.
11. 11. 2019 CTL + LTL Model Checking Lab04.pdf
25. 11. 2019 OBDD Exercises Lab06.pdf

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