Spatial interpolants

Aws Albargouthi, Josh Berdine, Byron Cook, Zachary Kincaid

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

10 Scopus citations

Abstract

We propose SplInter, a new technique for proving properties of heap-manipulating programs that marries (1) a new separation logic–based analysis for heap reasoning with (2) an interpolation-based technique for refining heap-shape invariants with data invariants. SplInter is property directed, precise, and produces counterexample traces when a property does not hold. Using the novel notion of spatial interpolants modulo theories, SplInter can infer complex invariants over general recursive predicates, e.g., of the form all elements in a linked list are even or a binary tree is sorted. Furthermore, we treat interpolation as a black box, which gives us the freedom to encode data manipulation in any suitable theory for a given program (e.g., bit vectors, arrays, or linear arithmetic), so that our technique immediately benefits from any future advances in SMT solving and interpolation.

Original languageEnglish (US)
Title of host publicationProgramming Languages and Systems - 24th European Symposiumon Programming, ESOP 2015 held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, Proceedings
EditorsJan Vitek
PublisherSpringer Verlag
Pages634-660
Number of pages27
ISBN (Electronic)9783662466681
DOIs
StatePublished - Jan 1 2015
Externally publishedYes
Event24th European Symposium on Programming, ESOP 2015 held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015 - London, United Kingdom
Duration: Apr 11 2015Apr 18 2015

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume9032
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other24th European Symposium on Programming, ESOP 2015 held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015
CountryUnited Kingdom
CityLondon
Period4/11/154/18/15

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Spatial interpolants'. Together they form a unique fingerprint.

  • Cite this

    Albargouthi, A., Berdine, J., Cook, B., & Kincaid, Z. (2015). Spatial interpolants. In J. Vitek (Ed.), Programming Languages and Systems - 24th European Symposiumon Programming, ESOP 2015 held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, Proceedings (pp. 634-660). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 9032). Springer Verlag. https://doi.org/10.1007/978-3-662-46669-8_26