Skip to main content
SpringerLink
Log in
Book cover

International Joint Conference on Automated Reasoning

IJCAR 2012: Automated Reasoning pp 118–133Cite as

From Strong Amalgamability to Modularity of Quantifier-Free Interpolation

  • Conference paper

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

Abstract

The use of interpolants in verification is gaining more and more importance. Since theories used in applications are usually obtained as (disjoint) combinations of simpler theories, it is important to modularly re-use interpolation algorithms for the component theories. We show that a sufficient and necessary condition to do this for quantifier-free interpolation is that the component theories have the ‘strong (sub-)amalgamation’ property. Then, we provide an equivalent syntactic characterization, identify a sufficient condition, and design a combined quantifier-free interpolation algorithm handling both convex and non-convex theories, that subsumes and extends most existing work on combined interpolation.

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   39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.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. Bacsich, P.D.: Amalgamation properties and interpolation theorems for equational theories. Algebra Universalis 5, 45–55 (1975)

    Article  MathSciNet  MATH  Google Scholar 

  2. 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 

  3. Bozzano, M., Bruttomesso, R., Cimatti, A., Junttila, T., Ranise, S., van Rossum, P., Sebastiani, R.: Efficient Satisfiability Modulo Theories via Delayed Theory Combination. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 335–349. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  4. Brillout, A., Kroening, D., Rümmer, P., Wahl, T.: An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic. In: Giesl, J., Hähnle, R. (eds.) IJCAR 2010. LNCS, vol. 6173, pp. 384–399. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  5. Brillout, A., Kroening, D., Rümmer, P., Wahl, T.: Beyond Quantifier-Free Interpolation in Extensions of Presburger Arithmetic. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol. 6538, pp. 88–102. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  6. Bruttomesso, R., Ghilardi, S., Ranise, S.: A Combination of Rewriting and Constraint Solving for the Quantifier-Free Interpolation of Arrays with Integer Difference Constraints. In: Tinelli, C., Sofronie-Stokkermans, V. (eds.) FroCos 2011. LNCS, vol. 6989, pp. 103–118. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  7. Bruttomesso, R., Ghilardi, S., Ranise, S.: Rewriting-based Quantifier-free Interpolation for a Theory of Arrays. In: RTA (2011)

    Google Scholar 

  8. Bruttomesso, R., Ghilardi, S., Ranise, S.: From Strong Amalgamation to Modularity of Quantifier-Free Interpolation. Technical Report RI 337-12, Dip. Scienze dell’Informazione, Univ. di Milano (2012)

    Google Scholar 

  9. Bruttomesso, R., Ghilardi, S., Ranise, S.: Quantifier-Free Interpolation of a Theory of Arrays. Logical Methods in Computer Science (to appear, 2012)

    Google Scholar 

  10. Chang, C., Keisler, J.H.: Model Theory, 3rd edn. North-Holland, Amsterdam (1990)

    MATH  Google Scholar 

  11. Cimatti, A., Griggio, A., Sebastiani, R.: Efficient Interpolant Generation in Satisfiability Modulo Theories. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 397–412. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  12. Enderton, H.B.: A Mathematical Introduction to Logic. Academic Press, New York (1972)

    MATH  Google Scholar 

  13. Fuchs, A., Goel, A., Grundy, J., Krstić, S., Tinelli, C.: Ground Interpolation for the Theory of Equality. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 413–427. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  14. Ghilardi, S.: Model theoretic methods in combined constraint satisfiability. Journal of Automated Reasoning 33(3-4), 221–249 (2004)

    Article  MathSciNet  MATH  Google Scholar 

  15. Goel, A., Krstić, S., Tinelli, C.: Ground Interpolation for Combined Theories. In: Schmidt, R.A. (ed.) CADE 2009. LNCS, vol. 5663, pp. 183–198. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  16. Henzinger, T., McMillan, K.L., Jhala, R., Majumdar, R.: Abstractions from Proofs. In: POPL (2004)

    Google Scholar 

  17. Mal’cev, A.I.: Axiomatizable classes of locally free algebras of certain types. Sibirsk. Mat. Ž. 3, 729–743 (1962)

    MathSciNet  Google Scholar 

  18. Jhala, R., McMillan, K.L.: A Practical and Complete Approach to Predicate Refinement. In: Hermanns, H. (ed.) TACAS 2006. LNCS, vol. 3920, pp. 459–473. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  19. Jónsson, B.: Universal relational systems. Math. Scand. 4, 193–208 (1956)

    MathSciNet  MATH  Google Scholar 

  20. Kapur, D., Majumdar, R., Zarba, C.: Interpolation for Data Structures. In: SIGSOFT 2006/FSE-14, pp. 105–116 (2006)

    Google Scholar 

  21. Kiss, E.W., Márki, L., Pröhle, P., Tholen, W.: Categorical algebraic properties. A compendium on amalgamation, congruence extension, epimorphisms, residual smallness, and injectivity. Studia Sci. Math. Hungar. 18(1), 79–140 (1982)

    MathSciNet  Google Scholar 

  22. Kovács, L., Voronkov, A.: Finding Loop Invariants for Programs over Arrays Using a Theorem Prover. In: Chechik, M., Wirsing, M. (eds.) FASE 2009. LNCS, vol. 5503, pp. 470–485. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  23. McMillan, K.: Interpolants from Z3 proofs. In: Proc. of FMCAD (2011)

    Google Scholar 

  24. McMillan, K.L.: An Interpolating Theorem Prover. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 16–30. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  25. McMillan, K.L.: An Interpolating Theorem Prover. Theor. Comput. Sci. 345(1), 101–121 (2005)

    Article  MathSciNet  MATH  Google Scholar 

  26. Nelson, G., Oppen, D.C.: Simplification by Cooperating Decision Procedures. ACM Transactions on Programming Languages and Systems 1(2), 245–257 (1979)

    Article  MATH  Google Scholar 

  27. Oppen, D.C.: Reasoning about recursively defined data structures. Journal of the ACM 27, 403–411 (1980)

    Article  MathSciNet  MATH  Google Scholar 

  28. Ringel, C.M.: The intersection property of amalgamations. J. Pure Appl. Algebra 2, 341–342 (1972)

    Article  MathSciNet  MATH  Google Scholar 

  29. Rybalchenko, A., Sofronie-Stokkermans, V.: Constraint Solving for Interpolation. J. of Symbolic Logic 45(11), 1212–1233 (2010)

    MathSciNet  MATH  Google Scholar 

  30. Sofronie-Stokkermans, V.: Interpolation in Local Theory Extensions. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol. 4130, pp. 235–250. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  31. Tinelli, C., Harandi, M.T.: A new correctness proof of the Nelson-Oppen combination procedure. In: Proc. FroCoS 1996, pp. 103–119 (1996)

    Google Scholar 

  32. Yorsh, G., Musuvathi, M.: A Combination Method for Generating Interpolants. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS (LNAI), vol. 3632, pp. 353–368. Springer, Heidelberg (2005); Extended version available as Technical Report MSR-TR-2004-108, Microsoft Research (October 2004)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Università degli Studi di Milano, Milan, Italy

    Roberto Bruttomesso & Silvio Ghilardi

  2. FBK (Fondazione Bruno Kessler), Trento, Italy

    Silvio Ranise

Authors
  1. Roberto Bruttomesso
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Silvio Ghilardi
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Silvio Ranise
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Fakultät für Informatik, Technische Universität Wien, Favoritenstr. 9, E185/2, 1040, Wien, Austria

    Bernhard Gramlich

  2. École Polytechnique, INRIA Saclay and Laboratoire d’Informatique, Route de Saclay, 91128, Palaiseau Cedex, France

    Dale Miller

  3. School of Computer Science, University of Manchester, Oxford Road, M13 9PL, Manchester, UK

    Uli Sattler

Rights and permissions

Reprints and permissions

Copyright information

© 2012 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Bruttomesso, R., Ghilardi, S., Ranise, S. (2012). From Strong Amalgamability to Modularity of Quantifier-Free Interpolation. In: Gramlich, B., Miller, D., Sattler, U. (eds) Automated Reasoning. IJCAR 2012. Lecture Notes in Computer Science(), vol 7364. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-31365-3_12

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-31365-3_12

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-31364-6

  • Online ISBN: 978-3-642-31365-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation