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

News

Lectures

Date Title Downloads
02. 10. 2019 LTS, Process Algebras
09. 10. 2019 Spin
16. 10. 2019 Kripke Structures, model checking, LTL
23. 10. 2019 LTL Explicit Model Checking
30. 10. 2019 CTL, Explicit CTL Model Checking
06. 11. 2019 Ordered Binary Decision Diagrams
13. 11. 2019 Symbolic CTL Model Checking
20. 11. 2019 Partial Order Reduction
27. 11. 2019 Timed Automata
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

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