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
Homework
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
Acknowledgements
Some slides are taken from the Decision Procedures Website, and some are taken from The Calculus of Computation course.