Complete instantiation-based interpolation

Nishant Totla, Thomas Wies

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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.

Original languageEnglish (US)
Title of host publicationPOPL 2013 - Proceedings of 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
Pages537-548
Number of pages12
DOIs
StatePublished - 2013
Event40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2013 - Rome, Italy
Duration: Jan 23 2013Jan 25 2013

Other

Other40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2013
CountryItaly
CityRome
Period1/23/131/25/13

Fingerprint

Interpolation
Surface mount technology
Formal methods
Data structures

Keywords

  • craig interpolants
  • crdecision procedures
  • crsatisfiability module theories
  • data structures
  • program analysis

ASJC Scopus subject areas

  • Software

Cite this

Totla, N., & Wies, T. (2013). Complete instantiation-based interpolation. In POPL 2013 - Proceedings of 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (pp. 537-548) https://doi.org/10.1145/2429069.2429132

Complete instantiation-based interpolation. / Totla, Nishant; Wies, Thomas.

POPL 2013 - Proceedings of 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. 2013. p. 537-548.

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Totla, N & Wies, T 2013, Complete instantiation-based interpolation. in POPL 2013 - Proceedings of 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. pp. 537-548, 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2013, Rome, Italy, 1/23/13. https://doi.org/10.1145/2429069.2429132
Totla N, Wies T. Complete instantiation-based interpolation. In POPL 2013 - Proceedings of 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. 2013. p. 537-548 https://doi.org/10.1145/2429069.2429132
Totla, Nishant ; Wies, Thomas. / Complete instantiation-based interpolation. POPL 2013 - Proceedings of 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. 2013. pp. 537-548
@inproceedings{ac0fcde98c6a4ff8b04d3419f1f5a816,
title = "Complete instantiation-based interpolation",
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.",
keywords = "craig interpolants, crdecision procedures, crsatisfiability module theories, data structures, program analysis",
author = "Nishant Totla and Thomas Wies",
year = "2013",
doi = "10.1145/2429069.2429132",
language = "English (US)",
isbn = "9781450318327",
pages = "537--548",
booktitle = "POPL 2013 - Proceedings of 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages",

}

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

SP - 537

EP - 548

BT - POPL 2013 - Proceedings of 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

ER -