3 Angelo Brillout Daniel Kroening Philipp Rümmer Thomas Wahl 2010 An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic IJCAR Edinburgh Springer to appear Lecture Notes on Computer Science 16/07/2010 <p><font face="CMR9" size="1"><font face="CMR9" size="1"><font face="CMR9" size="1"><font face="CMR9" size="1">Craig interpolation has become a versatile tool in formal verification, for instance to generate intermediate assertions for safety analysis. Interpolants are typically determined by annotating the stepsof an unsatisfiability proof with&nbsp;<font face="CMTI9" size="1"><font face="CMTI9" size="1">partial interpolants</font></font><font face="CMR9" size="1"><font face="CMR9" size="1">. In this paper, we consider Craig interpolation for full </font></font><font face="CMTI9" size="1"><font face="CMTI9" size="1">quantifier-free Presburger arithmetic </font></font><font face="CMR9" size="1"><font face="CMR9" size="1">(QFPA), for which currently no ecient interpolation procedures are known. Closing this gap, we introduce an </font></font><font face="CMTI9" size="1"><font face="CMTI9" size="1">interpolating sequent calculus </font></font><font face="CMR9" size="1"><font face="CMR9" size="1">for QFPA and prove it to be sound and complete. We then add uninterpreted predicates to the calculus, thus extending it to important theories such as arrays and uninterpreted functions. We demonstrate the efficiency of our interpolation procedure on a large range of publicly available benchmarks.</font></font>&nbsp;</font></font></font></font></p><p>&nbsp;</p><p>&nbsp;</p><p>&nbsp;</p><p align="left">&nbsp;</p> http://www.kroening.com/publications/view-publications-bkrw2010.html