You are here: Home › Teaching › Summer Term 2022 › Decision Procedures (Lecture)

Decision Procedures

Decision Procedures are the basis for program verification: The task of program verification is to give a formal proof that a program meets its specification. This amounts to determining the truth value of a logical formula. A decision procedure is an algorithm that can for a certain type of formulas decide whether the formula is true or false. We will investigate decision procedures for different logics. Starting with propositional logic we will investigate decision procedures for logics with integers, reals, recursive structures (lists and trees), arrays, etc.
Course type Lecture
Instructors Andreas Podelski, Jochen Hoenicke, Tanja Schindler
Lecture Tuesday, 14:00–16:00, Bld. 101, Room 01-016/018
Thursday, 14:00–15:00, Bld. 101, Room 01-016/018
Exercise Thursday, 15:00–16:00, Bld. 101, Room 01-016/018
First session Tuesday 26.04.2022
Language of instruction English
Credits 6
Exams t.b.a.
Course Catalog Decision Procedures - Lecture
Decision Procedures - Exercises
Ilias Course Decision Procedures 2022

 

News

  • 2022-04-08: Section "Sessions" added.
  • 2022-04-07: Ilias course added.
  • 2022-04-05: Homepage online.

Sessions

The lecture and exercise sessions take place in-person at the location and time given above.
We will have hybrid lectures in the first week – remote participation is possible via BigBlueButton in our Ilias course.
This may change depending on the situation.

Formalia

Admission criteria

Half of the maximum points from the exercises have to be achieved in order to be admitted for the exam.
There will be an exercise sheet each week, usually with three exercises and a maximum of 12 points. You can usually hand in your submission before the lecture on Tuesday – alone or in groups of two.

Exam

The exam will be oral or written, depending on the number of participants.

 Please register via the examination office as usual.

Resources

Course Materials

Textbooks

  • Bradley A. R., Manna Z.: The Calculus of Computation: Decision Procedures with Applications to Verification, 2007, Springer, New York.
  • Kroening D., Strichmann O.: Decision Procedures - An Algorithmic Point of View, 2008, Springer.

Papers

  • B. Dutertre, L. de Moura: Integrating Simplex with DPLL(T), Technical Report, SRI_CSL-06-01, 2006.
  • B. Dutertre, L. de Moura: A fast linear-arithmetic solver for DPLL(T), CAV 2006.

Tools and Standards

  • SMTInterpol  (Interpolating SMT-Solver developed by us --- the chair of software engineering)
  • CVC5 (SMT-Solver developed by Stanford University and the University of Iowa)
  • Yices (SMT-Solver developed by SRI International)
  • Z3 (SMT-Solver developed by Microsoft Research)
  • SMTLIB (A standard for encoding SMT-problems which is read by many solvers)
  • PiVC (Tool for program verification by Stanford University)

Old Decision Procedures Lectures