中国科学技术大学：《程序分析与程序验证》课程教学资源（PPT课件讲稿）第7章 程序验证 ProgramVerification Necula 04 Decision-Procedure Based Theorem Provers Tactic-Based Theorem Proving Inferring Loop Invariants

Decision-Procedure Based Theorem Provers Tactic-Based Theorem Proving Inferring Loop Invariants CS294-8 Lecture 12 Prof.Necula CS 294-8 Lecture 12 1

Prof. Necula CS 294-8 Lecture 12 1 Decision-Procedure Based Theorem Provers Tactic-Based Theorem Proving Inferring Loop Invariants CS 294-8 Lecture 12

Review Source language VCGen FOL Theories Goal-directed Sat.proc Sat.proc proving 1 n Prof.Necula CS 294-8 Lecture 12 2

Prof. Necula CS 294-8 Lecture 12 2 Review Source language VCGen FOL Theories Sat. proc 1 Sat. proc n Goal-directed proving … ?

Combining Satisfiability Procedures Consider a set of literals F Containing symbols from two theories Ti and Ta We split F into two sets of literals Fi containing only literals in theory Ti F2 containing only literals in theory T2 We name all subexpressions: pi(f2(E))is split into f2(E)=n^pi(n) We have:unsat (F1A F2)iff unsat(F) unsat(F)v unsat(F2)=unsat(F) But the converse is not true So we cannot compute unsat(F)with a trivial combination of the sat.procedures for Ti and Ta Prof.Necula CS 294-8 Lecture 12 3

Prof. Necula CS 294-8 Lecture 12 3 Combining Satisfiability Procedures • Consider a set of literals F – Containing symbols from two theories T1 and T2 • We split F into two sets of literals – F1 containing only literals in theory T1 – F2 containing only literals in theory T2 – We name all subexpressions: p1 (f2 (E)) is split into f2 (E) = n  p1 (n) • We have: unsat (F1  F2 ) iff unsat(F) – unsat(F1 )  unsat(F2 )  unsat(F) – But the converse is not true • So we cannot compute unsat(F) with a trivial combination of the sat. procedures for T1 and T2

Combining Satisfiability Procedures.Example Consider equality and arithmetic ffx)-fy)≠fz) x≤y y+Z≤X 0≤Z y≤x X- f(x)=f(y) 0=Z fx)-fy）=z false← f(f(x)-f(y))=f(z) Prof.Necula CS 294-8 Lecture 12 4

Prof. Necula CS 294-8 Lecture 12 4 Combining Satisfiability Procedures. Example • Consider equality and arithmetic f(f(x) - f(y))  f(z) x  y y + z  x 0  z false f(x) = f(y) y  x x = y 0 = z f(x) - f(y) = z f(f(x) - f(y)) = f(z)

Combining Satisfiability Procedures Combining satisfiability procedures is non trivial And that is to be expected: Equality was solved by Ackerman in 1924,arithmetic by Fourier even before,but E+A only in 1979 yet in any single verification problem we will have literals from several theories: Equality,arithmetic,lists,... When and how can we combine separate satisfiability procedures? Prof.Necula CS 294-8 Lecture 12 5

Prof. Necula CS 294-8 Lecture 12 5 Combining Satisfiability Procedures • Combining satisfiability procedures is non trivial • And that is to be expected: – Equality was solved by Ackerman in 1924, arithmetic by Fourier even before, but E + A only in 1979 ! • Yet in any single verification problem we will have literals from several theories: – Equality, arithmetic, lists, … • When and how can we combine separate satisfiability procedures?

Nelson-Oppen Method (1) 1. Represent all conjuncts in the same DAG f(f(x)-f(y)≠f(z)∧Y≥×∧×≥Y+z∧z≥0 X Z 0 Prof.Necula CS 294-8 Lecture 12 6

Prof. Necula CS 294-8 Lecture 12 6 Nelson-Oppen Method (1) 1. Represent all conjuncts in the same DAG f(f(x) - f(y))  f(z)  y  x  x  y + z  z  0 f - f f y x  z 0  + f 

Nelson-Oppen Method (2) 2.Run each sat.procedure Require it to report all contradictions (as usual) Also require it to report all equalities between nodes f Z、 Prof.Necula CS 294-8 Lecture 12 7

Prof. Necula CS 294-8 Lecture 12 7 Nelson-Oppen Method (2) 2. Run each sat. procedure • Require it to report all contradictions (as usual) • Also require it to report all equalities between nodes f - f f y x  z 0  + f 

Nelson-Oppen Method (3) 3.Broadcast all discovered equalities and re-run sat. procedures Until no more equalities are discovered or a contradiction arises f x Contradiction Z、 Prof.Necula CS 294-8 Lecture 12 8

Prof. Necula CS 294-8 Lecture 12 8 Nelson-Oppen Method (3) 3. Broadcast all discovered equalities and re-run sat. procedures • Until no more equalities are discovered or a contradiction arises f - f f y x  z 0  + f  x Contradiction

What Theories Can be Combined? Only theories without common interpreted symbols But Ok if one theory takes the symbol uninterpreted Only certain theories can be combined Consider (Z,+,and Equality -Consider:1≤×≤2Λa=1Ab=2∧f(X)≠f(a)Af(X)≠f(b) No equalities and no contradictions are discovered yet,unsatisfiable A theory is non-convex when a set of literals entails a dis junction of equalities without entailing any single equality Prof.Necula CS 294-8 Lecture 12 9

Prof. Necula CS 294-8 Lecture 12 9 What Theories Can be Combined? • Only theories without common interpreted symbols – But Ok if one theory takes the symbol uninterpreted • Only certain theories can be combined – Consider (Z, +, ·) and Equality – Consider: 1  x  2  a = 1  b = 2  f(x)  f(a)  f(x)  f(b) – No equalities and no contradictions are discovered – Yet, unsatisfiable • A theory is non-convex when a set of literals entails a disjunction of equalities without entailing any single equality

Handling Non-Convex Theories Many theories are non-convex Consider the theory of memory and pointers It is not-convex: trueA=A'v sel(upd(M,A,V),A')=sel(M,A) (neither of the dis juncts is entailed individually) For such theories it can be the case that No contradiction is discovered No single equality is discovered - But a disjunction of equalities is discovered We need to propagate disjunction of equalities.. Prof.Necula CS 294-8 Lecture 12 10

Prof. Necula CS 294-8 Lecture 12 10 Handling Non-Convex Theories • Many theories are non-convex • Consider the theory of memory and pointers – It is not-convex: true  A = A’  sel(upd(M, A, V), A’) = sel(M, A’) (neither of the disjuncts is entailed individually) • For such theories it can be the case that – No contradiction is discovered – No single equality is discovered – But a disjunction of equalities is discovered • We need to propagate disjunction of equalities …