IntroductiontoSatisfiabilityModuloTheories(SMT).ppt

C. Barrett S. A. Seshia ICCAD 2009 Tutorial Introduction to Satisfiability Modulo Theories(SMT) Clark Barrett, NYU Sanjit A. Seshia, UC Berkeley Boolean Satisfiability (SAT) Satisfiability Modulo Theories Satisfiability Modulo Theories Given a formula in first-order logic, with associated background theories, is the formula satisfiable? Yes: return a satisfying solution No [generate a proof of unsatisfiability] Applications of SMT Hardware verification at higher levels of abstraction (RTL and above) Verification of analog/mixed-signal circuits Verification of hybrid systems Software model checking Software testing Security: Finding vulnerabilities, verifying electronic voting machines, … Program synthesis … References Satisfiability Modulo Theories Clark Barrett, Roberto Sebastiani, Sanjit A. Seshia, and Cesare Tinelli. Chapter 8 in the Handbook of Satisfiability, Armin Biere, Hans van Maaren, and Toby Walsh, editors, IOS Press, 2009. (available from our webpages) SMTLIB: A repository for SMT formulas (common format) and tools SMTCOMP: An annual competition of SMT solvers Roadmap for this Tutorial Background and Notation Survey of Theories Theory Solvers Approaches to SMT Solving Lazy Encoding to SAT Eager Encoding to SAT Conclusion Roadmap for this Tutorial Background and Notation Survey of Theories Theory Solvers Approaches to SMT Solving Lazy Encoding to SAT Eager Encoding to SAT Conclusion First-Order Logic A formal notation for mathematics, with expressions involving Propositional symbols Predicates Functions and constant symbols Quantifiers In contrast, propositional (Boolean) logic only involves propositional symbols and operators First-Order Logic: Syntax As with propositional logic, expressions in first-order logic are made up of sequences of symbols. Symbols are divided into logical symbols and non-logical symbols or parameters. Example: (x = y) ? (y = z) ? (f(z) ? f(x)+1) First-Order Logic: Syntax Logical Symbols Pr