7 Counterexample-guided abstraction refinement(CEGAR). CEGAR-based SMT solver (Презентации лекций)

SMT SolversandApplicationsVijay GaneshUniversity of WaterlooWinter 2013Wednesday, 16 January, 13Talk OutlineTopics covered in Lecture on SAT SolversMotivation for SAT/SMT solvers in software engineering• Software engineering (SE) problems reduced to logic problems• Automation, engineering, usability of SE tools through solversHigh-level description of the SAT/SMT problem & logics• Rich logics close to program semantics• Demonstrably easy to solve in many practical casesModern SAT solver architecture & techniques• DPLL search, shortcomings• Modern CDCL SAT solver: propagate (BCP), decide (VSIDS), conflict analysis, clause learn, backJump,• Termination, correctness• Big lesson: learning from mistakesTopics covered in Lecture on SMT Solvers• Modern SMT solver architecture & techniques• Rich logics closer to program semantics• DPLL(T), Combinations of solvers, Over/under approximations• My own contributions: STP & HAMPI• Abstraction-refinement for solving• Bounded logics• SAT/SMT-based applications• Future of SAT/SMT solversVijay GaneshWednesday, 16 January, 132Modern SMT SolversAre SAT Solvers Enough?What is SMT• Satisfiability Modulo Theories.

Just a fancy name for a mathematical theoryMotivations: why we need SMT?• A satisfiability solver for rich logics/natural theoriescorresponding SATisfiability problems)(Many natural complexity classes have• Easier to encode program semantics in these theories• Easier to exploit rich logic structure, greater opportunity for optimizationsSMT Logics• Bit-vectors, arrays, functions, linear integer/real arithmetic, strings, non-linear arithmetic• Datatypes, quantifiers, non-linear arithmetic, floating point• Extensible, programmableSAT & SMT is an explosive combo: incredible impactVijay GaneshWednesday, 16 January, 133What is Logic?Formal Languages and Valid ReasoningWhat is Logic• A formal language for constructing mathematical formulas with an associated proof system• Modern logic starts with the works of Boole, De Morgan, Frege, Cantor, Russell.What is a formal language in the context of logic• Well-defined rules for constructing formulas• Formulas are defined inductively• Universe of constant and variables• Terms are constructed out of constants, variables and functions• Atomic formulas are predicates applied to terms• Formulas are Boolean combination of atomic formulas• Appropriate quantification over variablesVijay GaneshWednesday, 16 January, 134First-order LogicA Language for Mathematics (most of it)First-order logic• Functions and predicates are uninterpreted• FOL has equality• Quantification only over variables (higher-order logics quantify over functions, predicates)Soundness and completeness of first-order logic (Godel, 1930)• Equivalence between provability and validity• Axioms ⊢A ⟺ Axioms ⊨ AUndecidability of first-order logic (Turing, Church 1936)• Hilbert’s 23rd problem• No fully automatic proof system for first-order logicVijay GaneshWednesday, 16 January, 135Mathematical TheoriesPeano Arithmetic and IncompletenessMathematical Theories• Functions and predicates are interpreted (and appropriate axioms are added to FOL)• Peano arithmetic (PA): +,-,*,/ are the functions.

= and < the predicates.• It is believed to be powerful enough to axiomatize number theoryIncompleteness theorem (Godel 1931)• There are true statements that are not provable in a system as powerful as Peano arithmetic,assuming consistency of PA• For the first time, this result distinguished truth from proof• Huge impact on logic and computability• Arithematization of syntax, Encode proofs as numbers, Diagonalize• G: G is not provable in this Theory TVijay GaneshWednesday, 16 January, 136Mathematical TheoriesThe SMT ProblemMathematical Theories• Peano arithmetic, Presburger, theories of strings, modular arithmetic, quantified Boolean logic• Different complexity classes: From undecidable, doubly-exponential, all the way down to NPcompleteSMT problem refers to the satisfiability problems for such rich theories• Satisfiability modulo-theories• How do we solve the SAT problem for rich theories efficiently and practically• Given the difficulty of solving these problems in general, what kind of heuristics are efficient• Can we play with soundness and completeness in a controlled fashion?• How do we combine such SATisfiability solvers into a solver for the combined theory• Quantifiers• How do we connect these solvers to practical software engineering applicationsVijay GaneshWednesday, 16 January, 137Standard-issue SMT Solver ArchitectureCombination of theories & DPLL(T)Input SMT InstanceCore Solver(Detects Equivalent Terms)Output: SAT or UNSATPurifyDPLL(T)(HandlesBoolean Structure)Theory 1Vijay GaneshWednesday, 16 January, 13...Theory n8Standard-issue SMT Solver ArchitectureCombination of theories: Nelson-OppenProblem Statement• Combine theory solvers to obtain a solver for a union theoryMotivation• Software engineering constraints over many natural theories• Natural theories well understood• ModularityHow• Setup communication between individual theory solvers• Communication over shared signature• Soundness, completeness and terminationVijay GaneshWednesday, 16 January, 139Standard-issue SMT Solver ArchitectureCombination of theories: Nelson-OppenExample Constraint over Linear Reals (R) and Uninterpreted Functions (UF)f(f(x)− f(y)) = af(0) = a+2x=yIDEA: Φcomb(ΦT1 ∧ EQ) ∧ (ΦT2 ∧ EQ)• First Step: purify each literal so that it belongs to a single theory• Second Step: check satisfiability and exchange entailed equalities over shared vars (EQ)• The solvers have to agree on equalities/disequalities between shared varsUFf(e1) = af(x) = e2f(y) = e3f(e4) = e5x=yVijay GaneshWednesday, 16 January, 13Re2 - e3 = e1e4 = 0e5 = a + 210Standard-issue SMT Solver ArchitectureCombination of theories: Nelson-OppenExample Constraint over Linear Reals (R) and Uninterpreted Functions (UF)f(f(x)− f(y)) = af(0) = a+2x=yIDEA: Φcomb(ΦT1 ∧ EQ) ∧ (ΦT2 ∧ EQ)• First Step: purify each literal so that it belongs to a single theory• Second Step: check satisfiability and exchange entailed equalities over shared vars (EQ)• The solvers have to agree on equalities/disequalities between shared varsUFf(e1) = af(x) = e2f(y) = e3f(e4) = e5x=yVijay GaneshWednesday, 16 January, 13Re2 - e3 = e1e4 = 0e5 = a + 2e2 = e311Standard-issue SMT Solver ArchitectureCombination of theories: Nelson-OppenExample Constraint over Linear Reals (R) and Uninterpreted Functions (UF)f(f(x)− f(y)) = af(0) = a+2x=yIDEA: Φcomb(ΦT1 ∧ EQ) ∧ (ΦT2 ∧ EQ)• First Step: purify each literal so that it belongs to a single theory• Second Step: check satisfiability and exchange entailed equalities over shared vars (EQ)• The solvers have to agree on equalities/disequalities between shared varsUFf(e1) = af(x) = e2f(y) = e3f(e4) = e5x=ye1 = e4Vijay GaneshWednesday, 16 January, 13Re2 - e3 = e1e4 = 0e5 = a + 2e2 = e312Standard-issue SMT Solver ArchitectureCombination of theories: Nelson-OppenExample Constraint over Linear Reals (R) and Uninterpreted Functions (UF)f(f(x)− f(y)) = af(0) = a+2x=yIDEA: Φcomb(ΦT1 ∧ EQ) ∧ (ΦT2 ∧ EQ)• First Step: purify each literal so that it belongs to a single theory• Second Step: check satisfiability and exchange entailed equalities over shared vars (EQ)• The solvers have to agree on equalities/disequalities between shared vars• UF says SAT, R says UNSAT.

Combination returns UNSAT.UFf(e1) = af(x) = e2f(y) = e3f(e4) = e5x=ye1 = e4Vijay GaneshWednesday, 16 January, 13Re2 - e3 = e1e4 = 0e5 = a + 2e2 = e3e5 = a13Standard-issue SMT Solver ArchitectureCombination of theories: Nelson-OppenIDEA: Φcomb(ΦT1 ∧ EQ) ∧ (ΦT2 ∧ EQ)• Does NOT always work, i.e., does not always give a complete solver• Example: Cannot combine T1 with only finite models, and T2 with infinite models• Impose conditions on T1 and T2• Stably Infinite: If a T-formula has a model it has an infinite model• Examples: Functions, Arithmetic• Extensions proved to be artificial or difficult• Deep model-theoretic implications (Ghilardi 2006, G. 2007)Vijay GaneshWednesday, 16 January, 1314Standard-issue SMT Solver ArchitectureCombination of theories & DPLL(T)Input SMT InstanceCore Solver(Detects Equivalent Terms)Output: SAT or UNSATPurifyDPLL(T)(HandlesBoolean Structure)Theory 1Vijay GaneshWednesday, 16 January, 13...Theory n15Standard-issue SMT Solver ArchitectureDPLL(T)Problem Statement• Efficiently handle the Boolean structure of the input formulaBasic Idea• Use a SAT solver for the Boolean structure &check assignment consistency against a T-solver• T-solver only supports conjunction of T-literalsImprovements• Check partial assignments against T-solver• Do theory propagation (similar to SAT solvers)• Conflict analysis guided by T-solver &generate conflict clauses (similar to SAT solvers)• BackJump (similar to SAT solvers)Vijay GaneshWednesday, 16 January, 1316Standard-issue SMT Solver ArchitectureDPLL(T)Uninterpreted Functions formula(1)(g(a) = c) ∧(¬2∨3) (f(g(a)) ≠ f(c) ∨ (g(a) = d)) ∧(¬4)(c ≠d)Theory and Unit Propagation Steps by DPLL(T)(Unit Propagate) (1)(Unit Propagate) (¬4)(Theory Propagate) (2)(Theory Propagate) (3)UNSATVijay GaneshWednesday, 16 January, 1317History of SMT SolversCategoryResearch ProjectResearcher/Institution/Time PeriodTheorem Proving(very early roots of decisionprocedures)NuPRLBoyer-Moore Theorem ProverACL2PVS Proof CheckerRobert Constable / Cornell / 1970’s-presentBoyer & Moore / UT Austin / 1970’s-presentMoore, Kauffmann et al.

/ UT Austin / 1980’s - presentNatarajan Shankar / SRI International / 1990’s-presentSAT SolversDPLLGRASP (Clause learning and backjumping)Chaff & zChaffMiniSATDavis, Putnam, Logemann & Loveland / 1962Marques-Silva & Sakallah / U. Michigan / 1996-2000Zhang, Malik et al. / Princeton / 1997-2002Een & Sorensson / 2005 - presentSimplifyShostakICSSVC, CVC, CVC-Lite, CVC3 ...Non-disjoint theoriesNelson & Oppen / DEC and Compaq / late 1980sShostak / SRI International / late 1980’sRuess & Shankar / SRI International / late 1990’sBarrett & Dill / Stanford U. / late 1990’sTinelli, Ghilardi,..., / 2000 - 2008DPLL(T)Barcelogic and Tinelli groupOliveras, Nieuwenhuis & Tinelli / UPC and Iowa / 2006Under/Over ApproximationsUCLIDSTPSeshia & Bryant / CMU / 2004 - presentGanesh & Dill / Stanford / 2005 - presentWidely-used SMT SolversZ3CVC4OpenSMTYicesMathSATSTPUCLIDDeMoura & Bjorner / Microsoft / 2006 - presentBarrett & Tinelli / NYU and Iowa / early 2000’s - presentBruttomesso / USI Lugano / 2008 - presentDeuterre / SRI International / 2005 - presentCimatti et al.