skip to main content
10.1145/2429069.2429132acmconferencesArticle/Chapter ViewAbstractPublication PagespoplConference Proceedingsconference-collections
research-article

Complete instantiation-based interpolation

Published: 23 January 2013 Publication History

Abstract

Craig interpolation has been a valuable tool for formal methods with interesting applications in program analysis and verification. Modern SMT solvers implement interpolation procedures for the theories that are most commonly used in these applications. However, many application-specific theories remain unsupported, which limits the class of problems to which interpolation-based techniques apply. In this paper, we present a generic framework to build new interpolation procedures via reduction to existing interpolation procedures. We consider the case where an application-specific theory can be formalized as an extension of a base theory with additional symbols and axioms. Our technique uses finite instantiation of the extension axioms to reduce an interpolation problem in the theory extension to one in the base theory. We identify a model-theoretic criterion that allows us to detect the cases where our technique is complete. We discuss specific theories that are relevant in program verification and that satisfy this criterion. In particular, we obtain complete interpolation procedures for theories of arrays and linked lists. The latter is the first complete interpolation procedure for a theory that supports reasoning about complex shape properties of heap-allocated data structures. We have implemented this procedure in a prototype on top of existing SMT solvers and used it to automatically infer loop invariants of list-manipulating programs.

Supplementary Material

JPG File (r2d3_talk5.jpg)
MP4 File (r2d3_talk5.mp4)

References

[1]
F. Alberti, R. Bruttomesso, S. Ghilardi, S. Ranise, and N. Sharygina. Lazy abstraction with interpolants for arrays. In LPAR, volume 7180 of LNCS, pages 46--61. Springer, 2012.
[2]
P. Bacsich. Amalgamation properties and interpolation theorems for equational theories. Algebra Universalis, 5:45--55, 1975.
[3]
M. Barnett and K. R. M. Leino. To goto where no statement has gone before. In VSTTE, volume 6217 of LNCS, pages 157--168, 2010.
[4]
C. Barrett, A. Stump, and C. Tinelli. The SMT-LIB Standard: Version 2.0, 2010.
[5]
D. Beyer, T. A. Henzinger, and G. Théoduloz. Lazy shape analysis. In CAV, volume 4144 of LNCS, pages 532--546. Springer, 2006.
[6]
D. Beyer, D. Zufferey, and R. Majumdar. CSIsat: Interpolation for LA
[7]
EUF. In CAV, volume 5123 of LNCS, pages 304--308, 2008.
[8]
R. Bornat. Proving Pointer Programs in Hoare Logic. In MPC, volume 1837 of LNCS, pages 102--126. Springer, 2000.
[9]
A. Brillout, D. Kroening, P. Rümmer, and T. Wahl. An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic. J. Autom. Reasoning, 47(4):341--367, 2011.
[10]
A. Brillout, D. Kroening, P. Rümmer, and T. Wahl. Beyond Quantifier-Free Interpolation in Extensions of Presburger Arithmetic. In VMCAI, volume 6538 of LNCS, pages 88--102. Springer, 2011.
[11]
R. Bruttomesso, S. Ghilardi, and S. Ranise. Rewriting-based quantifier-free interpolation for a theory of arrays. In RTA, volume 10 of LIPIcs, pages 171--186, 2011.
[12]
R. Bruttomesso, S. Ghilardi, and S. Ranise. From strong amalgamability to modularity of quantifier-free interpolation. In IJCAR, volume 7364 of LNCS, pages 118--133. Springer, 2012.
[13]
P. Cousot, R. Cousot, and L. Mauborgne. The reduced product of abstract domains and the combination of decision procedures. In FOSSACS, volume 6604 of LNCS, pages 456--472. Springer, 2011.
[14]
W. Craig. Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory. The Journal of Symbolic Logic, 22(3):269--285, 1957.
[15]
L. de Moura and N. Bjørner. Z3: An efficient SMT solver. In TACAS, pages 337--340, 2008.
[16]
K. Dr\"ager, A. Kupriyanov, B. Finkbeiner, and H. Wehrheim. SLAB: A Certifying Model Checker for Infinite-State Concurrent Systems. In TACAS, volume 6015 of LNCS, pages 271--274. Springer, 2010.
[17]
V. D'Silva, D. Kroening, M. Purandare, and G. Weissenbacher. Interpolant strength. In VMCAI, volume 5944 of LNCS, pages 129--145. Springer, 2010.
[18]
E. Ermis, M. Sch\"af, and T. Wies. Error invariants. In FM, volume 7436 of LNCS, pages 187--201. Springer, 2012.
[19]
J.-C. Filliâtre and C. Marché. The Why/Krakatoa/Caduceus Platform for Deductive Program Verification. In CAV, volume 4590 of LNCS, pages 173--177. Springer, 2007.
[20]
A. Fuchs, A. Goel, J. Grundy, S. Krstic, and C. Tinelli. Ground interpolation for the theory of equality. In TACAS, volume 5505 of LNCS, pages 413--427. Springer, 2009.
[21]
Y. Ge and L. M. de Moura. Complete instantiation for quantified formulas in satisfiabiliby modulo theories. In CAV, volume 5643 of LNCS, pages 306--320. Springer, 2009.
[22]
A. Goel, S. Krstic, and C. Tinelli. Ground interpolation for combined theories. In CADE, volume 5663 of Lecture Notes in Computer Science, pages 183--198. Springer, 2009.
[23]
A. Griggio. A Practical Approach to Satisfiability Modulo Linear Integer Arithmetic. JSAT, 8:1--27, January 2012.
[24]
A. Griggio, T. T. H. Le, and R. Sebastiani. Efficient interpolant generation in satisfiability modulo linear integer arithmetic. In TACAS, volume 6605 of LNCS, pages 143--157. Springer, 2011.
[25]
M. Heizmann, J. Hoenicke, and A. Podelski. Nested interpolants. In POPL, pages 471--482. ACM, 2010.
[26]
T. A. Henzinger, R. Jhala, R. Majumdar, and K. L. McMillan. Abstractions from proofs. In 31st POPL, 2004.
[27]
K. Hoder, L. Kovács, and A. Voronkov. Interpolation and symbol elimination in vampire. In IJCAR, volume 6173 of LNCS, pages 188--195. Springer, 2010.
[28]
K. Hoder, L. Kovács, and A. Voronkov. Playing in the grey area of proofs. In POPL, pages 259--272. ACM, 2012.
[29]
C. Ihlemann, S. Jacobs, and V. Sofronie-Stokkermans. On local reasoning in verification. In TACAS, pages 265--281, 2008.
[30]
S. Jacobs. Incremental instance generation in local reasoning. In CAV, volume 5643 of LNCS, pages 368--382. Springer, 2009.
[31]
R. Jhala and K. L. McMillan. A practical and complete approach to predicate refinement. In TACAS, volume 3920 of LNCS, pages 459--473. Springer, 2006.
[32]
R. Jhala and K. L. McMillan. Interpolant-based transition relation approximation. Logical Methods in Computer Science, 3(4), 2007.
[33]
B. Jónsson. Universal relational systems. Math. Scand., 4:193--208, 1956.
[34]
D. Kapur, R. Majumdar, and C. G. Zarba. Interpolation for data structures. In SIGSOFT FSE, pages 105--116. ACM, 2006.
[35]
D. Kroening and G. Weissenbacher. Interpolation-Based Software Verification with Wolverine. In CAV, volume 6806 of LNCS, pages 573--578. Springer, 2011.
[36]
S. K. Lahiri and S. Qadeer. Back to the future: revisiting precise program verification using SMT solvers. In POPL, pages 171--182. ACM, 2008.
[37]
J. McCarthy. Towards a mathematical science of computation. In IFIP Congress, pages 21--28, 1962.
[38]
K. L. McMillan. Interpolation and SAT-Based Model Checking. In CAV, volume 2725 of LNCS, pages 1--13. Springer, 2003.
[39]
K. L. McMillan. An interpolating theorem prover. Theor. Comput. Sci., 345(1):101--121, 2005.
[40]
K. L. McMillan. Lazy abstraction with interpolants. In CAV, volume 4144 of LNCS, pages 123--136. Springer, 2006.
[41]
K. L. McMillan. Quantified invariant generation using an interpolating saturation prover. In TACAS, volume 4963 of LNCS, pages 413--427. Springer, 2008.
[42]
G. Nelson. Verifying reachability invariants of linked structures. In POPL, pages 38--47. ACM, 1983.
[43]
A. Podelski and T. Wies. Counterexample-guided focus. In POPL, pages 249--260. ACM, 2010.
[44]
T. W. Reps, S. Sagiv, and G. Yorsh. Symbolic implementation of the best transformer. In VMCAI, volume 2937 of LNCS, pages 252--266. Springer, 2004.
[45]
A. Rybalchenko and V. Sofronie-Stokkermans. Constraint solving for interpolation. In VMCAI, volume 4349 of LNCS, pages 346--362. Springer, 2007.
[46]
M. Sagiv, T. Reps, and R. Wilhelm. Parametric shape analysis via 3-valued logic. ACM TOPLAS, 24(3):217--298, 2002.
[47]
V. Sofronie-Stokkermans. Hierarchic reasoning in local theory extensions. In CADE, pages 219--234, 2005.
[48]
V. Sofronie-Stokkermans. Interpolation in local theory extensions. Logical Methods in Computer Science, 4(4), 2008.
[49]
N. Totla and T. Wies. Complete instantiation-based interpolation. Technical Report TR2012--950, New York University, 2012.
[50]
T. Wies, M. Mu\ niz, and V. Kuncak. An efficient decision procedure for imperative tree data structures. In CADE, volume 6803 of LNCS, pages 476--491. Springer, 2011.
[51]
G. Yorsh and M. Musuvathi. A combination method for generating interpolants. In CADE, volume 3632 of LNCS, pages 353--368, 2005.

Cited By

View all
  • (2023)Interpolation Results for Arrays with Length and MaxDiffACM Transactions on Computational Logic10.1145/358716124:4(1-33)Online publication date: 9-Jun-2023
  • (2017)Complexity verification using guided theorem enumerationACM SIGPLAN Notices10.1145/3093333.300986452:1(639-652)Online publication date: 1-Jan-2017
  • (2017)Complexity verification using guided theorem enumerationProceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages10.1145/3009837.3009864(639-652)Online publication date: 1-Jan-2017
  • Show More Cited By

Recommendations

Comments

Information & Contributors

Information

Published In

cover image ACM Conferences
POPL '13: Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages
January 2013
586 pages
ISBN:9781450318327
DOI:10.1145/2429069
  • cover image ACM SIGPLAN Notices
    ACM SIGPLAN Notices  Volume 48, Issue 1
    POPL '13
    January 2013
    561 pages
    ISSN:0362-1340
    EISSN:1558-1160
    DOI:10.1145/2480359
    Issue’s Table of Contents
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

In-Cooperation

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 23 January 2013

Permissions

Request permissions for this article.

Check for updates

Author Tags

  1. craig interpolants
  2. crdecision procedures
  3. crsatisfiability module theories
  4. data structures
  5. program analysis

Qualifiers

  • Research-article

Conference

POPL '13
Sponsor:

Acceptance Rates

Overall Acceptance Rate 860 of 4,328 submissions, 20%

Upcoming Conference

POPL '26

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)5
  • Downloads (Last 6 weeks)0
Reflects downloads up to 19 Feb 2025

Other Metrics

Citations

Cited By

View all
  • (2023)Interpolation Results for Arrays with Length and MaxDiffACM Transactions on Computational Logic10.1145/358716124:4(1-33)Online publication date: 9-Jun-2023
  • (2017)Complexity verification using guided theorem enumerationACM SIGPLAN Notices10.1145/3093333.300986452:1(639-652)Online publication date: 1-Jan-2017
  • (2017)Complexity verification using guided theorem enumerationProceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages10.1145/3009837.3009864(639-652)Online publication date: 1-Jan-2017
  • (2017)Splitting Proofs for InterpolationAutomated Deduction – CADE 2610.1007/978-3-319-63046-5_18(291-309)Online publication date: 11-Jul-2017
  • (2016)Complete Instantiation-Based InterpolationJournal of Automated Reasoning10.1007/s10817-016-9371-757:1(37-65)Online publication date: 1-Jun-2016
  • (2016)Proof Tree Preserving Tree InterpolationJournal of Automated Reasoning10.1007/s10817-016-9365-557:1(67-95)Online publication date: 1-Jun-2016
  • (2016)Labelled Interpolation Systems for Hyper-Resolution, Clausal, and Local ProofsJournal of Automated Reasoning10.1007/s10817-016-9364-657:1(3-36)Online publication date: 1-Jun-2016
  • (2016)Guiding Craig interpolation with domain-specific abstractionsActa Informatica10.1007/s00236-015-0236-z53:4(387-424)Online publication date: 1-Jun-2016
  • (2016)Effectively Propositional InterpolantsComputer Aided Verification10.1007/978-3-319-41540-6_12(210-229)Online publication date: 13-Jul-2016
  • (2016)On Interpolation and Symbol Elimination in Theory ExtensionsProceedings of the 8th International Joint Conference on Automated Reasoning - Volume 970610.1007/978-3-319-40229-1_19(273-289)Online publication date: 27-Jun-2016
  • Show More Cited By

View Options

Login options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Figures

Tables

Media

Share

Share

Share this Publication link

Share on social media