Satisfiability Modulo Abstraction for Separation Logic with Linked Lists
Aditya Thakur, Jason Breck, and Thomas Reps
Separation logic is an expressive logic for reasoning about heap
structures in programs. This paper presents a semi-decision procedure
for checking unsatisfiability of formulas in a fragment of separation
logic that includes points-to assertions (x→y),
acyclic-list-segment assertions (ls(x,y)), logical-and, logical-or,
separating conjunction, and septraction (the DeMorgan-dual of
separating implication). The fragment that we consider allows
negation at leaves, and includes formulas that lie outside other
separation-logic fragments considered in the literature.
The semi-decision procedure is designed using concepts from abstract
interpretation. The procedure uses an abstract domain of shape graphs
to represent a set of heap structures, and computes an abstraction
that over-approximates the set of satisfying models of a given
formula. If the over-approximation is empty, then the formula is
unsatisfiable.
We have implemented the method, and evaluated it on a set of formulas
taken from the literature. The implementation is able to establish
the unsatisfiability of formulas that cannot be handled by previous
approaches.
(Click here to access the paper:
PDF.)
University of Wisconsin