Contact    Jobs
Search:

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

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.

Homeworks