The page of the course in USOSweb is here (in Polish) or here (in English).

- lecture 1: introduction
- lecture 2: Coq first time, second time
- lecture 3: LTL
- lecture 4: LTL and automata
- lecture 5: model checking for LTL
- lecture 6: CTL
- lecture 7,8: symbolic verification I: OBDD
- lecture 8: symbolic verification II
- lecture 9: bounded model checking
- lecture 10: Why3
- lecture 11: Why3 (slides from the web of Why3)
- lecture 12: abstract interpretation

Thanks to Sławkek Lasota and Daria Walukiewicz-Chrząszcz for their slides.

- lab 1: Coq
- lab 2: Coq & HAHA
- lab 3: Coq
- lab 4: Coq
- lab 5: SPIN - basics, LTL
- lab 6: NuSMV - basics
- lab 7: project TFTP (implementation of the Ocaml part)
- lab 8: NuSMV - modelling and verification, examples
- lab 9: project TFTP (implementation and specification in Coq)
- lab 10: NuSMV - bounded model checking
- lab 11: NuSMV - assignment
- lab 12: project TFTP (proofs in Coq)
- lab 13: Why3
- lab 14: Why3

- Coq - TFTP lab assignment (14 points)
- NuSMV - lab assignment (8 points)
- Why3 - lab assignment. (8 points)
- Exam assignment. (30 points)

To get a grade one has to complete

- three lab assignments (NuSMV, Why3 and a bigger project in Coq)
- written exam.