Satisfiability modulo abstraction for separation logic with linked lists

Thakur, Aditya V. and Breck, Jason and Reps, Thomas W.
2014 International Symposium on Model Checking of Software (SPIN), 2014

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.

PDF     ACM©    

@inproceedings{thakur_etal_SPIN14,
  author = {Thakur, Aditya V. and Breck, Jason and Reps, Thomas W.},
  title = {Satisfiability modulo abstraction for separation logic with linked
                 lists},
  booktitle = {2014 International Symposium on Model Checking of Software ({SPIN})},
  year = {2014},
  pages = {58--67},
  doi = {10.1145/2632362.2632376},
  publisher = {ACM}
}