# Computer-aided Verification 2017/18

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

### Course slides

- lecture 1: introduction
- lecture 2: Coq
- lecture 3: LTL
- lecture 4: LTL and automata
- lecture 5: model checking for LTL
- lecture 6: CTL
- lecture 7: symbolic verification I: OBDD
- writing formulas in CTL: microwave assignment
- lecture 8: wymbolic 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.

### Laboratory

- 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