Complete Instantiation-Based Interpolation

Nishant Totla, Thomas Wies

Research output: Contribution to journalArticlepeer-review


Craig interpolation has been a valuable tool 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 a 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.

Original languageEnglish (US)
Pages (from-to)37-65
Number of pages29
JournalJournal of Automated Reasoning
Issue number1
StatePublished - Jun 1 2016


  • Amalgamation
  • Craig interpolation
  • Local theory extensions
  • Program verification
  • Satisfiability modulo theories

ASJC Scopus subject areas

  • Software
  • Computational Theory and Mathematics
  • Artificial Intelligence


Dive into the research topics of 'Complete Instantiation-Based Interpolation'. Together they form a unique fingerprint.

Cite this