EfficientCraigInterpolationForSubsetsofIntegerLinear

《EfficientCraigInterpolationForSubsetsofIntegerLinear》由会员分享，可在线阅读，更多相关《EfficientCraigInterpolationForSubsetsofIntegerLinear（30页珍藏版）》请在装配图网上搜索。

1、Efficient Craig Interpolation For Subsets of Integer Linear Arithmetic Himanshu Jain,CMU Edmund M.Clarke,CMUOrna Grumberg,Technion0Interpolants Craig 1957Given formulas F,G such that F G is unsatisfiableAn interpolant for(F,G)is a formula I:1.F)I2.I G is unsatisfiable3.I contains only common variabl

2、es of F and G I(y)F(x,y)G(y,z)1Interpolants ExampleExample 1(propositional logic):F:=p q G:=:q r s I:=qExample 2(linear arithmetic):F:=x+2y 3 x-y -1G:=y 3F)y 2I:=y 2 2Interpolants in Verification McMillan 2003Useful in symbolic model checkingReach1(S)SComputing Reach1(S)requires existential quantifi

3、cation(costly using BDDs or SAT)Interpolant based image3Interpolants in Verification Jhala et al.2004Useful for Property Directed Invariant GenerationPredicateAbstractionPredicates SProgram PInvariants forP expressiblein terms of SInterpolants help in finding right set of predicates4How are Interpol

4、ants ObtainedF Gproof of unsatisfiability of F GInterpolant for(F,G)F,G5Existing Work on Computing Interpolants Pudlak,McMillan,Jhala et al.,Yorsh et al.,Kapur et al.,Rybalchenko et al.,Kroening et al.,Cimatti et al.,Beyer et al.vCan efficiently compute interpolants For rational/real linear arithmet

5、icFor equality with uninterpreted function symbols Propositional logic(using SAT solvers)vNo efficient interpolation algorithms for Integer linear arithmeticBit-vector arithmeticDecision problem for conjunctions is itself NP-hardWe make progress in this direction.6Difference between rational and int

6、eger linear arithmeticvLet H:=x=2y x=2z+1vIf x,y,z are rational variables H is satisfiable(take x=1,y=1/2,z=0)vIf x,y,z are integer variables H is unsatisfiable7Our resultsvPolynomial time interpolation algorithmsFor useful subsets of integer linear arithmeticvInteger(Diophantine)linear equationsE.g

7、.x=3y 5x=3z+u+2 vInteger linear congruences(modular equations)E.g.4x=2y+9(mod 3)2z+5x y=7(mod 4)vInteger linear equations and disequationsE.g.:(4x+5y=8)x=3y 8vIntroductionCraig InterpolationRelated Work vInteger Linear EquationsvInteger Linear CongruencesvInteger Linear Equations+DisequationsvExperi

8、mental resultsOutlineNew interpolation algorithmsWe will only give intuition and examples in the talk.See paper for precise description of results.9Interpolation for Integer Linear EquationsvF,G be conjuctions of integer linear equationsvWe show that interpolant for(F,G)is always:An integer linear e

9、quation or An integer linear congruencevF:=(x=2y)and G:=(x=2z+1)An interpolant is x=0(mod 2)10 1/5 F+1/5 G is equal to 6x+y+z=4/5(Contradiction)Interpolation Algorithm Step 1Obtain a proof of unsatisfiability of F G(How to get a contradiction from F G)F:=(30 x+4y =2)G:=(y+5z=2)1/5,1/511 F G1/5(30 x+

10、4y=2)+1/5(y+5z=2)Interpolation Algorithm Step 2 Sum the equations from F according to the proof of unsatisfiability 6 x+4/5 y=2/5 Partial interpolant We do not want x12 6 x+4/5 y=2/5 4/5 y-2/5=-6x)4/5 y 2/5 is divisible by 6)4/5 y 2/5=0(mod 6)4y-2=0(mod 30)Interpolation Algorithm Step 3 Remove varia

11、bles not common to F and G4y-2=0(mod 30)is an interpolant for(F,G)We have proved the correctness of above algorithm13Complexity of the AlgorithmvObtain proof of unsatisfiability(step 1)Polynomial time using Hermite Normal FormOverall algorithm is polynomial timevCan also use modern SMT solversvMulti

12、ple interpolants can be obtained14Multiple InterpolantsF:=30 x+4y=24y 2=0(mod 30)4y 2=0(mod 15)4y 2=0(mod 10)G:=y+5z=24y 2=0(mod 5)15vIntroductionCraig InterpolationRelated Work vInteger Linear EquationsvInteger Linear CongruencesvInteger Linear Equations+DisequationsvExperimental resultsOutlineNew

13、interpolation algorithms16Integer Linear Congruencesva=b(mod m)iff m divides(a-b)a,b,m can be rational numbersvInteger Linear Congruence:i ai xi=b(mod m)xi are integer variablesvExample:3x+2y+5z=0(mod 6)SATISFIABLE(x=2,y=0,z=0)17Interpolation for Integer Linear CongruencesvF,G be conjuctions of inte

14、ger linear congruencesvWe show that interpolant for(F,G)is always:An integer linear congruencevBasic steps same as beforeProof of unsatisfiability is more interesting18Proof of Unsatisfiability vCongruences may not hold with rational multipliers9=5(mod 2).But 9/4 5/4(mod 2)vWe show get a proof of un

15、satisfiabilityWith integer multipliers for equationsCongruence hold with integer multipliers19Proof of Unsatisfiability for Congruences2x+2y=4(mod 8)2x+y =4(mod 8)4x =4(mod 8)2(2x+2y=4)(mod 8)+-4(2x+y =4)(mod 8)+1 (4x =4)(mod 8)0 =-4(mod 8)Both proofs of unsatisfiability and(multiple)interpolants ca

16、n be obtained in polynomial time20vIntroductionCraig InterpolationRelated Work vInteger Linear EquationsvInteger Linear CongruencesvInteger Linear Equations+DisequationsvExperimental resultsOutlineNew interpolation algorithms21Integer Linear Equations+DisequationsvExample:(x+2y+z=1):(x=1)All integer

17、 variablesvLet F=Feq FneqvWe show F has no integral solution iffF has no rational solution,ORFeq has no integral solution22Interpolation for Integer Linear Equations+DisequationsGiven F=Feq Fneq,G=Geq Gneq,F G is unsat1.F G has no rational solutionInterpolant as integer linear eqn/disequation2.Feq G

18、eq has no integral solutionInterpolant as integer linear eqn/congruence23vIntroductionCraig InterpolationRelated Work vInteger Linear EquationsvInteger Linear CongruencesvInteger Linear Equations+DisequationsvExperimental resultsOutlineNew interpolation algorithms24Predicate Discoveryvoid main()int

19、x=0,y=0;while(*)x=x+4*nondet();y=y+8*nondet();assert(x+y!=1);assert(x+y!=2);assert(x+y!=3);Loop invariant:x+y is divisible by 4 That is,x+y=0(mod 4)C programSuch predicates can be found using our interpolation algorithms25Predicate Discovery ExperimentsExamplePredicates/InterpolantsTime(secs)ex1y=1(

20、mod 2)2.72ex2x+y=0(mod 2)0.83ex4x+y+z=0(mod 4)0.95ex5x=0(mod 4),y=0(mod 4)1.1ex64x+2y+z=0(mod 8)0.93ex74x-2y+z=0(mod 222)0.54forb1x+y=0(mod 3)0.1Existing state-of-the-art tools such as BLAST,SATABS,VCEGAR cannot verify these programs.With the help of predicates found byour algorithms they can(VCEGAR

21、).26ConclusionvEfficient Interpolation AlgorithmsInteger linear equationsInteger linear congruencesInteger linear equations and disequationsvEasy to implementvProofs of unsatisfiabilityInteger linear congruencesInteger linear equations and disequations27Future WorkvFull integer linear arithmetic Cutting-plane proofs/Pudlaks algorithm vBit-vector arithmeticvBoolean Combinations using SMT28Questions29