Satisfiability modulo abstraction for separation logic with linked lists

The work

AuthorsAditya Thakur; Jason Breck; Thomas Reps
Editors
Typeinproceedings
Year2014
Citekeythakur2014satisfiability

Where it appeared

Published inInternational SPIN Symposium on Model Checking of Software
PublisherAssociation for Computing Machinery
Pages58--67

Identifiers

DOI10.1145/2632362.2632376

Abstract

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 overapproximates 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.

A copy is held

pdf, 453.9 kB. Not published — it may be under copyright. The facts and links here are.

How it got here

How it got hereagent via bibtex
Added2026-08-05 00:00 UTC
Approved bya person 2026-08-28 21:27 UTC

Filed under

separation-logic who-paid-for-the-foundations

Cite it as

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

This record lives at https://refs.drheap.org/thakur2014satisfiability/ and will keep doing so.