Spatial Interpolants

TL;DR

Splinter is a novel technique combining separation logic and interpolation to verify heap-manipulating programs, capable of inferring complex invariants and refining properties with counterexamples, adaptable to various theories.

Contribution

Introducing spatial interpolants modulo theories, Splinter advances heap analysis by enabling property-directed, precise invariant inference over recursive data structures.

Findings

Can infer complex recursive invariants like sorted trees and even lists.

Produces counterexamples when properties do not hold.

Flexible to different theories via black-box interpolation.

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.