Computer-aided Verification 2017/18
The page of the course in USOSweb
or here (in English).
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
To get a grade one has to complete
- three lab assignments (NuSMV, Why3 and a bigger project in Coq)
- written exam.