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. 82, Room 00-006 Thursday, 14:00–15:00, Bld. 82, Room 00-006 |
| Exercise | Thursday, 15:00–16:00, Bld. 82, Room 00-006 |
| First session | Tuesday 18.10.2016 |
| Language of instruction | English |
| Credits | 6 |
| Exams | t.b.a. |
| Course Catalog | here |
News
- Feb. 10: Craig interpolation for Nelson-Oppen theory combination (i.e. slides 401 - 418 in the slide set Craig Interpolation) is not relevant to the exam.
- Jan. 31: If the PiVC server is not responding when using the "Compile" button, you can use our server.
Menu->Settings->Change Server Address and enter "monteverdi.informatik.uni-freiburg.de:4242" as server address.
If that server is also not responding, contact Jochen. - Jan. 26: Note that sheet 13 is a short sheet (8 points possible). If you have problems with pivc, contact Tanja.
- Jan. 10: Because of the delayed upload of sheet 11, the deadline is extended until Jan. 17, 18:30.
- Dec. 13: Extended deadline for exercise 3 on sheet 8: Dec. 14, 23:59.
- Nov. 22: To solve the bonus exercise on sheet 6, you will need SMTInterpol. At the bottom of this page you can find a link to a page where you can download it.
- Oct. 31: Exercise sheet 3 is online, submit your solutions as usual before the lecture on Tuesday, Nov. 8.
- Oct. 25: As next Tuesday is a holiday, you can hand in your solutions to exercise sheet 2 by e-mail or at Tanja's office until Wednesday Nov. 2, 12:00 noon.
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)
- CVC4 (SMT-Solver developed by New York University and the University of Iowa)
- 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 (Tool for program verification by Stanford University)
Old Decision Procedures Lectures