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, Alexander Nutz |
| Lecture | Tuesday, 14:00–16:00, HS 101-01-016 Thursday, 14:00–15:00, HS 101-01-016 |
| Exercise | Thursday, 15:00–16:00, HS 101-01-016 |
| First session | Tuesday 24.4.2012 |
| Language of instruction | English |
| Credits | 6 |
| Exams | TBA |
| Course Catalog | here |
News
- Slides are now uploaded in logical units, the annotated versions are not saved, because no important annotations are made that are not written down on later slides
- SMTInterpol participated in the SMT-COMP 2012 -- look up the results here (look for the links to the different tracks)
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
Slides
- Introduction and Motivation, printable
- Propositional logic, printable
- First-order logic, printable
- Theories, printable
- Quantifier Elimination, printable
- Deciding the Conjunctive Fragment of the Theory of Rationals, printable
- Deciding Equalities with Uninterpreted Functions (conjunctive), printable
- Deciding the Theory of Arrays, printable
- Nelson Oppen Theory Combination, printable
- DPLL(T), printable
- PiVC, printable
- Interpolants, printable
- Conclusion, printable
Exercises
- Exercise 1
- Exercise 2, smtlib2 example
- Exercise 3
- Exercise 4
- Exercise 5
- Exercise 6
- Exercise 7, Main.java, LraSolver.java
update: you may also do it with precise Rationals. Use this class instead and change "LraSolver" to "LraSolverRationals" in Main.java. If you use this version, you have to use the inbuilt methods for computations -- here is the source of the Rational class. Also added an example smt-file (which corresponds to 1b from the sheet).
note: If you want to use an IDE like Eclipse, the easiest solution is to get the SmtInterpol source from the website and insert your solver into the smtlib2 directory and change Main.java there accordingly.
Other Material
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)
- Yices (SMT-Solver developed by Stanford Research Institute)
- Z3 (SMT-Solver developed by Microsoft Research)
- SMTLIB (A standard for encoding SMT-problems which is read by many solvers)