Verifying Cyberphysical Systems with Satisfiability Modulo Theories
Explore the concepts of Satisfiability Modulo Theories (SMT), theories, models, decision procedures, and examples in the context of cyberphysical systems. Learn about SAT, SMT problems, and the architecture of an SMT solver. Understand the importance of theories and models in mathematical logic. Dive into the syntax of writing formulas and defining signatures in building up a theory.
Download Presentation
Please find below an Image/Link to download the presentation.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author. If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.
You are allowed to download the files provided on this website for personal or commercial use, subject to the condition that they are used lawfully. All files are the property of their respective owners.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author.
E N D
Presentation Transcript
Satisfiability modulo theories Verifying cyberphysical systems Sayan Mitra mitras@illinois.edu Some of the slides and examples for this lecture are from Clark Barrett
Today Satisfiability modulo theories (SMT) Theories, models, decision procedures Examples Brief z3 tutorial (see notebook)
Satisfiability modulo theories SAT: Given a well-formed formula in propositional logic, determine whether there exists a satisfying solution A satisfiability modulo theory (SMT) problem is a generalization of SAT in which some of the binary variables are replaced by predicates over a suitable set of non-binary variables ?1?,?,?,? := ? ? = 5 ? ? 2 ? ? > 2 (? ? = 2) ?2?,?,? := 3?2 4? + 5? 5 ( 2? + 5?3 7) ?1is a predicate in difference logic in which the variables are real-valued, and the clauses are constructed with standard comparison operations >, >=, =$ and (minus) ?2is a predicate in real arithmetic
Architecture of an SMT solver Theory solvers/decision procedures boolean skeleton of problem CNF formula in real arithmetic Arithmetic Bitvectors Difference logic Core DPLL Uninterpreted functions assertions solution or counterexample
????? A short overview of theories, models, decision procedures
What is a theory in mathematical logic? When we talk about well-formed formulas with non-binary variables, we have to say exactly what type of formulas are allowed and, what it means for assignments to satisfy such formulas This brings us to the notions theory and models in mathematical logic
Building up a theory First we define the syntax for writing formulas A signature = ( ?, ?,?) set of function symbols ?,?.?., +, ,?,?,???, set of predicate symbols ? arity of each function: ?????: ? 0 arity functions are constants ?: set of variables ?= 0,+ , ?= < ????? 0 = 0 ????? + = 2 ????? < = 2 ? = {?,?,?} Terms defined by this signature are ?,?,?,+ ?,? ,+ + ?,? ,0 ,0, ????? ,? Elements of ? are terms If ?1, ,?? ????? ,? and ? ? with arity k, then ? ?1, ,?? ?????( ,?) Ground terms are terms without variables
Terms to Formulas ? < ? + ?,? = +(?,?) Atomic formulas ?? True, False If ?1, ,?? ????? ,? and p ? with arity k, then p ?1, ,?? ??( ,?) A literal is an AF or its negation Set of all atomic formulas ?? ,? + ?,? = 0 ? > ? Quantifier free formulas ??? ,? ?, ?:+ ?,? = 0 ?, ?:? < ? ?, ?:+ ?,? = ? ?? if ?1,?2 ??? then ?1 ???,?1 ?2 ???,?1 ?2 ???,?1 ?2 ??? Set of all quantifier free formulas ??? ,? First order formulas is the set of quantifier free formulas under universal and existential quantifiers Bound variables are those that are attached to quantifiers Free variables: variables not bound ?:+ ?,? = ? Sentence: First order formula with no free variables Theory ,? set of all sentences over ,?
Models for theories Example model for = {0,+,<} ? = ?,?,? ? 0 = ? This notion of model from mathematical logic is not to be confused with the notion of a model for a computational or physical process ? < = { ?,? , ?,? , ?,? } ? + ? ? ? A model gives meanings or interpretations to formulas in theory ? ? ? ? ? ? ? ? ? A model ? for T = Theory( ,?) has to define A domain |M| interpretations of all functions and predicate symbols ? ? : ?? |?| if arity ? = ? ? ? ?? if ????? ? = ? Assignment ? ? |?| for every variable ? ? ? ? ? ? if ? ? = ?,? ? = ? then ? +(?,?) is ? + ? ? ,? ? ? + ?,? = ? ?(+ + ?,? ,? = ? ? ? ? + ?,? = ? = A formula ? is true in ? if it evaluates to true under the given interpretations over domain ? We say that the model ?T-satisfies the formula ?
Decision procedures Given a theory ? a theory solver or a decision procedure for ? takes as input a set of literals ? (atomic propositions) and determines whether ? is ?-satisfiable, that is, a model ? such that ? ??
\????? A short overview of theories and models in mathematical logic
Example theories Uninterpreted functions (UF) ?:= ?,?, , ?:= = ,?:= ?? ?1= ?2 ?3 ?2 ? ?3 ?(?2) Difference logic ?:= 1,2,.., , ?:= <, ,=,>, ?1 ?2 ?, where <, ,=,>, Linear arithmetic 4? 3? + 6? 10 Real arithmetic (nonlinear) 4?2+ 6? 9?3 5 Bit vectors Arrays ? ? = ? ? + 1
Example decision procedure 1: Difference logic ? = (? ? = 5) (? ? 2) (? ? > 2) (? ? = 2) (? ? < 0) Decision procedure: Convert each literal (AF) to ?1 ?2 ? form: ? = ? ? 5 (? ? 5) ? ? 2 ? ? 3 ? ? 2 (? ? 2) (? ? 1)
?= ? ? 5 (? ? 5) ? ? 2 ? ? 3 ? ? 2 (? ? 2) (? ? 1) Construct a graph with edge from ? ?? for each literal ? ? 2 5 5 ? ? 3 2 1 2 ?
?= ? ? 5 (? ? 5) ? ? 2 ? ? 3 ? ? 2 (? ? 2) (? ? 1) Construct a graph ?? with edge from ? ?? for each literal ? ? 5 2 Proposition. ? is satisfiable iff G? is negative cycle free. Exercise. 5 ? ? 3 2 1 2 ?
Example decision procedure 2: Uninterpreted functions (UF) ? = ?1= ?2 (?2= ?3) (?4= ?5) ?5 ?1 (? ?1 ? ?3) Decision procedure 1. Put all variables and function instances in their own classes 2. If ?1= ?2 is a literal then merge the classes containing them; do this repeatedly 3. If ?1 and ?2 are terms in the same class then merge classes containing ? ?1 and ?(?2); repeat 4. If ?1 ?2 is a literal in ? and they belong to the same class then return unsat else return sat ?1 and ?2
Example decision procedure 2: Uninterpreted functions (UF) Initial classes ? = ?1= ?2 (?2= ?3) (?4= ?5) ?5 ?1 (? ?1 ? ?3) Classes {?1} ?2 ?3 ?4 ?5 ? ?1 ? ?3 {?1,?2,?3} ?4,?5 ? ?1 ? ?3 {?1,?2,?3} ?4,?5 ? ?1,?(?3) Unsat
? ? ? = ? ? ? ? ? ? ? ? = ? ? ? Return to SMT Several approaches, lazy approach: Abstract ? to propositional form Feed to DPLL Use theory decision procedure to refine propositional formula a guide SAT Theory solvers/decision procedures boolean skeleton of problem literals/formula in real arithmetic Arithmetic Bitvectors Difference logic Core DPLL Uninterpreted functions assertions solution or counterexample
Theory solvers/decision procedures boolean skeleton of problem literals/formula in real arithmetic Arithmetic Bitvectors Difference logic Core DPLL ? ? ? = ? ? ? ? ? ? ? ? = ? ? ? Uninterprete d functions asserti ons solution or counterexample 3 4 2 1 send {1, 2 3, 4 } to DPLL returns model {1, 2, 4 } UF solver concretizes to ? ? = ? , ? ? ? checks this as UNSAT send {1, 2 3, 4 , 1 2 4 } to DPLL returns model {1, 2, 3, 4 } UF solver concretizes and finds this to be UNSAT send {1, 2 3, 4 , 1 2 4, 1 2 3 4 } to DPLL returns UNSAT ? ? , ? ?
Assignments HW1 Learn z3 https://ericpony.github.io/z3py-tutorial/guide-examples.htm Readings Chapter 7.5.3 of CPSBook on using SAT/SMT for verification Read chapter 4 for next week Reading more about decision procedures
