TY - GEN
T1 - Spatial interpolants
AU - Albargouthi, Aws
AU - Berdine, Josh
AU - Cook, Byron
AU - Kincaid, Zachary
N1 - Publisher Copyright:
© Springer-Verlag Berlin Heidelberg 2015.
PY - 2015
Y1 - 2015
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=84926648099&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84926648099&partnerID=8YFLogxK
U2 - 10.1007/978-3-662-46669-8_26
DO - 10.1007/978-3-662-46669-8_26
M3 - Conference contribution
AN - SCOPUS:84926648099
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 634
EP - 660
BT - 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
A2 - Vitek, Jan
PB - Springer Verlag
T2 - 24th European Symposium on Programming, ESOP 2015 held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015
Y2 - 11 April 2015 through 18 April 2015
ER -