Strong-separation logic
The work
| Authors | Jens Pagel; Florian Zuleger |
|---|---|
| Editors | |
| Type | article |
| Year | 2022 |
| Citekey | pagel2022strong |
Where it appeared
| Published in | ACM Transactions on Programming Languages and Systems (TOPLAS) |
|---|---|
| Volume | 44 |
| Issue | 3 |
| Pages | 16:1--16:40 |
Identifiers
| DOI | 10.1145/3498847 |
|---|
Abstract
Most automated verifiers for separation logic are based on the symbolic-heap fragment, which disallows both the magic-wand operator and the application of classical Boolean operators to spatial formulas. This is not surprising, as support for the magic wand quickly leads to undecidability, especially when combined with inductive predicates for reasoning about data structures. To circumvent these undecidability results, we propose assigning a more restrictive semantics to the separating conjunction. We argue that the resulting logic, strong-separation logic, can be used for symbolic execution and abductive reasoning just like “standard” separation logic, while remaining decidable even in the presence of both the magic wand and inductive predicates (we consider a list-segment predicate and a tree predicate)—a combination of features that leads to undecidability for the standard semantics.
A copy is held
pdf, 1.4 MB. Not published — it may be under copyright. The facts and links here are.
How it got here
| How it got here | agent via bibtex |
|---|---|
| Added | 2026-08-05 00:00 UTC |
| Approved by | a person 2026-08-26 09:46 UTC |
Filed under
Cite it as
@article{pagel2022strong,
title = {Strong-separation logic},
author = {Jens Pagel and Florian Zuleger},
year = {2022},
journal = {ACM Transactions on Programming Languages and Systems (TOPLAS)},
volume = {44},
number = {3},
pages = {16:1--16:40},
doi = {10.1145/3498847},
}
This record lives at https://refs.drheap.org/pagel2022strong/ and will keep doing so.