Craig Interpolation for Quantifier-Free Presburger Arithmetic

Details Craig Interpolation for Quantifier-Free Presburger Arithmetic Craig Interpolation for Quantifier-Free Presburger Arithmetic

2008-11-21

arxiv.org/abs/0811.3521v1

Computer Science

Logic in Computer Science

15 pages, 1 algorithm, 1 figure

Scientific paper

Craig interpolation has become a versatile algorithmic tool for improving software verification. Interpolants can, for instance, accelerate the convergence of fixpoint computations for infinite-state systems. They also help improve the refinement of iteratively computed lazy abstractions. Efficient interpolation procedures have been presented only for a few theories. In this paper, we introduce a complete interpolation method for the full range of quantifier-free Presburger arithmetic formulas. We propose a novel convex variable projection for integer inequalities and a technique to combine them with equalities. The derivation of the interpolant has complexity low-degree polynomial in the size of the refutation proof and is typically fast in practice.

Affiliated with

Also associated with

No associations

Rating

Craig Interpolation for Quantifier-Free Presburger Arithmetic does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.

If you have personal experience with Craig Interpolation for Quantifier-Free Presburger Arithmetic, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Craig Interpolation for Quantifier-Free Presburger Arithmetic will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-163260