Decision Procedures for Verification

Bernd Finkbeiner, Calogero G. Zarba

Time and place

Main Lecture: Friday 9am-11am, Building E1.3, Room 001

Exercise Session: Tuesday, 4pm-6pm, Building E1.1, Basement


Decision procedures for the satisfiability of logical formulas in first-order theories. Decision procedures for propositional logic. Decision procedures for the theories of equality, real numbers, integer numbers, lists, arrays, sets, and multisets. Cooperation methods: integration, combination, reduction.

Lecture notes