en | de

Experiments in Verification – Practice of Decision Procedures

master program

VO1  SS 2012  703523

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)
- 13.03.
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