Skip to main content
SpringerLink
Log in
Book cover

International Joint Conference on Automated Reasoning

IJCAR 2010: Automated Reasoning pp 384–399Cite as

An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 6173))

Abstract

Craig interpolation has become a versatile tool in formal verification, for instance to generate intermediate assertions for safety analysis of programs. Interpolants are typically determined by annotating the steps of an unsatisfiability proof with partial interpolants. In this paper, we consider Craig interpolation for full quantifier-free Presburger arithmetic (QFPA), for which currently no efficient interpolation procedures are known. Closing this gap, we introduce an interpolating sequent calculus for QFPA and prove it to be sound and complete. We have extended the Princess theorem prover to generate interpolating proofs, and applied it to a large number of publicly available linear integer arithmetic benchmarks. The results indicate the robustness and efficiency of our proof-based interpolation procedure.

Supported by the Engineering and Physical Sciences Research Council (EPSRC) under grant no. EP/G026254/1, by the EU FP7 STREP MOGENTES, and by the EU ARTEMIS CESAR project.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Beyer, D., Zufferey, D., Majumdar, R.: CSIsat: Interpolation for LA+EUF. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 304–308. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  2. Cimatti, A., Griggio, A., Sebastiani, R.: Interpolant generation for UTVPI. In: Schmidt, R.A. (ed.) CADE 2009. LNCS, vol. 5663, pp. 167–182. Springer, Heidelberg (2009)

    Google Scholar 

  3. Craig, W.: Linear reasoning. a new form of the Herbrand-Gentzen theorem. The Journal of Symbolic Logic 22(3), 250–268 (1957)

    Article  MathSciNet  Google Scholar 

  4. Fitting, M.C.: First-Order Logic and Automated Theorem Proving, 2nd edn. Springer, Heidelberg (1996)

    Book  Google Scholar 

  5. Jain, H., Clarke, E., Grumberg, O.: Efficient interpolation for linear diophantine (dis)equations and linear modular equations. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 254–267. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  6. Kannan, R., Bachem, A.: Polynomial algorithms for computing the Smith and Hermite normal forms of an integer matrix. SIAM J. Comput. 8(4), 499–507 (1979)

    Article  MathSciNet  Google Scholar 

  7. Kapur, D., Majumdar, R., Zarba, C.G.: Interpolation for data structures. In: SIGSOFT ’06/FSE-14, pp. 105–116. ACM, New York (2006)

    Chapter  Google Scholar 

  8. Lynch, C., Tang, Y.: Interpolants for linear arithmetic in SMT. In: Cha, S(S.), Choi, J.-Y., Kim, M., Lee, I., Viswanathan, M. (eds.) ATVA 2008. LNCS, vol. 5311, pp. 156–170. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  9. Maehara, S.: On the interpolation theorem of Craig. Sugaku 12, 235–237 (1960)

    MathSciNet  MATH  Google Scholar 

  10. McMillan, K.L.: An interpolating theorem prover. Theor. Comput. Sci. 345(1) (2005)

    Google Scholar 

  11. McMillan, K.L.: Lazy abstraction with interpolants. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 123–136. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  12. Presburger, M.: Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt. In: Comptes Rendus du Ier congrès de Mathématiciens des Pays Slaves (1929)

    Google Scholar 

  13. Pugh, W.: The Omega test: a fast and practical integer programming algorithm for dependence analysis. Communications of the ACM 8, 102–114 (1992)

    Article  Google Scholar 

  14. Rümmer, P.: A sequent calculus for integer arithmetic with counterexample generation. In: VERIFY. CEUR, vol. 259 (2007), http://ceur-ws.org/

  15. Rümmer, P.: A constraint sequent calculus for first-order logic with linear integer arithmetic. In: Cervesato, I., Veith, H., Voronkov, A. (eds.) LPAR 2008. LNCS (LNAI), vol. 5330, pp. 274–289. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  16. Rybalchenko, A., Sofronie-Stokkermans, V.: Constraint solving for interpolation. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol. 4349, pp. 346–362. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  17. Schrijver, A.: Theory of Linear and Integer Programming. Wiley, Chichester (1986)

    MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. ETH Zurich, Switzerland

    Angelo Brillout

  2. Oxford University Computing Laboratory, United Kingdom

    Daniel Kroening, Philipp Rümmer & Thomas Wahl

Authors
  1. Angelo Brillout
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Daniel Kroening
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Philipp Rümmer
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Thomas Wahl
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. RWTH Aachen, LuFG Informatik, 2, Ahornstr. 55, 52074, Aachen, Germany

    Jürgen Giesl

  2. Department of Computer Science, Chalmers University of Technology, 41296, Gothenburg, Sweden

    Reiner Hähnle

Rights and permissions

Reprints and permissions

Copyright information

© 2010 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Brillout, A., Kroening, D., Rümmer, P., Wahl, T. (2010). An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic. In: Giesl, J., Hähnle, R. (eds) Automated Reasoning. IJCAR 2010. Lecture Notes in Computer Science(), vol 6173. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-14203-1_33

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-14203-1_33

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-14202-4

  • Online ISBN: 978-3-642-14203-1

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation