Satisfiability Modulo Abstraction for Separation Logic with Linked Lists
File(s)
Date
2014-02-13Author
Thakur, Aditya
Breck, Jason
Reps, Thomas
Publisher
University of Wisconsin-Madison Department of Computer Sciences
Metadata
Show full item recordAbstract
Separation logic is an expressive logic for reasoning about heap
structures in programs. This paper presents a semi-decision procedure
for deciding unsatisfiability of formulas in a fragment of separation
logic that includes predicates describing 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 other
existing approaches.
Subject
abstract interpretation
separation logic
canonical abstraction
semi-decision procedure
Permanent Link
http://digital.library.wisc.edu/1793/68280Citation
TR1800