# 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

## Keywords

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

- Table of Contents
- Chapter 1: Many-Sorted Logic
- Chapter 2: Equality
- Chapter 3: Reals
- Chapter 4: Integers
- Chapter 5: Lists
- Chapter 6: Arrays
- Chapter 7: Sets
- Chapter 8: Multisets
- Chapter 9: Combination

## Readings

- David G. Mitchell. A SAT solver primer. Bulletin of the EATCS, 85:112-132, 2005.
- Vijay Ganesh, Sergey Berezin, and David L. Dill. Deciding Presburger Arithmetic by Model Checking and Comparisons with Other Methods. In Formal Methods in Computer-Aided Design, volume 2517 of Lecture Notes in Computer Science, pages 171-186, Springer, 2002.