Pagel, J., & Zuleger, F. (2022). Strong-separation Logic (Extended Version). ACM Letters on Programming Languages and Systems, 44(3), 1–40. https://doi.org/10.1145/3498847
E192-04 - Forschungsbereich Formal Methods in Systems Engineering
-
Journal:
ACM Letters on Programming Languages and Systems
-
ISSN:
0164-0925
-
Date (published):
Sep-2022
-
Number of Pages:
40
-
Publisher:
ASSOC COMPUTING MACHINERY
-
Peer reviewed:
Yes
-
Keywords:
(bi-)abduction; Decision procedure; magic wand
en
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.