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, 10:00–12:00, HS 51-03-026 Thursday, 10:00–11:00, HS 51-03-026 |
| Exercise | Thursday, 11:00–12:00, HS 51-03-026 |
| First session | Tuesday 16.4.2013 |
| Language of instruction | English |
| Credits | 6 |
| Exams | TBA |
| Course Catalog | here |
News
- (18.04.2013) corrected dates on first exercise sheet. If you want to submit electronically, please send it to nutz@informatik.uni...
- (5.6.2013) The files accompanying exercise sheet 6 will be delayed a little more (new target: Wednesday -- today -- 16:00). We are sorry for any inconvenience, you still have a week for working on it, of course.
- (5.6.2013, 16:15) The mentioned files are online, now. The deadline will be Wednesday 12.6. in the evening.
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 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
(The slides are initially from last year's lecture and are updated on-the-fly. So they are subject to minor changes like changing dates, fixing typos, or other smaller errors. The final version should be online a few days after the corresponding lecture has been held.)
- Introduction and Motivation
- Propositional logic
- First-order logic
- Theories
- Quantifier Elimination
- Quantifier-Free Theory of Rationals
- Quantifier-Free Theory of Equality
- Theories of Arrays
- Nelson-Oppen Theory Combination
- DPLL(T)
- PiVC
(slides are up-to-date until here)
Exercises
- Exercise Sheet 1
- Exercise Sheet 2, smtlib2 propositional example script
- Exercise Sheet 3
- Exercise Sheet 4
- Exercise Sheet 5
- Exercise Sheet 6
readmeEx6.txt, smtinterpol.jar, QuantifierEliminationTQ.java, test.smt2
readMeEx7.txt, smtinterpol.jar, LraSolver.java, test file, smtinterpol-src.zip
CcSolver.java, ccTest.smt2
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)
- piVC (A tool for program verification)
- I have set up a πVC server at flaedle.informatik.uni-freiburg.de:4242 (Settings->Change Server Address)