Content
The course provides an introduction to verification. The emphasis is on the practical side. It might be helpful to also attend the courses Automated Deduction (Theory of Decision Procedures) and Model Checking.
Schedule
| week | date | topics | slides | sources | ||
|---|---|---|---|---|---|---|
| 1 | 06.03. | overview, verification, Sudoku encoding | pdf (1x1, 1x2, 1x4) | |||
| - | ||||||
| 2 | 20.03. | CNF generation | pdf (1x1, 1x2, 1x4) | |||
| 3 | 27.03. | reachability | pdf (1x1, 1x2, 1x4) | |||
| 4 | 17.04. | SAT in OCaml | pdf (1x1, 1x2, 1x4) | tar.gz | ||
| 5 | 24.04. | pseudo boolean constraints + proper orders | pdf (1x1, 1x2, 1x4) | |||
| 6 | 08.05. | non-linear arithmetic (1) | pdf (1x1, 1x2, 1x4) | |||
| 7 | 15.05. | non-linear arithmetic (2) | pdf (1x1, 1x2, 1x4) | |||
| 8 | 22.05. | bit-vector arithmetic | pdf (1x1, 1x2, 1x4) | |||
| 9 | 29.05. | answer set programming | pdf (1x1, 1x2, 1x4) | |||
| 10 | 05.06. | Hamiltonian Cycles, Evaluation | pdf (1x1, 1x2, 1x4) | |||
| 11 | 12.06. | SMT in term rewriting | pdf (1x1, 1x2, 1x4) | |||
| 12 | 19.06. | questions & answers session | ||||
| 13 | 26.06. | first exam | ||||
| 14 | 28.09 | second exam |