TY - GEN
T1 - Complete instantiation-based interpolation
AU - Totla, Nishant
AU - Wies, Thomas
PY - 2013
Y1 - 2013
N2 - 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.
AB - 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.
KW - craig interpolants
KW - crdecision procedures
KW - crsatisfiability module theories
KW - data structures
KW - program analysis
UR - http://www.scopus.com/inward/record.url?scp=84874129799&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84874129799&partnerID=8YFLogxK
U2 - 10.1145/2429069.2429132
DO - 10.1145/2429069.2429132
M3 - Conference contribution
AN - SCOPUS:84874129799
SN - 9781450318327
T3 - Conference Record of the Annual ACM Symposium on Principles of Programming Languages
SP - 537
EP - 548
BT - POPL 2013 - Proceedings of 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
T2 - 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2013
Y2 - 23 January 2013 through 25 January 2013
ER -