Understanding Algorithms and Combination in Theory
Cover operations, quantifier elimination, and applications like strongest post-condition and procedure summaries are explored in the context of algorithms and their combination, shedding light on symbolic model checking, uninterpreted functions, and more.
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. Download presentation by click this link. If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.
E N D
Presentation Transcript
Cover Algorithms and Their Combination Sumit Gulwani, Madan Musuvathi Microsoft Research, Redmond 1
Cover Definition Cover operation is useful for simplifying a formula by discarding facts related to a set of variables Given A quantifier-free formula in theory T A set of symbols V Cover( , V) is The most-precise quantifier-free formula implied by that does not involve V e.g. Cover(y=f(a+v) f(b+v), {v}) : (a=b) ) y=0 2
Cover vs. Quantifier Elimination Quantifier Elimination: Given a quantified formula, output a logically equivalent quantifier-free formula 9V CoverT( ,V) if T admits quantifier elimination Some theories do not: theory of uninterpreted functions Example: f(y) = 0 Cannot say 0 is in the domain of y without using quantifiers Cover( ,V) is the most-precise quantifier-free approximation to 9V 3
Applications Strongest post-condition Useful for abstract interpretation on logical formulas Existential quantification of dead variables SP( , x := e) = 9 x ( [x /x] x = e[x /x]) Image computation Useful for reachability analysis in symbolic model checking Existential quantification of old state variables Ri+1(S) = 9S (Ri[S /S] T(S ,S)) Ri(S) 4
Applications Procedure summaries Existential quantification of local variables Useful for interprocedural analysis Interpolants Suppose A ) B. Then I is the Interpolant(A,B) if A ) I ) B I only contains variables common to A and B Cover(A, VA) is most precise Interpolant(A,B) :Cover(:B, VB) is least precise Interpolant(A,B) 5
Outline Symbolic model checking using Cover Cover algorithm for uninterpreted functions Cover algorithm for the combination of uninterpreted functions and linear arithmetic 6
Symbolic Model Checking Algorithm I(S) : initial states, E(S) : error states T(S ,S) : transition from old state S to new state S R(S): reachable states R0(S) = I(S) Ri+1(S) = 9S (Ri[S /S] T(S ,S)) Ri(S) Error found if Rn+1(S) E(S) is satisfiable 7
Symbolic Model Checking Using Cover I(S) : initial states, E(S) : error states T(S ,S) : transition from old state S to new state S R(S): reachable states R0(S) = I(S) Ri+1(S) = Cover(Ri[S /S] T(S ,S), S ) Ri(S) 8
Symbolic Model Checking Using Cover I(S) : initial states, E(S) : error states T(S ,S) : transition from old state S to new state S R(S): reachable states R0(S) = I(S) Ri+1(S) = Cover(Ri[S /S] T(S ,S), S ) Ri(S) This algorithm can find false errors As Cover over-approximates the set of reachable states 9
Symbolic Model Checking Using Cover I(S) : initial states, E(S) : error states T(S ,S) : transition from old state S to new state S R(S): reachable states R0(S) = I(S) Ri+1(S) = Cover(Ri[S /S] T(S ,S), S ) Ri(S) Theorem: If the transition system is described using quantifier-free formulas, symbolic model checking using cover is sound and precise 10
Outline Symbolic model checking using Cover Cover algorithm for uninterpreted functions Cover algorithm for the combination of uninterpreted functions and linear arithmetic 11
Cover Algorithm for Unary Uninterpreted Functions Cover( , V) = Erase V from congruence closure of Example: Let be x=f(v1) y=f(v2) v1 = v2 f x f y v2 v1 Cover( , {v1,v2}) is x=y 12
Cover Algorithm for Binary Uninterpreted Functions The erasure technique does not work Let be x=f(a,v) y=f(b,v) Erasure( , {v}) is true Cover( , {v}) is a=b ) x=y Cover( , V) is: For all partitions E of congruence classes in E ) Erasure( E, V) 13
Example a1 = b1 a2 = b1 ) y f y f x1 x1 f f a1 = b1 a2 = b2 ) y f x1 x2 f a2 v a1 v a1 = b2 a2 = b1 ) y x2 f x1 f x2 x1 a1 = b2 a2 = b2 ) y f b2 v b1 v x2x2 Cover( ,{v}) Cover( , {v}) can be exponential in 14
Outline Cover algorithm for linear arithmetic Cover algorithm for uninterpreted functions Cover algorithm for combination of theories 15
Combining Cover Algorithms: Idea 1 CoverT1 [ T2( 1 2, V): Return CoverT1( 1,V) CoverT2( 2,V) Fails on x=v1+1 y=v2+1 v1=f(z) v2=f(z) Algorithm returns true Cover is x=y Solution: Share variable equalities 16
Combining Cover Algorithms: Idea 2 CoverT1 [ T2( 1 2, V): E Saturate( 1, 2) Return CoverT1( 1 E,V) CoverT2( 2 E,V) Fails on v=x+1 y=f(v) Algorithm returns true Cover is y=f(x+1) Solution: Share equalities between variables and simple terms 17
Combining Cover Algorithms: Idea 3 CoverT1 [ T2( 1 2, V): E Saturate( 1, 2) Return CoverT1( 1 E,V) CoverT2( 2 E,V) Fails on x v v y v=f(z,v) Algorithm returns x y Cover is x y (x=y ) x=f(z,x)) Solution: Share conditional equalities 18
Example Cover(y=f(a+v) f(b+v), {v}) a=b ) v1=v2 v3 = f(v1) v4 = f(v2) v1 = a+v v2 = b+v y = v3-v4 a=b ) v3=v4 a=b ) y=0 true 19
Conclusion Cover is the most-precise quantifier-free approximation to quantifier elimination Cover algorithm for uninterpreted functions Cover algorithm for combination of theories Exchange equalities between variables and good terms Exchange conditional equalities 20
