Seminar: Decision Procedures

Seminar (7CP)

Winter Semester 2012/2013

Instructor: Ruzica Piskac

Content

In this seminar we will introduce the machinery and algorithms deployed inside modern SMT solvers.

Organization

When: seminar takes place on Friday from 12:30–16:30.

The seminar will take place on the following dates: November 9th, 16th, 23rd, 30th, December 14th, January 11th, 18th, 25th, February 1st, 8th, 15th

Where: room 029, E1 5 (MPI-SWS building, UdS Campus), videocast to KL room 206.

Attendance policy: Seminars thrive on lively discussions. Therefore, attendance is mandatory. Absences require prior approval of the instructor (with the obvious exception of medical emergencies).

Grading Scheme

The final grade is calculated using the following scheme: 50% of the grade is based on your presentation, 30% of the grade comes from the home works, and 20% comes from the seminar participation. Regularly submitting your homework is mandatory.

Course Material

The seminar is based on the "The Calculus of Computation" book by Aaron R. Bradley and Zohar Manna

Slides and Suggested Readings

  1. Motivation (pdf)
    Leonardo de Moura, Nikolaj Bjørner: Satisfiability modulo theories: introduction and applications. Commun. ACM 54(9): 69-77 (2011) (href)
  2. Propositional Logic (pdf)
    Sharad Malik, Lintao Zhang: Boolean satisfiability from theoretical hardness to practical success. Commun. ACM 52(8): 76-82 (2009) (href)
  3. First-Order Logic (pdf)
    Leo Bachmair, Harald Ganzinger: Resolution Theorem Proving. Handbook of Automated Reasoning 2001: 19-99 (href)
    Rob van Glabbeek's proof of the undecidability of first-order logic (href)
  4. First-Order Theories (pdf)
  5. Multisets with Cardinality Constraints (pdf)
    Ruzica Piskac, Viktor Kuncak: Decision Procedures for Multisets with Cardinality Constraints. VMCAI 2008: 218-232 (href)
    Ruzica Piskac, Viktor Kuncak: Linear Arithmetic with Stars. CAV 2008: 268-280 (href)
  6. Quantifier-Free Theory of Equality. Congruence Closure Algorithm presented by Farzaneh Ansari (pdf)
    Greg Nelson, Derek C. Oppen: Fast Decision Procedures Based on Congruence Closure. J. ACM 27(2): 356-364 (1980) (href)
  7. Quantifier Elimination. Ferrante-Rackoff's Method. Cooper's Method. presented by Tigran Mkrtchyan (pdf)
    D.C. Cooper: Theorem Proving in Arithmetic without Multiplication. Machine Intelligence. Edinburgh University Press: 91-100. (1972) (href)
    Jeanne Ferrante, Charles Rackoff: A Decision Procedure for the First Order Theory of Real Addition with Order. SIAM J. Comput. 4(1): 69-76 (1975) (href)
  8. Quantifier-Free Linear Arithmetic. Linear Programming. presented by Nancy Estrada (pdf)
    Christos H. Papadimitriou: On the complexity of integer programming. J. ACM 28(4): 765-768 (1981) (href)
  9. Boolean Algebra with Presburger Arithmetic. presented by Lavdrim Selimi (pdf)
    Viktor Kuncak, Huu Hai Nguyen, Martin C. Rinard: Deciding Boolean Algebra with Presburger Arithmetic. J. Autom. Reasoning 36(3): 213-239 (2006) (href)
    Viktor Kuncak, Martin C. Rinard: Towards Efficient Satisfiability Checking for Boolean Algebra with Presburger Arithmetic. CADE 2007: 215-230 (href)
  10. More on LIA: Omega Test. Difference Logic. presented by Johannes Kloos (pdf)
    William Pugh: The Omega test: a fast and practical integer programming algorithm for dependence analysis. SC 1991: 4-13 (1991) (href)
    Scott Cotton, Eugene Asarin, Oded Maler, Peter Niebert: Some Progress in Satisfiability Checking for Difference Logic. FORMATS/FTRTFT 2004: 263-276 (href)
  11. A Fast Linear-Arithmetic Solver for Quantifier-free Rational Arithmetic. presented by Filip Niksic (pdf)
    Bruno Dutertre, Leonardo de Moura: A Fast Linear-Arithmetic Solver for DPLL(T). CAV 2006:81-94 (href)
  12. Weak Monadic Second-Order Theory of One Successor (WS1S). presented by Susanne van den Elsen (pdf)
    James Glenn, William I. Gasarch. Implementing WS1S via Finite Automata. Workshop on Implementing Automata, 1996: 50-63. (href)
    Shunichi Toida's slides on the conversion of NFA to DFA (href)
  13. Array Property Fragment. presented by Max-Ferdinand Suffel (pdf)
    Aaron R. Bradley, Zohar Manna, Henny B. Sipma. What's decidable about arrays? VMCAI 2006: 427-442. (href)
  14. Bitvectors. presented by Jose Lopes (pdf)
    David Cyrluk, M. Oliver Möller, Harald Rueß. An Efficient Decision Procedure for the Theory of Fixed-Sized Bit-Vectors. CAV 1997: 60-71. (href)
  15. Nelson-Oppen Combination of Decision Procedures. presented by Stefan Bier (pdf)
    Greg Nelson, Derek C. Oppen. Simplification by Cooperating Decision Procedures. TOPLAS, Volume 1 Issue 2, Oct. 1979. (href)
  16. DPLL(T). presented by Heinrich Ody (pdf)
    Robert Nieuwenhuis, Albert Oliveras, Cesare Tinelli. Solving SAT and SAT Modulo Theories: From an abstract Davis--Putnam--Logemann--Loveland procedure to DPLL(T). J. ACM 53(6): 937-977 (2006). (href)
  17. Quantifiers. (pdf)
    Leonardo de Moura, Nikolaj Bjørner: Efficient E-Matching for SMT Solvers. CADE 2007: 183-198. (href)
    Yeting Ge, Leonardo de Moura: Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories. CAV 2009: 306-320. (href)
  18. A Quick Overview of Verification Condition Generation.
    Viktor Kuncak's notes on verification condition generation. (href)
    Viktor Kuncak's notes on basics of Hoare Logic. (href)
    Işıl Dillig's slides on the Hoare calculus. (href)

Home Assignments

  1. Home Assignments 01 (pdf)
  2. Home Assignments 02 (pdf)
  3. Home Assignments 03 (pdf)
  4. Home Assignments 04 (pdf)
  5. Home Assignments 05 (pdf)
    (deadline: 05. 03. 2013.)