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.