Syllabus
A course on logic theories and procedures for deciding satisfiability in these theories with emphasis on the application in program verification.
Construction of an efficient SAT solver (DPLL, conflict-directed clause learning), local algorithms for satisfiability (WalkSAT, survey propagation), decisions in logic with equality, uninterpreted functions and pointers, quantified Boolean formulae (QBF), combining logic theories,
SAT-modulo solvers.
The course is accompanied with a seminar. There will be tasks to exercise the taught material as well as implementation tasks based on the existent software libraries.
Annotation
A course on logic theories and procedures for deciding satisfiability in these theories with emphasis on the application in program verification.
Construction of an efficient SAT solver (DPLL, conflict-directed clause learning), local algorithms for satisfiability (WalkSAT, survey propagation), decisions in logic with equality, uninterpreted functions and pointers, quantified Boolean formulae (QBF), combining logic theories,
SAT-modulo solvers.