Logical Abstract InterpretationFinal Goal of the classOutlineDecision ProceduresSlide 5Linear ArithmeticDifference ConstraintsSlide 8Uninterpreted FunctionsUninterpreted Functions: ExampleUninterpreted Functions: ComplexitySlide 12Combination of Linear Arithmetic and Uninterpreted FunctionsCombining Decision ProceduresConvex TheoryExamples of Non-convex TheoryStably Infinite TheoryNelson-Oppen MethodologyCombining Decision Procedures: ExampleSlide 20Slide 21Transfer Functions for Logical Abstract InterpreterFixed-point ComputationInitializationSlide 25Slide 26Slide 27Difference Constraints: ExampleSlide 29Slide 30Slide 31Uninterpreted Functions: Example of JoinSlide 33Combination: Decision ProcedureCombination: Join AlgorithmCombination: Existential Quantifier EliminationSlide 38Abstract Interpretation over Combined Domain: ExampleSlide 40Universally Quantified Abstract DomainQuantified Abstract Domain: Join AlgorithmQuantified Abstract Domain: Example of JoinQuantified Abstract Domain: EliminateSlide 45Quantified Abstract Domain: Example of EliminateQuantified Abstract Domain : ExampleReferencesSlide 49Abstract Program Model / Problem StatementSlide 51Assertion Checking: Linear ArithmeticReducing PCP Problem to Assertion CheckingSlide 54Slide 55Assertion Checking: Uninterpreted FunctionsSlide 57Slide 58Assertion Checking: Combination of Linear Arithmetic & Uninterpreted FunctionsReducing Unsatisfiability to Assertion CheckingEncoding disjunctionConclusionLogical Abstract InterpretationSumit GulwaniMicrosoft Research, RedmondFinal Goal of the classAutomatically verify partial correctness of programs like the following using abstract interpretation.Void Init(int* A, int n) { for (i := 0; i<n; i++;) A[i] := 0; for (j := 0; j<n; j++;) Assert(A[j] = 0);}OutlineDecision Procedures–Linear Arithmetic–Uninterpreted Functions–Combination of Linear Arithmetic and Uninterpreted Fns•Logical Abstract Interpretation–Linear Arithmetic–Uninterpreted Functions–Combination of Linear Arithmetic and Uninterpreted Fns–Universally Quantified Formulas•Hardness of Assertion Checking–Linear Arithmetic–Uninterpreted Functions–Combination of Linear Arithmetic and Uninterpreted FnsDecision ProceduresDPT() = Yes, if  is satisfiable = No, if  is unsatisfiableWithout loss of generality, we can assume that  is a conjunction of atomic facts. •Why?–DP(1Ç2) is sat iff DP(1) is sat or DP(2) is sat•What is the trade-off?–Converting  into DNF may incur exponential blow-upOutline•Decision ProceduresLinear Arithmetic–Uninterpreted Functions–Combination of Linear Arithmetic and Uninterpreted Fns•Logical Abstract Interpretation–Linear Arithmetic–Uninterpreted Functions–Combination of Linear Arithmetic and Uninterpreted Fns–Universally Quantified Formulas•Hardness of Assertion Checking–Linear Arithmetic–Uninterpreted Functions–Combination of Linear Arithmetic and Uninterpreted FnsLinear ArithmeticExpressions e := y | c | e1 § e2 | c £ eAtomic facts g := e¸0 | e 0Note that e=0 can be represented as e¸0 Æ e·0 e>0 can be represented as e-1¸0 (over integer LA)•The decision problem for integer LA is NP-hard. •The decision problem for rational LA is PTime.–PTime algorithms are complicated to implement. Popular choice is an exponential algorithm called “Simplex”–We will study a PTime algorithm for a special case.Difference Constraints•A special case of Linear Arithmetic•Constraints of the form x·c and x-y·c–We can represent x·c by x-u·c, where u is a special zero variable. Wlog, we will assume henceforth that we only have constraints x-y·c•Reasoning required: x-y·c1 Æ y-z·c2 ) x-z·c1+c2•O(n3) (saturation-based) decision procedure–Represent contraints by a matrix Mn£n• where M[i][j] = c represents xi–xj· c–Perform transitive closure of M•M[i][j] = min { M[i][j], M[i][k]+M[k][j] }–  is unsat iff 9i: M[i][i] < 0Outline•Decision Procedures–Linear ArithmeticUninterpreted Functions–Combination of Linear Arithmetic and Uninterpreted Fns•Logical Abstract Interpretation–Linear Arithmetic–Uninterpreted Functions–Combination of Linear Arithmetic and Uninterpreted Fns–Universally Quantified Formulas•Hardness of Assertion Checking–Linear Arithmetic–Uninterpreted Functions–Combination of Linear Arithmetic and Uninterpreted FnsUninterpreted FunctionsExpressions e := x | F(e1,e2)Atomic fact g := e1=e2 | e1e2Axiom 8e1,e2,e1’,e2’: e1=e1’ Æ e2=e2’ ) F(e1,e2)=F(e1’,e2’) (called congruence axiom)(saturation-based) Decision Procedure•Represent equalities e1=e2 2 G in Equivalence DAG (EDAG)–Nodes of an EDAG represent congruence classes of expressions that are known to be equal.•Saturate equalities in the EDAG by following rule:–If C(e1)=C(e1’) Æ C(e2)=C(e2’), Merge C(F(e1,e2)), C(F(e1’,e2’))where C(e) denotes congruence class of expression e•Declare unsatisfiability iff 9 e1e2 in G s.t. C(e1) = C(e2)Uninterpreted Functions: ExampleyFFFFFy=F3(y)F(y)=F4(y)F2(y)=F5(y)y=F2(y)y=F5(y)yF(y)F(y)=F3(y)y=F(y)?: unsatÆÆUninterpreted Functions: Complexity•Complexity of congruence closure : O(n log n), where n is the size of the input formula–In each step, we merge 2 congruence classes. The total number of steps required is thus n, where n is a bound on the original number of congruence classes.–The complexity of each step can be O(log n) by using union-find data structureOutline•Decision Procedures–Linear Arithmetic–Uninterpreted FunctionsCombination of Linear Arithmetic and Uninterpreted Fns•Logical Abstract Interpretation–Linear Arithmetic–Uninterpreted Functions–Combination of Linear Arithmetic and Uninterpreted Fns–Universally Quantified Formulas•Hardness of Assertion Checking–Linear Arithmetic–Uninterpreted Functions–Combination of Linear Arithmetic and Uninterpreted FnsCombination of Linear Arithmetic and Uninterpreted FunctionsExpressions e := y | c | e1 § e2 | c £ e | F(e1,e2)Atomic Facts g := e¸0 | e0Axioms: Combined axioms of linear arithmetic + uninterpreted fns.Decision Procedure: Nelson-Oppen methodology for combining decision proceduresCombining Decision Procedures•Nelson-Oppen gave an algorithm in 1979 to combine decision procedures for theories T1 and T2, where:–T1 and T2 have disjoint signatures •except equality–T1, T2 are stably