Computer-aided Verification 2018/19
The page of the course in USOSweb
is here
(in Polish)
or here (in English).
Course slides
Thanks to Sławkek Lasota and Daria Walukiewicz-Chrząszcz
for their slides.
Laboratory
- lab 1: Coq
- lab 2: Coq & HAHA
- lab 3: Coq
- lab 4: Coq
- lab 5: Cryptol and SAW
- lab 6: Why3
- lab 7: Why3
- lab 8: project TFTP (implementation of the Ocaml part)/s2n (choice of VT)
- lab 9: Why3 assignment
- lab 10: SPIN - basics, LTL
- lab 11: NuSMV - basics
- lab 12: NuSMV/SPIN - assignment
- lab 13: project TFTP (implementation and specification in Coq)/s2n Specifications in Cryptol and other formalisms
- lab 14: project TFTP (proofs in Coq)/s2n proofs in Coq/SAW
Assignments (year 2018/19)
Assignments (year 2017/18)
Grading
To get a grade one has to complete
- three lab assignments (NuSMV/SPIN, Why3 and a bigger project in Coq or SAW)
- written exam.