Deciding Boolean Separation Logic via Small Models (Technical Report)

TL;DR

This work introduces a decision procedure for boolean separation logic (BSL) that supports arbitrary boolean combinations, guarded negations, and common inductive predicates for lists. It hinges on a small-model property and a translation-based approach to SMT, using footprint-based reasoning to handle separating conjunctions without heavy quantification. The authors implement the Astral solver and demonstrate competitive performance on symbolic-heap benchmarks and notable capability beyond that fragment, while also establishing PSPACE-hardness for BSL with guarded negation. The result is a practical path toward integrating richer separation-logic reasoning with SMT-based verification, enabling efficient handling of complex memory-manipulating programs. Overall, the approach advances both the theoretical and practical landscape of combining SL with SMT, offering scalable decision procedures for a significantly more expressive fragment than prior work.

Abstract

We present a novel decision procedure for a fragment of separation logic (SL) with arbitrary nesting of separating conjunctions with boolean conjunctions, disjunctions, and guarded negations together with a support for the most common variants of linked lists. Our method is based on a model-based translation to SMT for which we introduce several optimisations$\unicode{x2013}$the most important of them is based on bounding the size of predicate instantiations within models of larger formulae, which leads to a much more efficient translation of SL formulae to SMT. Through a series of experiments, we show that, on the frequently used symbolic heap fragment, our decision procedure is competitive with other existing approaches, and it can outperform them outside the symbolic heap fragment. Moreover, our decision procedure can also handle some formulae for which no decision procedure has been implemented so far.

Figures (4)

• Figure 1: The semantics of the separation logic. The existential quantifier is used for the definition of the semantics of inductive predicates and it is not a part of our fragment.
• Figure 2: An illustration of reductions of atomic models of inductive predicates. Removed heap locations are red, removed edges are dotted, and added edges are highlighted.
• Figure 3: An illustration of the bound computation for the path $\sigma$ from $a$ to $c$ on a fragment of SL-graph of $\varphi \triangleq \bigl(\mathsf{sls}(a, b) \ast b \mapsto c \ast c \mapsto d \ast \mathsf{sls}(d, a)\bigr) \land \neg \bigl(\mathsf{sls}(a,c) \ast \mathsf{sls}(c,a)\bigr)$. The highlighted edges denote the paths used to determine the bound $[1, 3]$.
• Figure 4: A comparison of Astral with cvc5 and GRASShopper on randomly generated formulae. Times are in seconds, axes are logarithmic. The timeout was set to 60 s.

Theorems & Definitions (51)

• lemma thmcounterlemma: Chunk decomposition
• lemma thmcounterlemma
• definition thmcounterdefinition
• theorem thmcountertheorem
• theorem thmcountertheorem: Small-model property
• definition thmcounterdefinition: Inverse translation
• theorem thmcountertheorem: Translation correctness
• lemma thmcounterlemma
• lemma thmcounterlemma
• theorem thmcountertheorem