Report

Satisfiability Modulo Theories (An introduction) Magnus Madsen Todays Talk What are SMT solvers? How are they used in practice? Motivation Find and s.t.: ≥3∧ ≤0∨ ≥0 Knowledge of prop. logic ≥3∧ ≤0 ∨ ≥3∧ ≥0 Knowledge of integers =3∧ =0 Solution Knowledge of integers What is SMT? Satisfiability Modulo + Theories What is a SMT instance? A logical formula built using – negation, conjunction and disjuction k-SAT • e.g. ∧ ∨ • e.g. ∨ ¬ ∨ ∧ ¬ ∨ ¬ ∨ ∧ ∨ ∨ theory of theory of – theory bitwise specific operators integers operators • e.g. ≤ 5, ≠ • e.g. ⊕ ⊕ = • e.g. = () ∧ ( ) ≠ ( ) theory of uninterpreted functions Recall k-SAT The Boolean SATisfiability Problem: ∨ ¬ ∨ ∧ ¬ ∨ ¬ ∨ ∧ ∨ ∨ ∧ ⋯ clause literal or negated literal • 2SAT is solveable in polynomial time • 3SAT is NP-complete (solveable in exponential time) Q: Why not encode every formula in SAT? Graph Problems: • Shortest-Path • Minimum Spanning Tree Optimization: • Max-Flow • Linear Programming (just to name a few) A: Theory solvers have very efficient algorithms Q: But then, Why not get rid of the SAT solver? A: SAT solvers are very good at case analysis Formula ≥3∧ ≤0∨ ≥0 SMT Solver ≥3∧ ≤0 ∧ ∨ ≥3∧ ≥0 SAT NO YES ∧ ∧ Theory NO add clause: ¬ ∧ YES =3 =0 Important Properties • Efficiency of both SAT and Theory solver! • SAT Solver – Incremental (supports adding new clauses) • Theory Solver – Ability to construct blocking clauses – Ability to create so-called "theory lemmas" Theories Theory of: – Difference Arithemetic – Linear Arithmetic – Arrays – Bit Vectors – Algebraic Datatypes – Uninterpreted Functions SMT-LIB • A modeling language for SMT instances – A declarative language with Lisp-like syntax – Defines common/shared terminology • e.g. LRA = Closed linear formulas in linear real arithmetic • e.g. QF_BC = Closed quantifier-free formulas over the theory of fixed-size bitvectors. – http://www.smtlib.org/ Example 1 =∧= Solution Example 2 Applications • • • • • Dynamic Symbolic Execution Program Verification Extended Static Checking Model Checking Termination Analysis See Also: Tapas: Theory Combinations and Practical Applications Dynamic Symbolic Execution • combines dynamic and symbolic execution – step 1: execute the program recording the branches taken and their symbolic constraints – step 2: negate one constraint – step 3: solve the constraints to generate new input to the program (e.g. by using a SMT solver) – step 4: if a solution exists then execute the program on the new input Program Path Negate ¬3 ¬1 2 ¬3 4 Run SMT Solver New Program Path ¬1 2 3 5 Example: Greatest Common Divisor Original program SSA unfolding int gcd(int x, int y) { while (true) { int m = x % y; if (m == 0) return y; x = y; y = m; } } int gcd(int x0, int y0) { while (true) { int m0 = x0 % y0; assert(m0 != 0) if (m0 == 0) return y0; x1 = y0; y1 = m0; int m1 = x1 % y1; assert(m1 == 0) if (m1 == 0) return y1; } } int result = gcd(2, 4) Collecting Constraints Collected constraints SSA unfolding int result = gcd(2, 4) int gcd(int x0, int y0) { while (true) { int m0 = x0 % y0; assert(m0 != 0) if (m0 == 0) return y0; x1 = y0; y1 = m0; int m1 = x1 % y1; assert(m1 == 1) if (m1 == 0) return y1; } } (assert (= m0 (mod x0 y0))) (assert (not (= m0 0))) (assert (assert (assert (assert (= (= (= (= x1 y1 m1 m1 y0)) m0)) (mod x1 y1))) 0)) (assert (not (= m1 0))) Computing a new path int gcd(int x, int y) { while (true) { int m = x % y; if (m == 0) return y; x = y; y = m; } Iteration 1: x = } Iteration 2: x = 2&y=3 3&y=2 Iteration 3: x = 2 & y = 1 Solution: x = 2 and y = 3 Program Verification int binary_search(int[] arr, int low, int height, int key) { assert(low > high || 0 <= < high); while (low <= high) { // Find middle value int mid = (low + high) / 2; assert(0 <= mid < high); Assertion Violation: int val = arr[mid]; low = 230, high = 230+1 // Refine range if (key == val) return mid; if (val > key) low = mid + 1; else high = mid – 1; } return -1; } SMT Solvers • Z3 – Microsoft Research • MathSAT5 – University of Trento • CVC4 – New York University • Many more SMT-COMP • A yearly competition between SMT solvers Z3 Research Directions in SMT • Improving the efficiency of SAT/Theory solvers • Improving the interplay between the SAT solver and the theory solver – e.g. "online" solvers (partial truth assignment) • Developing solvers for new theories • Combining different theories With Thanks to Evan Driscoll References • Satisfiability Modulo Theories: Introduction and Applications – Leonardo De Moura & Nikolaj Bjørner • Tapas: Theory Combinations and Practical Applications – Leonardo De Moura & Nikolaj Bjørner • Z3 Tutorial Guide – http://rise4fun.com/z3/tutorial/guide Summary Satisfiability Modulo Theory (SMT): – constraint systems involving SAT + Theory SMT solvers combine the best of: – SAT solvers and theory solvers SMTs have applications in program analysis More Work To Be Done?