Decision Procedures

Lecture slides

• Propositional Logic
• Propositional Logic
• Normal Forms, DPLL
• First order logic
• First order logic
• First order logic, Theory of equality
• Equality logic with uninterpreted functions
• Equality logic with uninterpreted functions
• Equality logic with uninterpreted functions
• Linear arithmetic, Simplex
• Simplex, Fourier-Motzkin
• The Omega test
• The Omega test, Difference logic
• Bit-Vectors
• Bit Flattening
• Presburger Arithmetic, Theory of array
• Combining decision procedures
• Combining decision procedures, Eliminating quantifiers
• Quantified Boolean Formulas, QDLA
• General Quantification, E-Matching
• Array Property Fragment
• Dafny, Program Correctness (Binary Search) (Linear Search) (Bubble Sort)
• Program Correctness, Loop Invariant
• Hoare Logic, Weakest Precondition, Strongest Postcondition
• WP Rules, Weakest Liberal Precondition, SP Rules
• SP Rules, Termination

Assignments

• Tseitin transformation (patch.txt) (aim-100-1_6-no-1.cnf)
• DPLL algorithm (sat.cnf) (unsat.cnf) (dubois22.cnf)
• Equality logic with uninterpreted functions

Homework

• Bit-vectors (add.z3)

Project ideas

• Implement the Omega test algorithm.
• Implement BST APIs in Dafny and verify that the BST property holds at each node in the BST.
• Implement the CDCL algorithm for SAT solving.
• Implement a solver for Bit-vectors.

Books

• The calculus of computation: decision procedures with applications to verification, by Aaron R.Bradley and Zohar Manna
• Decision Procedures: An Algorithmic Point of View, by Daniel Kroening and Ofer Strichman

Feedback

Acknowledgements