# Reasoning in the Bernays-Schoenfinkel-Ramsey Fragment of Separation Logic

arXiv: https://arxiv.org/abs/1610.04707 · HTML: https://mlsanity.com/paper/1610.04707/

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 15 Oct 2016.

## Built on by (most cited first, 2 of 2)

- [Shield Synthesis for LTL Modulo Theories](https://mlsanity.com/paper/2406.04184/) (2024)
- [A separation logic for sequences in pointer programs and its decidability](https://mlsanity.com/paper/2301.06237/) (2023)

## Abstract (arXiv)

Separation Logic (SL) is a well-known assertion language used in Hoare-style modular proof systems for programs with dynamically allocated data structures. In this paper we investigate the fragment of first-order SL restricted to the Bernays-Schoenfinkel-Ramsey quantifier prefix exists^*forall^*, where the quantified variables range over the set of memory locations. When this set is uninterpreted (has no associated theory) the fragment is PSPACE-complete, which matches the complexity of the quantifier-free fragment. However, SL becomes undecidable when the quantifier prefix belongs to exists^*forall^*exists^* instead, or when the memory locations are interpreted as integers with linear arithmetic constraints, thus setting a sharp boundary for decidability within SL. We have implemented a decision procedure for the decidable fragment of exists^*forall^*SL as a specialized solver inside a DPLL(T) architecture, within the CVC4 SMT solver. The evaluation of our implementation was carried out using two sets of verification conditions, produced by (i) unfolding inductive predicates, and (ii) a weakest precondition-based verification condition generator. Experimental data shows that automated quantifier instantiation has little overhead, compared to manual model-based instantiation.