Document Actions
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.
piVC (πVC)
Binaries for MacOS X and Linux and sources for πVC can be downloaded from Aaron Bradley's Homepage. I have built binaries for Cygwin (extract it into C:\pivc). Yices can be downloaded from the yices web-site.
Links & Literature
- A.R. Bradley, Z. Manna: The Calculus of Computation, Springer, 2007
- D. Kroening, O. Strichman: Decision Procedures, Springer, 2008
- 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.
- H. Arnold: A linearized DPLL calculus with learning
- S. Krstić: Architecting Solvers for SAT Modulo Theories: Nelson-Oppen with DPLL, Materials of Dagstuhl Seminar Deduction and Decision Procedures, 2007
- Instructors: Jochen Hoenicke | Sergio Feo Arenis
- Times & Locations: Fri, 09:00 - 10:00 c.t., HS 02-017 Geb. 052 | Tue, 11:00 - 13:00 c.t., HS 02-017 Geb. 052
- Times & Locations of tutorials: Fri, 10:00 - 11:00 c.t., HS 02-017 Geb. 052