Content

How can the correctness of security-critical software and hardware be ensured? How should an airline assign flight crew to flights to minimise costs, at the same time meeting regulations and ensuring the schedule is robust? How can a fixed number of software tests cover a maximal number of test situations? For such verification and optimization tasks SAT and SMT solvers turned out to be powerful catalyzers which render problems practically solvable that have long been considered infeasible.

The course provides an introduction into the theory and practice of SAT and SMT solving, covering the following topics:

• propositional logic (SAT) and DPLL
• maximal satisfiability (maxSAT)
• satisfiability modulo theories (SMT) and DPLL(T)
• how to solve common theories such as linear arithmetic, uninterpreted functions, and bit vectors
• Nelson-Oppen combination method

The course will consist of both lecture parts and practical parts. While the former provide theoretical input, the latter give opportunity to gain hands-on experience with problem solving using SAT and SMT encodings ...

Schedule

week	date	slides	sources	exercises	solutions
1	07.10.	pdf (1x1, 4x1)	test.py	pdf	pdf
2	21.10.	pdf (1x1, 4x1)	gardening.py	pdf	pdf
3	28.10.	pdf (1x1, 4x1)	optimize.py	pdf	pdf
4	04.11.	pdf (1x1, 4x1)	unsatCore.py	pdf	pdf
5	11.11.	pdf (1x1, 4x1)	euf.py	pdf	pdf
6	18.11.	pdf (1x1, 4x1)		pdf
7	25.11.	pdf (1x1, 4x1)		pdf	pdf
8	02.12.	pdf (1x1, 4x1)
9	09.12.	pdf (1x1, 4x1)		pdf	pdf
10	16.12.	pdf (1x1, 4x1)	bithacksmin.py	pdf	pdf
11	13.01.	pdf (1x1, 4x1)	sax_collision.py	pdf	pdf
12	20.01.	pdf (1x1, 4x1)	verification.py, prog.smt2	pdf	pdf
13	27.01.	pdf (1x1, 4x1)
14	03.02.

Tests

Two tests will take place on December 2 (test, solution) and February 3, respectively.