# A Decision Procedure for Separation Logic in SMT

Andrew Reynolds, Radu Iosif, Cristina Serban, Tim King

► To cite this version:

Andrew Reynolds, Radu Iosif, Cristina Serban, Tim King. A Decision Procedure for Separation Logic in SMT. Automated Technology for Verification and Analysis 14th International Symposium (ATVA 2016), Oct 2016, Chiba, Japan. pp.244-261, 10.1007/978-3-319-46520-3_16 . hal-01418883

HAL Id: hal-01418883

https://hal.science/hal-01418883

Submitted on 17 Dec 2016

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

Public Domain
# A Decision Procedure for Separation Logic in SMT

Andrew Reynolds¹, Radu Iosif², Cristina Serban², and Tim King³

¹ The University of Iowa

² Université de Grenoble Alpes, CNRS, VERIMAG

³ Google Inc.

**Abstract.** This paper presents a complete decision procedure for the entire quantifier-free fragment of Separation Logic (SL) interpreted over heaplets with data elements ranging over a parametric multi-sorted (possibly infinite) domain. The algorithm uses a combination of theories and is used as a specialized solver inside a DPLL(T) architecture. A prototype was implemented within the CVC4 SMT solver. Preliminary evaluation suggests the possibility of using this procedure as a building block of a more elaborate theorem prover for SL with inductive predicates, or as back-end of a bounded model checker for programs with low-level pointer and data manipulations.

## 1 Introduction

Separation Logic (SL) [21] is a logical framework for describing dynamically allocated mutable data structures generated by programs that use pointers and low-level memory allocation primitives. The logics in this framework are used by a number of academic (SPACE INVADER [4]), and industrial (INFER [7]) tools for program verification. The main reason for choosing to work within the SL framework is its ability to provide compositional proofs of programs, based on the principle of *local reasoning*: analyzing different parts of the program (e.g. functions, threads), that work on *disjoint parts of the heap*, and combining the analysis results a posteriori.

The main ingredients of SL are: (i) the *separating conjunction* $\phi * \psi$, which asserts that $\phi$ and $\psi$ hold for separate portions of the memory (heap), and (ii) the *magic wand* $\varphi * \psi$, which asserts that any extension of the heap by a disjoint heap that satisfies $\varphi$ must satisfy $\psi$. Consider, for instance, a memory configuration (heap), in which two cells are allocated, and pointed to by the program variables x and y, respectively, where the x cell has an outgoing selector field to the y cell, and vice versa. The heap can be split into two disjoint parts, each containing exactly one cell, and described by an atomic proposition $x \mapsto y$ and $y \mapsto x$, respectively. Then the entire heap is described by the formula $x \mapsto y * y \mapsto x$, which reads "x points to y and, separately, y points to x".

The expressive power of SL comes with the inherent difficulty of automatically reasoning about the satisfiability of its formulae, as required by push-button program analysis tools. Indeed, SL becomes undecidable in the presence of first-order quantification, even when the fragment uses only points-to predicates, without the separating conjunction or the magic wand [9]. Moreover, the quantifier-free fragment with no data constraints, using only points-to predicates $x \mapsto (y,z)$, where x, y and z are interpreted as
memory addresses, is PSPACE-complete, due to the implicit quantification over memory partitions, induced by the semantics of the separation logic connectives [9].

This paper presents a decision procedure for quantifier-free SL which is entirely parameterized by a base theory T of heap locations and data, i.e. the sorts of memory addresses and their contents can be chosen from a large variety of available theories handled by Satisfiability Modulo Theories (SMT) solvers, such as linear integer (real) arithmetic, strings, sets, uninterpreted functions, etc. Given a base theory T, we call SL(T) the set of separation logic formulae built on top of T, by considering points-to predicates and the separation logic connectives.

**Contributions** First, we show that the satisfiability problem for the quantifier-free fragment of SL(T) is PSPACE-complete, provided that the satisfiability of the quantifier-free fragment of the base theory T is in PSPACE. Our method is based on a semantics-preserving translation of SL(T) into second-order T formulae with quantifiers over a domain of sets and uninterpreted functions, whose cardinality is polynomially bound by the size of the input formula. For the fragment of T formulae produced by the translation from SL(T), we developed a lazy quantifier instantiation method, based on counterexample-driven refinement. We show that the quantifier instantiation algorithm is sound, complete and terminates on the fragment under consideration. We present our algorithm for the satisfiability of quantifier-free SL(T) logics as a component of a DPLL(T) architecture, which is widely used by modern SMT solvers. We have implemented the technique as a subsolver of the CVC4 SMT solver [2] and carried out experiments that handle non-trivial examples quite effectively. Applications of our procedure include:

1. Integration within theorem provers for SL with inductive predicates. Most inductive provers for SL use a high-level proof search strategy relying on a separate decision procedure for entailments in the non-inductive fragment, used to simplify the proof obligations, by discharging the non-inductive parts of both left- and right-hand sides, and attain an inductive hypothesis [6]. Due to the hard problem of proving entailments in the non-inductive fragment of SL, these predicates use very simple non-inductive formulae (a list of points-to propositions connected with separating conjunction), for which entailments are proved by syntactic substitutions and matching. Our work aims at extending the language of inductive SL solvers, by outsourcing entailments in a generic non-inductive fragment to a specialized procedure. To this end, we conducted experiments on several entailments corresponding to finite unfoldings of inductive predicates used in practice (Section 6).

2. Use as back-end of a bounded model checker for programs with pointer and data manipulations, based on a complete weakest precondition calculus that involves the magic wand connective [15]. To corroborate this hypothesis, we tested our procedure on verification conditions automatically generated by applying the weakest precondition calculus described in [15] to several program fragments (Section 6).

**Related Work** The study of the algorithmic properties of Separation Logic [21] has produced an extensive body of literature over time. We need to distinguish between SL with inductive predicates and restrictive non-inductive fragments, and SL without inductive predicates, which is the focus of this paper.
Regarding SL with fixed inductive predicates, Perez and Rybalchenko [16] define a theorem proving framework relying on a combination of SL inference rules dealing with singly-linked lists only, and a superposition calculus dealing with equalities and aliasing between variables. Concerning SL with generic user-provided inductive predicates, the theorem prover CYCLIST [6] builds entailment proofs using a sequent calculus. More recently, the tool SLIDE [14] reduces the entailment between inductive predicates to an inclusion between tree automata. The great majority of these inductive provers focus on applying induction strategies efficiently, and consider a very simple fragment of non-inductive SL formulae, typically conjunctions of equalities and disequalities between location variables and separated points-to predicates, without negations or the magic wand. On a more general note, the tool SPEN [10] considers also arithmetic constraints between the data elements in the memory cells, but fixes the shape of the user-defined predicates.

The idea of applying SMT techniques to decide satisfiability of SL formulae is not new. In their work, Piskac, Wies and Zufferey translate from SL with singly-linked list segments [17] and trees [18], respectively, into first-order logics (GRASS and GRIT) that are decidable in NP. The fragment handled in this paper is incomparable to the logics GRASS [17] and GRIT [18]. On one hand, we do not consider predicates defining recursive data structures, such as singly-linked lists. On the other hand, we deal with the entire quantifier-free fragment of SL, including arbitrary nesting of the magic wand, separating conjunction and classical boolean connectives. As a result, the decision problem we consider is PSPACE-complete, due to the possibility of arbitrary nesting of the boolean and SL connectives. To the best of our knowledge, our implementation is also the first to enable theory combination involving SL, in a fine-grained fashion, directly within the DPLL(T) loop.

The first theoretical results on decidability and complexity of SL without inductive predicates were given by Calcagno, Yang and O'Hearn [9]. They show that the quantifier-free fragment of SL without data constraints is PSPACE-complete by an argument that enumerates a finite (yet large) set of heap models. Their argument shows also the difficulty of the problem, however it cannot be directly turned into an effective decision procedure, because of the ineffectiveness of model enumeration. Building up on this small model property for the quantifier-free fragment of SL, a translation to first-order logic over uninterpreted sorts with empty signature is described in [8]. This translation is very similar to our translation to multi-sorted second-order logic, the main difference being using bounded tuples instead of sets of bounded cardinality. It also provides a decision procedure, though no implementation is available for comparison. A more elaborate tableau-based decision procedure is described by Méry and Galmiche [11]. This procedure generates verification conditions on-demand, but here no data constraints are considered, either.

Our procedure relies on a decision procedure for quantifier-free parametric theory of sets and on-demand techniques for quantifier instantiation. Decision procedures for the theory of sets in SMT are given in [23, 1]. Techniques for model-driven quantifier instantiation were introduced in the context of SMT in [13], and have been developed recently in [19, 5].
## 2 Preliminaries

We consider formulae in multi-sorted first-order logic, over a signature $\Sigma$ consisting of a countable set of sort symbols and a set of function symbols. We assume that signatures always include a boolean sort `Bool` with constants $\top$ and $\bot$ denoting true and false respectively, and that each sort $\sigma$ is implicitly equipped with an equality predicate $\approx$ over $\sigma \times \sigma$. Moreover, we may assume without loss of generality that equality is the only predicate belonging to $\Sigma$, since we can model other predicate symbols as function symbols with return sort `Bool`<fnref n="4" />.

We consider a set `Var` of first-order variables, with associated sorts, and denote by $\varphi(\mathbf{x})$ the fact that the free variables of the formula $\varphi$ belong to $\mathbf{x} \subseteq \text{Var}$. Given a signature $\Sigma$, well-sorted terms, atoms, literals, and formulae are defined as usual, and referred to respectively as $\Sigma$-terms. We denote by $\phi[\varphi]$ the fact that $\varphi$ is a subformula (subterm) of $\phi$ and by $\phi[\psi/\varphi]$ the result of replacing $\varphi$ with $\psi$ in $\phi$. We write $\forall x.\varphi$ to denote universal quantification over variable $x$, where $x$ occurs as a free variable in $\varphi$. If $\mathbf{x} = (x_1, \dots, x_n)$ is a tuple of variables, we write $\forall \mathbf{x} \varphi$ as an abbreviation of $\forall x_1 \dots \forall x_n \varphi$. We say that a $\Sigma$-term is ground if it contains no free variables. We assume that $\Sigma$ contains an if-then-else operator $ite(b, t, u)$, of sort `Bool` $\times \sigma \times \sigma \to \sigma$, for each sort $\sigma$, that evaluates to $t$ if $b$ is true, and to $u$, otherwise.

A $\Sigma$-interpretation $\mathcal{I}$ maps: (i) each set sort symbol $\sigma \in \Sigma$ to a non-empty set $\sigma^I$, the domain of $\sigma$ in $\mathcal{I}$, (ii) each function symbol $f \in \Sigma$ of sort $\sigma_1 \times \dots \times \sigma_n \to \sigma$ to a total function $f^I$ of sort $\sigma_1^I \times \dots \times \sigma_n^I \to \sigma^I$ if $n > 0$, and to an element of $\sigma^I$ if $n = 0$, and (iii) each variable $x \in \mathbf{x}$ to an element of $\sigma_x^I$, where $\sigma_x$ is the sort symbol associated with $x$. We denote by $t^I$ the interpretation of a term $t$ induced by the mapping $\mathcal{I}$. The satisfiability relation between $\Sigma$-interpretations and $\Sigma$-formulae, written $\mathcal{I} \models \varphi$, is defined inductively, as usual. We say that $\mathcal{I}$ is a model of $\varphi$ if $\mathcal{I} \models \varphi$.

A first-order theory is a pair $T = (\Sigma, \mathbf{I})$ where $\Sigma$ is a signature and $\mathbf{I}$ is a non-empty set of $\Sigma$-interpretations, the models of $T$. For a formula $\varphi$, we denote by $[[\varphi]]_T = \{\mathcal{I} \in \mathbf{I} | \mathcal{I} \models \varphi\}$ its set of $T$-models. A $\Sigma$-formula $\varphi$ is $T$-satisfiable if $[[\varphi]]_T \neq \emptyset$, and $T$-unsatisfiable otherwise. A $\Sigma$-formula $\varphi$ is $T$-valid if $[[\varphi]]_T = \mathbf{I}$, i.e. if $\neg \varphi$ is $T$-unsatisfiable. A formula $\varphi$ $T$-entails a $\Sigma$-formula $\psi$, written $\varphi \models_T \psi$, if every model of $T$ that satisfies $\varphi$ also satisfies $\psi$. The formulae $\varphi$ and $\psi$ are $T$-equivalent if $\varphi \models_T \psi$ and $\psi \models_T \varphi$, and equisatisfiable (in $T$) if $\psi$ is $T$-satisfiable if and only if $\varphi$ is $T$-satisfiable. Furthermore, formulas $\varphi$ and $\psi$ are equivalent (up to $\mathbf{k}$) if they are satisfied by the same set of models (when restricted to the interpretation of variables $\mathbf{k}$). The $T$-satisfiability problem asks, given a $\Sigma$-formula $\varphi$, whether $[[\varphi]]_T \neq \emptyset$, i.e. whether $\varphi$ has a $T$-model.

### 2.1 Separation Logic

In the remainder of the paper we fix a theory $T = (\Sigma, \mathbf{I})$, such that the $T$-satisfiability for the language of quantifier-free boolean combinations of equalities and disequalities between $\Sigma$-terms is decidable. We fix two sorts `Loc` and `Data` from $\Sigma$, with no restriction other than the fact that `Loc` is always interpreted as a countably infinite set. We refer to

<footnote n="4">⁴ For brevity, we may write $p(t)$ as shorthand for $p(t) \approx \top$, where $p$ is a function into `Bool`.</footnote>
Separation Logic for T, written SL(T), as the set of formulae generated by the syntax:

$$ \phi := t \approx u | t \mapsto u | \text{emp} | \phi_1 * \phi_2 | \phi_1 \leftarrow \phi_2 | \phi_1 \wedge \phi_2 | \neg \phi_1 $$

where t and u are well-sorted Σ-terms and that for any atomic proposition t ↦→ u, t is of sort Loc and u is of sort Data. Also, we consider that Σ has a constant nil of sort Loc, with the meaning that t ↦→ u never holds when t ≈ nil. In the following, we write φ ∨ ψ for ¬(¬φ ∧ ¬ψ) and φ ⇒ ψ for ¬φ ∨ ψ.

Given an interpretation I, a heap is a finite partial mapping h : Loc^I → fin Data^I. For a heap h, we denote by dom(h) its domain. For two heaps h₁ and h₂, we write h₁#h₂ for dom(h₁) ∩ dom(h₂) = ∅ and h = h₁ ⊎ h₂ for h₁#h₂ and h = h₁ ∪ h₂. For an interpretation I, a heap h : Loc^I → fin Data^I and a SL(T) formula φ, we define the satisfaction relation I, h |= SL φ inductively, as follows:

$$ \begin{align*} 
I, h &\models_{\text{SL}} \text{emp} &\iff h = \emptyset \\ 
I, h &\models_{\text{SL}} t \mapsto u &\iff h = \{(t^I, u^I)\} \text{ and } t^I \not\models \text{nil}^I \\ 
I, h &\models_{\text{SL}} \phi_1 * \phi_2 &\iff \exists h_1, h_2. h = h_1 \oplus h_2 \text{ and } I, h_i \models_{\text{SL}} \phi_i, \text{ for all } i = 1, 2 \\ 
I, h &\models_{\text{SL}} \phi_1 \leftarrow \phi_2 &\iff \forall h' \text{ if } h' \# h \text{ and } I, h' \models_{\text{SL}} \phi_1 \text{ then } I, h' \oplus h \models_{\text{SL}} \phi_2 
\end{align*} $$

The satisfaction relation for the equality atoms t ≈ u and the Boolean connectives ∧, ∨ are the classical ones from first-order logic. In particular t ≈ t is always true, denoted by T, for any given heap. The (SL, T)-satisfiability problem asks, given an SL formula φ, if there is a T-model I such that (I, h) |= SL φ for some heap h.

In this paper we tackle the (SL, T)-satisfiability problem, under the assumption that the quantifier-free data theory T = (Σ, I) has a decidable satisfiability problem for constraints involving Σ-terms. It has been proved [9] that the satisfiability problem is PSPACE-complete for the fragment of separation logic in which Data is interpreted as the set of pairs of sort Loc. We generalize this result to any theory whose satisfiability problem, for the quantifier-free fragment, is in PSPACE. This is, in general, the case of most SMT theories, which are typically in NP, such as the linear arithmetic of integers and reals, possibly with sets and uninterpreted functions, etc.

## 3 Reducing SL(T) to Multisorted Second-Order Logic

It is well-known [21] that separation logic cannot be formalized as a classical (unsorted) first-order theory, for instance, due to the behavior of the * connective, that does not comply with the standard rules of contraction φ ⇒ φ * φ and weakening φ * φ ⇒ φ<fnref n="5" />. The basic reason is that φ * φ requires that φ and φ hold on disjoint heaps. Analogously, φ * φ holds on a heap whose extensions, by disjoint heaps satisfying φ, must satisfy φ. In the following, we leverage from the expressivity of multi-sorted first-order theories and translate SL(T) formulae into quantified formulae in the language of T, assuming that T subsumes a theory of sets and uninterpreted functions.

The integration of separation logic within the DPLL(T) framework [12] requires the input logic to be presented as a multi-sorted logic. To this end, we assume, without loss

<footnote n="5">⁵ Take for instance φ as x ↦→ 1 and φ as y ↦→ 2.</footnote>
of generality, the existence of a fixed theory $T = (\Sigma, \mathbf{I})$ that subsumes a theory of sets $\text{Set}(\sigma)$ [1], for any sort $\sigma$ of set elements, whose functions are the union $\cup$, intersection $\cap$ of sort $\text{Set}(\sigma) \times \text{Set}(\sigma) \to \text{Set}(\sigma)$, singleton $\{\cdot\}$ of sort $\sigma \to \text{Set}(\sigma)$ and emptyset $\emptyset$ of sort $\text{Set}(\sigma)$. We write $\ell \subseteq \ell'$ as a shorthand for $\ell \cup \ell' \approx \ell'$ and $t \in \ell$ for $\{t\} \subseteq \ell$, for any terms $\ell$ and $\ell'$ of sort $\text{Set}(\sigma)$ and $t$ of sort $\sigma$. The interpretation of the functions in the set theory is the classical (boolean) one.

Also, we assume that $\Sigma$ contains infinitely many function symbols $pt, pt', \dots \in \Sigma$ of sort $\text{Loc} \to \text{Data}$, where $\text{Loc}$ and $\text{Data}$ are two fixed sorts of $T$, such that for any interpretation $\mathcal{I} \in \mathbf{I}$, $\text{Loc}^{\mathcal{I}}$ is an infinite countable set.

The main idea is to express the atoms and connectives of separation logic in multi-sorted second-order logic by means of a transformation, called *labeling*, which introduces (i) constraints over variables of sort $\text{Set}(\text{Loc})$ and (ii) terms over uninterpreted points-to functions of sort $\text{Loc} \to \text{Data}$. We describe the labeling transformation using judgements of the form $\phi \llbracket \bar{\ell}, \overline{pt} \rrbracket$, where $\phi$ is a SL($T$) formula, $\bar{\ell} = \langle \ell_1, \dots, \ell_n \rangle$ is a tuple of variables of sort $\text{Set}(\text{Loc})$ and $\overline{pt} = \langle pt_1, \dots, pt_n \rangle$ is a tuple of uninterpreted function symbols occurring under the scopes of universal quantifiers. To ease the notation, we write $\ell$ and $pt$ instead of the singleton tuples $\langle \ell \rangle$ and $\langle pt \rangle$. In the following, we also write $\cup \bar{\ell}$ for $\ell_1 \cup \dots \cup \ell_n$, $\ell' \cap \bar{\ell}$ for $\langle \ell' \cap \ell_1, \dots, \ell' \cap \ell_n \rangle$, $\ell' \cdot \bar{\ell}$ for $\langle \ell', \ell_1, \dots, \ell_n \rangle$ and $\text{ite}(t \in \bar{\ell}, \overline{pt}(t) = u)$ for $\text{ite}(t \in \ell_1, pt_1(t) = u, \text{ite}(t \in \ell_2, pt_2(t) = u, \dots, \text{ite}(t \in \ell_n, pt_n(t) = u, \top)\dots))$.

Intuitively, a labeled formula $\phi \llbracket \bar{\ell}, \overline{pt} \rrbracket$ says that it is possible to build, from any of its satisfying interpretations $\mathcal{I}$, a heap $h$ such that $\mathcal{I}, h \models_{\text{SL}} \phi$, where $\text{dom}(h) = \ell_1^{\mathcal{I}} \cup \dots \cup \ell_n^{\mathcal{I}}$ and $h = pt_1^{\mathcal{I}} \searrow_{\ell_1^{\mathcal{I}}} \cup \dots \cup pt_n^{\mathcal{I}} \searrow_{\ell_n^{\mathcal{I}}}^6$. More precisely, a variable $\ell_i$ defines a slice of the domain of the heap, whereas the restriction of $pt_i$ to (the interpretation of) $\ell_i$ describes the heap relation on that slice. Observe that each interpretation of $\bar{\ell}$ and $\overline{pt}$, such that $\ell_i^{\mathcal{I}} \cap \ell_j^{\mathcal{I}} = \emptyset$, for all $i \neq j$, defines a unique heap.

First, we translate an input SL($T$) formula $\phi$ into a labeled second-order formula, with quantifiers over sets and uninterpreted functions, defined by the rewriting rules in Figure 1. A labeling step $\phi[\varphi] \Rightarrow \phi[\psi/\varphi]$ applies if $\varphi$ and $\psi$ match the antecedent and consequent of one of the rules in Figure 1, respectively. It is not hard to show that this rewriting system is confluent, and we denote by $\phi \downarrow$ the normal form of $\phi$ with respect to the application of labeling steps.

$$ \begin{array}{ccc} \frac{\begin{array}{l} (\phi * \psi) \llbracket \bar{\ell}, \overline{pt} \rrbracket \\ \neg \forall \ell_1 \forall \ell_2 . \neg (\ell_1 \cap \ell_2 \approx \emptyset \land \ell_1 \cup \ell_2 \approx \cup \ell \land \phi \llbracket \ell_1 \cap \bar{\ell}, \overline{pt} \rrbracket \land \psi \llbracket \ell_2 \cap \bar{\ell}, \overline{pt} \rrbracket) \end{array}}{\phi \llbracket \bar{\ell}, \overline{pt} \rrbracket \land \psi \llbracket \bar{\ell}, \overline{pt} \rrbracket} & \frac{\begin{array}{l} (\phi * \psi) \llbracket \bar{\ell}, \overline{pt} \rrbracket \\ \forall \ell' \forall pt' . (\ell' \cap (\cup \bar{\ell}) \approx \emptyset \land \phi \llbracket \ell', pt' \rrbracket) \Rightarrow \psi \llbracket \ell' \cdot \bar{\ell}, pt' \cdot \overline{pt} \rrbracket \end{array}}{(\neg \phi) \llbracket \bar{\ell}, \overline{pt} \rrbracket} & \frac{\begin{array}{l} (\phi \land \psi) \llbracket \bar{\ell}, \overline{pt} \rrbracket \\ \neg (\phi \llbracket \bar{\ell}, \overline{pt} \rrbracket) \end{array}}{\phi \llbracket \bar{\ell}, \overline{pt} \rrbracket \land \psi \llbracket \bar{\ell}, \overline{pt} \rrbracket} \\ \frac{t \mapsto u \llbracket \bar{\ell}, \overline{pt} \rrbracket}{\cup \bar{\ell} \approx \{t\} \land \text{ite}(t \in \bar{\ell}, \overline{pt}(t) \approx u) \land t \neq \text{nil}} & \frac{\text{emp} \llbracket \bar{\ell}, \overline{pt} \rrbracket}{\cup \bar{\ell} \approx \emptyset} & \frac{\varphi \llbracket \bar{\ell}, \overline{pt} \rrbracket}{\varphi} \quad \varphi \text{ is pure} \end{array} $$

<caption>Fig. 1. Labeling Rules</caption>

<footnote n="6">⁶ We denote by $F \downarrow_D$ the restriction of the function $F$ to the domain $D \subseteq \text{dom}(F)$.</footnote>
*Example 1.* Consider the SL(T) formula $(x \mapsto a * y \mapsto b) \wedge \text{emp}$. The reduction to second-order logic is given below:

$$ ((x \mapsto a * y \mapsto b) \wedge \text{emp}) \triangleleft [\ell, pt] \implies^* \\ \ell \approx \emptyset \wedge \forall \ell' \forall pt'. \ell' \cap \ell \approx \emptyset \wedge \ell' \approx \{x\} \wedge \text{ite}(x \in \ell', pt'(x) \approx a, \top) \wedge x \neq \text{nil} \implies \\ \ell' \cup \ell \approx \{y\} \wedge \text{ite}(y \in \ell', pt'(y) \approx b, \text{ite}(y \in \ell, pt(y) \approx b, \top)) \wedge y \neq \text{nil} \quad \blacksquare $$

The following lemma reduces the (SL, T)-satisfiability problem to the satisfiability of a quantified fragment of the multi-sorted second-order theory T, that contains sets and uninterpreted functions. For an interpretation $\mathcal{I}$, a variable $x$ and a value $s \in \sigma_x^{\mathcal{I}}$, we denote by $\mathcal{I}[x \leftarrow s]$ the extension of $\mathcal{I}$ which maps $x$ into $s$ and behaves like $\mathcal{I}$ for all other symbols. We extend this notation to tuples $\bar{x} = (x_1, \dots, x_n)$ and $\bar{s} = (s_1, \dots, s_n)$ and write $\mathcal{I}[\bar{x} \leftarrow \bar{s}]$ for $\mathcal{I}[x_1 \leftarrow s_1] \dots [x_n \leftarrow s_n]$. For a tuple of heaps $\bar{h} = (h_1, \dots, h_n)$ we write $\text{dom}(\bar{h})$ for $\langle\text{dom}(h_1), \dots, \text{dom}(h_n)\rangle$.

**Lemma 1.** Given a SL(T) formula $\varphi$ and tuples $\bar{\ell} = (\ell_1, \dots, \ell_n)$ and $\bar{pt} = (pt_1, \dots, pt_n)$ for $n > 0$, for any interpretation $\mathcal{I}$ of T and any heap $h: \mathcal{I}, h \models_{\text{SL}} \varphi$ if and only if

1. for all heaps $\bar{h} = (h_1, \dots, h_n)$ such that $h = h_1 \succ \dots \succ h_n$,
2. for all heaps $\bar{h}' = (h'_1, \dots, h'_n)$ such that $h_1 \subseteq h'_1, \dots, h_n \subseteq h'_n$,
we have $\mathcal{I}[\bar{\ell} \leftarrow \text{dom}(\bar{h})][\bar{pt} \leftarrow \bar{h}'] \models_T \varphi \triangleleft [\bar{\ell}, \bar{pt}] \downarrow$.

Although, in principle, satisfiability is undecidable in the presence of quantifiers and uninterpreted functions, the result of the next section strengthens this reduction, by adapting the labeling rules for $*$ and $-$ (Figure 1) to use bounded quantification over finite (set) domains.

# 4 A Reduction of SL(T) to Quantifiers Over Bounded Sets

In the previous section, we have reduced any instance of the (SL, T)-satisfiability problem to an instance of the T-satisfiability problem in the second-order multi-sorted theory T which subsumes the theory Set(Loc) and contains several quantified uninterpreted function symbols of sort Loc $\mapsto$ Data. A crucial point in the translation is that the only quantifiers occurring in T are of the forms $\forall \ell$ and $\forall pt$, where $\ell$ is a variable of sort Set(Loc) and $pt$ is a function symbol of sort Loc $\mapsto$ Data. Leveraging from a small model property for SL over the data domain $\mathcal{D} = \text{Loc} \times \text{Loc}$ [9], we show that it is sufficient to consider only the case when the quantified variables range over a bounded domain of sets. In principle, this allows us to eliminate the universal quantifiers by replacing them with finite conjunctions and obtain a decidability result based on the fact that the quantifier-free theory T with sets and uninterpreted functions is decidable. Since the cost of a-priori quantifier elimination is, in general, prohibitive, in the next section we develop an efficient lazy quantifier instantiation procedure, based on counterexample-driven refinement.

For reasons of self-containment, we quote the following lemma [24] and stress the fact that its proof is oblivious of the assumption $\mathcal{D} = \text{Loc} \times \text{Loc}$ on the range of heaps. Given a formula $\phi$ in the language SL(T), we first define the following measure:

$$ \begin{array}{l@{\quad}l@{\quad}l} |\phi * \psi| = |\phi| + |\psi| & |\phi * \psi| = |\psi| & |\phi \wedge \psi| = \max(|\phi|, |\psi|) \\ |t \mapsto u| = 1 & |\text{emp}| = 1 & |\phi| = 0 \text{ if } \phi \text{ is a } \Sigma\text{-formula} \end{array} $$
Intuitively, $|\phi|$ gives the maximum number of invisible locations in the domain of a heap $h$, that are not in the range of $\mathcal{I}$ and which can be distinguished by $\phi$. For instance, if $\mathcal{I}, h \models_{\mathrm{SL}} \neg\mathrm{emp} * \neg\mathrm{emp}$ and the domain of $h$ contains more than two locations, then it is possible to restrict $\mathrm{dom}(h)$ to $|\neg\mathrm{emp} * \neg\mathrm{emp}| = 2$ locations only, to satisfy this formula.

Let $\mathrm{Pt}(\phi)$ be the set of terms (of sort $\mathrm{Loc} \cup \mathrm{Data}$) that occur on the left- or right-hand side of a points-to atomic proposition in $\phi$. Formally, we have $\mathrm{Pt}(t \mapsto u) = \{t, u\}$, $\mathrm{Pt}(\phi * \psi) = \mathrm{Pt}(\phi * \psi) = \mathrm{Pt}(\phi) \cup \mathrm{Pt}(\psi)$, $\mathrm{Pt}(\neg\phi) = \mathrm{Pt}(\phi)$ and $\mathrm{Pt}(\mathrm{emp}) = \mathrm{Pt}(\phi) = \emptyset$, for a $\Sigma$-formula $\phi$. The small model property is given by the next lemma:

**Lemma 2.** [24, Proposition 96] Given a formula $\phi \in \mathrm{SL}(T)$, for any interpretation $\mathcal{I}$ of $T$, let $L \subseteq \mathrm{Loc}^I \setminus \mathrm{Pt}(\phi)^I$ be a set of locations, such that $\|L\| = |\phi|$ and $v \in \mathrm{Data}^I \setminus \mathrm{Pt}(\phi)^I$. Then, for any heap $h$, we have $\mathcal{I}, h \models_{\mathrm{SL}} \phi$ iff $\mathcal{I}, h' \models_{\mathrm{SL}} \phi$, for any heap $h'$ such that:
- $\mathrm{dom}(h') \subseteq L \cup \mathrm{Pt}(\phi)^I$,
- for all $\ell \in \mathrm{dom}(h')$, $h'(\ell) \in \mathrm{Pt}(\phi)^I \cup \{v\}

Based on the fact that the proof of Lemma 2 [24] does not involve reasoning about data values, other than equality checking, we refine our reduction from the previous section, by bounding the quantifiers to finite sets of constants of known size. To this end, we assume the existence of a total order on the (countable) set of constants in $\Sigma$ of sort $\mathrm{Loc}$, disjoint from any $\Sigma$-terms that occur in a given formula $\phi$, and define $\mathrm{Bnd}(\phi, C) = \{c_{m+1}, \dots, c_{m+|\phi|}\}$, where $m = \max\{i \mid c_i \in C\}$, and $m = 0$ if $C = \emptyset$. Clearly, we have $\mathrm{Pt}(\phi) \cap \mathrm{Bnd}(\phi, C) = \emptyset$ and also $C \cap \mathrm{Bnd}(\phi, C) = \emptyset$, for any $C$ and any $\phi$.

We now consider labeling judgements of the form $\varphi \triangleleft [\overline{\ell}, \overline{\mathrm{pt}}, C]$, where $C$ is a finite set of constants of sort $\mathrm{Loc}$, and modify all the rules in Figure 1, besides the ones with premises $(\phi * \psi) \triangleleft [\overline{\ell}, \overline{\mathrm{pt}}]$ and $(\phi * \psi) \triangleleft [\overline{\ell}, \overline{\mathrm{pt}}]$, by replacing any judgement $\varphi \triangleleft [\overline{\ell}, \overline{\mathrm{pt}}]$ with $\varphi \triangleleft [\overline{\ell}, \overline{\mathrm{pt}}, C]$. The two rules in Figure 2 are the bounded-quantifier equivalents of the $(\phi * \psi) \triangleleft [\overline{\ell}, \overline{\mathrm{pt}}]$ and $(\phi * \psi) \triangleleft [\overline{\ell}, \overline{\mathrm{pt}}]$ rules in Figure 1. As usual, we denote by $(\varphi \triangleleft [\overline{\ell}, \overline{\mathrm{pt}}, C]) \downarrow$ the formula obtained by exhaustively applying the new labeling rules to $\varphi \triangleleft [\overline{\ell}, \overline{\mathrm{pt}}, C]$.

Observe that the result of the labeling process is a formula in which all quantifiers are of the form $\forall \ell_1 \dots \forall \ell_n \forall \mathrm{pt}_1 \dots \forall \mathrm{pt}_n$. $\bigwedge_{i=1}^n \ell_i \subseteq L_i \wedge \bigwedge_{i=1}^n \mathrm{pt}_i \subseteq L_i \times D_i \Rightarrow \psi(\overline{\ell}, \overline{\mathrm{pt}})$, where $L_i$'s and $D_i$'s are finite sets of terms, none of which involves quantified variables, and $\psi$ is a formula in the theory $T$ with sets and uninterpreted functions. Moreover, the labeling rule for $\phi * \psi \triangleleft [\overline{\ell}, \overline{\mathrm{pt}}, C]$ uses a fresh constant $d$ that does not occur in $\phi$ or $\psi$.

$$
\begin{array}{l@{\qquad}l}
\begin{array}{@{}l@{}}
  \begin{array}{@{}l@{}}
    \phi * \psi \triangleleft [\overline{\ell}, \overline{\mathrm{pt}}, C] \\
    \neg\forall \ell_1 \forall \ell_2 . \ell_1 \cup \ell_2 \subseteq C \cup \mathrm{Pt}(\phi * \psi) \Rightarrow \\
    \phantom{\neg\forall \ell_1 \forall \ell_2 .} \neg(\ell_1 \cap \ell_2 \approx \emptyset \wedge \ell_1 \cup \ell_2 \approx \bigcup \overline{\ell} \wedge \phi \triangleleft [\ell_1 \cap \overline{\ell}, \overline{\mathrm{pt}}, C] \wedge \psi \triangleleft [\ell_2 \cap \overline{\ell}, \overline{\mathrm{pt}}, C])
  \end{array} &
  C' = \mathrm{Bnd}(\phi \wedge \psi, C) \\
  \begin{array}{@{}l@{}}
    \begin{array}{@{}l@{}}
      \phi * \psi \triangleleft [\overline{\ell}, \overline{\mathrm{pt}}, C] \\
      \forall \ell' \forall \mathrm{pt}' . \ell' \subseteq C' \cup \mathrm{Pt}(\phi * \psi) \wedge \\
      \phantom{\forall \ell' \forall \mathrm{pt}'} \mathrm{pt}' \subseteq (C' \cup \mathrm{Pt}(\phi * \psi)) \times (\mathrm{Pt}(\phi * \psi) \cup \{d\}) \Rightarrow \\
      \phantom{\forall \ell' \forall \mathrm{pt}'} (\ell' \cap (\bigcup \overline{\ell}) \approx \emptyset \wedge \phi \triangleleft [\ell', \mathrm{pt}', C']) \Rightarrow \psi \triangleleft [\ell' \cdot \overline{\ell}, \mathrm{pt}' \cdot \overline{\mathrm{pt}}, C]
    \end{array} &
    d \notin \mathrm{Pt}(\phi * \psi)
  \end{array}
\end{array}
$$

<caption>**Fig. 2.** Bounded Quantifier Labeling Rules</caption>
**Example 2.** We revisit below the labeling of the formula $(x \mapsto a \dashv y \mapsto b) \wedge \text{emp}$:

$$ ((x \mapsto a \dashv y \mapsto b) \wedge \text{emp}) \triangleleft [\ell, \text{pt}, C] \implies^* \\ \ell \approx \emptyset \wedge \forall \ell' \subseteq \{x, y, a, b, c\} \forall \text{pt}' \subseteq \{x, y, a, b, c\} \times \{x, y, a, b, d\}) . \\ \ell' \cap \ell \approx \emptyset \wedge \ell' \approx \{x\} \wedge \text{ite}(x \in \ell', \text{pt}'(x) \approx a, \top) \wedge x \neq \text{nil} \implies \\ \ell' \cup \ell \approx \{y\} \wedge \text{ite}(y \in \ell', \text{pt}'(y) \approx b, \text{ite}(y \in \ell, \text{pt}(y) \approx b, \top)) \wedge y \neq \text{nil} . $$

where $\text{Pt}((x \mapsto a \dashv y \mapsto b) \wedge \text{emp}) = \{x, y, a, b\}$. Observe that the constant $c$ was introduced by the bounded quantifier labeling of the term $x \mapsto a \dashv y \mapsto b$. ■

The next lemma states the soundness of the translation of SL(T) formulae in a fragment of T that contains only bounded quantifiers, by means of the rules in Figure 2.

**Lemma 3.** Given a formula $\varphi$ in the language SL(T), for any interpretation $\mathcal{I}$ of T, let $L \subseteq \text{Loc}^I \setminus \text{Pt}(\varphi)^I$ be a set of locations such that $\|L\| = |\varphi|$ and $v \in \text{Data}^I \setminus \text{Pt}(\varphi)^I$ be a data value. Then there exists a heap $h$ such that $\mathcal{I}, h \models_{\text{SL}} \varphi$ iff there exist heaps $\bar{h}' = \langle h'_1, \dots, h'_n \rangle$ and $\bar{h}'' = \langle \bar{h}''_1, \dots, \bar{h}''_n \rangle$ such that:

1. for all $1 \le i < j \le n$, we have $h'_i \neq h'_j$

2. for all $1 \le i \le n$, we have $h'_i \subseteq h''_i$ and

3. $\mathcal{I}[\bar{\ell} \leftarrow \text{dom}(\bar{h}')][\bar{\text{pt}} \leftarrow \bar{h}''][C \leftarrow L][d \leftarrow v] \models_T \varphi \triangleleft [\bar{\ell}, \bar{\text{pt}}, C]\triangleright$.

# 5 A Counterexample-Guided Approach for Solving SL(T) Inputs

This section presents a novel decision procedure for the (SL, T)-satisfiability of the set of quantifier-free SL(T) formulae $\varphi$. To this end, we present an efficient decision procedure for the T-satisfiability of $(\varphi \triangleleft [\ell, \text{pt}, C])\triangleright$, obtained as the result of the transformation described in Section 4. The main challenge in doing so is treating the universal quantification occurring in $(\varphi \triangleleft [\ell, \text{pt}, C])\triangleright$. As mentioned, the key to decidability is that all quantified formulae in $(\varphi \triangleleft [\ell, \text{pt}, C])\triangleright$ are equivalent to formulas of the form $\forall \mathbf{x}. (\wedge \mathbf{x} \subseteq \mathbf{s}) \Rightarrow \varphi$, where each term in the tuple $\mathbf{s}$ is a finite set (or product of sets) of ground $\Sigma$-terms. For brevity, we write $\forall \mathbf{x} \subseteq \mathbf{s}. \varphi$ to denote a quantified formula of this form. While such formulae are clearly equivalent to a finite conjunction of instances, the cost of constructing these instances is in practice prohibitively expensive. Following recent approaches for handling universal quantification [13, 19, 5, 20], we use a counterexample-guided approach for choosing instances of quantified formulae that are relevant to the satisfiability of our input. The approach is based on an iterative procedure maintaining an evolving set of quantifier-free $\Sigma$-formulae $\Gamma$, which is initially a set of formulae obtained from $\varphi$ by a purification step, described next.

We associate with each closed quantified formula a boolean variable $A$, called the *guard* of $\forall \mathbf{x}. \varphi$, and a (unique) set of Skolem symbols $\mathbf{k}$ of the same sort as $\mathbf{x}$. We write $(A, \mathbf{k}) \iff \forall \mathbf{x}. \varphi$ to denote that $A$ and $\mathbf{k}$ are associated with $\forall \mathbf{x}. \varphi$. For a set of formulae $\Gamma$, we write $\mathcal{Q}(\Gamma)$ to denote the set of quantified formulae whose guard occurs within a formula in $\Gamma$. We write $\lfloor \psi \rfloor$ for the result of replacing in $\psi$ all closed quantified formulae (not occurring beneath other quantifiers in $\psi$) with their corresponding guards. Conversely, we write $\lceil \Gamma \rceil$ to denote the result of replacing all guards in $\Gamma$ by the quantified formulae they are associated with. Then $\lfloor \psi \rfloor^*$ denotes the smallest set of $\Sigma$-formulae:
solve<sub>SL(T)</sub>(φ):

Let C be a set of fresh constants of sort Loc such that |C| = |φ|.

Let ℓ and pt be a fresh symbols of sort Set(Loc) and Loc ⇒ Data respectively.

Return solve<sub>T</sub>([φ<sub>↓</sub>[ℓ, pt, C]]↓<sup>*</sup>).

solve<sub>T</sub>(Γ):

1. If Γ is T-unsatisfiable,
   return “unsat”,

else let J be a T-model of Γ.

2. If Γ, A ⊨<sub>T</sub> [ψ[k/x]] for all ∀x.ψ ∈ Q(Γ), where (A, k) ⇄ ∀x.ψ and A<sup>J</sup> = ⊤,
   return “sat”,

else let J be a T-model of Γ ∪ {A, ¬[ψ[k/x]]} for some <<sub>Γ,J</sub>-minimal ∀x ⊆ s.ψ,
where (A, k) ⇄ ∀x ⊆ s.ψ.

3. Let t be a vector of terms, such that t ⊆ s, and t<sup>J</sup> = k<sup>J</sup>.

Return solve<sub>T</sub>(Γ ∪ [A ⇒ ψ[t/x]<sup>*</sup>]).

<caption>**Fig. 3.** Procedure `solve<sub>SL(T)</sub>` for deciding (SL, T)-satisfiability of SL(T) formula φ.</caption>

$$
\begin{array}{l}
\lfloor \psi \rfloor \in \lfloor \psi \rfloor^* \\
(\neg A \Rightarrow \lfloor \neg \varphi[\mathbf{k}/x] \rfloor) \in \lfloor \psi \rfloor^* \quad \text{if } \forall \mathbf{x}. \varphi \in Q(\lfloor \psi \rfloor^*) \text{ where } (A, \mathbf{k}) \Longleftrightarrow \forall \mathbf{x}. \varphi.
\end{array}
$$

In other words, ⌊ψ⌋* contains clauses that witness the negation of each universally quantified formula occurring in ψ. It is easy to see that if ψ is a Σ-formula possibly containing quantifiers, then ⌊ψ⌋* is a set of quantifier-free Σ-formulae, and if all quantified formulas in ψ are of the form ∀x ⊆ s.φ mentioned above, then all quantified formulas in Q(⌊ψ⌋*) are also of this form.

*Example 3.* If *ψ* is the formula ∀x.(P(x) ⇒ ¬∀y.R(x,y)), then ⌊*ψ*⌋<sup>*</sup> is the set:

$$
\{A_1, \neg A_1 \Rightarrow \neg (P(k_1) \Rightarrow A_2), \neg A_2 \Rightarrow \neg R(k_1, k_2)\}
$$

where (A₁, k₁) ⇄ ∀x.(P(x) ⇒ ¬∀y.R(x,y)) and (A₂, k₂) ⇄ ∀y.R(k₁,y).

<figure><img src="image_1.png" /></figure>

Our algorithm `solve<sub>SL(T)</sub>` for determining the (SL, T)-satisfiability of input φ is given in Figure 3. It first constructs the set C based on the value of |φ|, which it computes by traversing the structure of φ. It then invokes the subprocedure `solve<sub>T</sub>` on the set ⌊(φ<sub>↓</sub>[ℓ, pt, C])↓<sup>*</sup> where ℓ and pt are fresh free symbols.

At a high level, the recursive procedure `solve<sub>T</sub>` takes as input a (quantifier-free) set of T-formulae Γ, where Γ is T-unsatisfiable if and only if (φ<sub>↓</sub>[ℓ, pt, C])↓ is. On each invocation, `solve<sub>T</sub>` will either (i) terminate with “unsat”, in which case φ is T-unsatisfiable, (ii) terminate with “sat”, in which case φ is T-satisfiable, or (iii) add the set corresponding to the purification of the instance ⌊A ⇒ ψ[t/x]⌋* to Γ and repeats.

In more detail, in Step 1 of the procedure, we determine the T-satisfiability of Γ using a combination of a satisfiability solver and a decision procedure for T<sup>7</sup>. If Γ is

<footnote n="7"><sup>7</sup> Non-constant Skolem symbols k introduced by the procedure may be treated as uninterpreted functions. Constraints of the form k ⊆ S<sub>1</sub> × S<sub>2</sub> are translated to ⋀<sub>c∈S<sub>1</sub></sub> k(c) ∈ S<sub>2</sub>. Furthermore,</footnote>
T-unsatisfiable, since Γ is T-entailed by [Γ], we may terminate with “unsat”. Otherwise, there is a T-model I for Γ and T. In Step 2 of the procedure, for each A that is interpreted to be true by I, we check whether Γ ∪ {A} T-entails ⌜ψ[k/x]⌝ for fresh free constants k, which can be accomplished by determining whether Γ ∪ {A, ¬ψ[k/x]} is T-unsatisfiable. If this check succeeds for a quantified formula ∀x.ψ, the algorithm has established that ∀x.ψ is entailed by Γ. If this check succeeds for all such quantified formulae, then Γ is equivalent to [Γ], and we may terminate with “sat”. Otherwise, let Q<sup>+</sup><sub>I</sub>(Γ) be the subset of Q(Γ) for which this check did not succeed. We call this the set of active quantified formulae for (I, Γ). We consider an active quantified formula that is minimal with respect to the relation <<sub>I, I</sub> over Q(Γ), where:

$$ \varphi <_{I, I} \psi \quad \text{if and only if} \quad \varphi \in Q(\lfloor \psi \rfloor^*) \cap Q_I^+(\Gamma) $$

By this ordering, our approach considers innermost active quantified formulae first. Let ∀x.ψ be minimal with respect to <<sub>I, I</sub>, where (A, k) ⇌ ∀x.ψ. Since Γ, A does not T-entail ⌜ψ[k/x]⌝, there must exist a model J for Γ ∪ { ¬ψ[k/x] } where A<sup>J</sup> = ⊤. In Step 3 of the procedure, we choose a tuple of terms t = (t<sub>1</sub>, ..., t<sub>n</sub>) based on the model J, and add to Γ the set of formulae obtained by purifying A ⇒ ψ[t/x], where A is the guard of ∀x ⊆ s.ψ. Assume that s = (s<sub>1</sub>, ..., s<sub>n</sub>) and recall that each s<sub>i</sub> is a finite union of ground Σ-terms. We choose each t such that t<sub>i</sub> is a subset of s<sub>i</sub> for each i = 1, ..., n, and t<sup>J</sup> = k<sup>J</sup>. These two criteria are the key to the termination of the algorithm: the former ensures that only a finite number of possible instances can ever be added to Γ, and the latter ensures that we never add the same instance more than once.

**Theorem 1.** For all SL(T) formulae φ, solve<sub>SL(T)</sub>(φ):

1. Answers “unsat” only if φ is (SL, T)-unsatisfiable.

2. Answers “sat” only if φ is (SL, T)-satisfiable.

3. Terminates.

By Theorem 1, solve<sub>SL(T)</sub> is a decision procedure for the (SL, T)-satisfiability of the language of quantifier-free SL(T) formulae. The following corollary gives a tight complexity bound for the (SL, T)-satisfiability problem.

**Corollary 1.** The (SL, T)-satisfiability problem is PSPACE-complete for any theory T whose satisfiability (for the quantifier-free fragment) is in PSPACE.

In addition to being sound and complete, in practice, the approach solve<sub>SL(T)</sub> terminates in much less time that its theoretical worst-case complexity, given by the above corollary. This fact is corroborated by our evaluation of our prototype implementation of the algorithm, described in Section 6, and in the following example.

**Example 4.** Consider the SL(T) formula φ ≡ emp ∧ (y ↦ 0 ⇏ y ↦ 1) ∧ y ≠ nil. When running solve<sub>SL(T)</sub>(φ), we first compute the set C = {c}, and introduce fresh symbols ℓ

<footnote>the domain of k may be restricted to the set {c<sup>J</sup> | c ∈ S<sub>1</sub>} in models I found in Steps 1 and 2 of the procedure. This restriction comes with no loss of generality since, by construction of (φ < [ℓ, pt, C])↓, k is applied only to terms occurring in S<sub>1</sub>.</footnote>
and pt of sorts Set(Loc) and Loc → Data respectively. The formula $(\varphi \triangleleft [\ell, pt, C]) \downarrow$ is
$\ell \approx \emptyset \wedge \forall \ell_4 \forall pt'. \psi \wedge y \neq \text{nil}$, where after simplification $\psi$ is:

$$
\begin{align*}
\psi_4 &\equiv (\ell_4 \subseteq \{y, 0, 1, c\} \land pt' \subseteq \{y, 0, 1, c\} \times \{y, 0, 1, d\}) \Rightarrow \\
&\quad (\ell_4 \cap \ell \approx \emptyset \land \ell_4 \approx \{y\} \land pt'(y) \approx 0 \land y \neq \text{nil}) \Rightarrow \\
&\quad (\ell_4 \cup \ell \approx \{y\} \land \text{ite}(y \in \ell_4, pt'(y) \approx 1, pt(y) \approx 1) \land y \neq \text{nil})
\end{align*}
$$

Let $(A_4, (k_1, k_2)) \Leftrightarrow \forall \ell_4 \forall pt'. \psi_4$. We call the subprocedure solve<sub>T</sub> on $\Gamma_0$, where:

$$
\Gamma_0 \equiv [ (\varphi \triangleleft [\ell, pt, C]) \downarrow ]^* \equiv \{ \ell \approx \emptyset \wedge A_4 \wedge y \neq \text{nil}, \neg A_4 \Rightarrow \neg \psi_4 [k_1, k_2 / \ell_4, pt'] \}.
$$

The set Γ₀ is T-satisfiable with a model I₀ where A₄<sup>I₀</sup> = ⊤. Step 2 of the procedure determines a model J for Γ₀ ∪ {A₄, ¬ψ₄[k₁, k₂/ℓ₄, pt']}.

Let $t_1$ be $\{y\}$, where we know $t_1^J = k_1^J$ since $\mathcal{J}$ must satisfy $k_1 \approx \{y\}$ as a consequence of $\neg\psi_4[k_1, k_2/\ell_4, pt']$. Let $t_2$ be a well-sorted subset of $\{y, 0, 1, c\} \times \{y, 0, 1, d\}$ such that $t_2^J = k_2^J$. Such a subset exists since $\mathcal{J}$ satisfies $k_2 \subseteq \{y, 0, 1, c\} \times \{y, 0, 1, d\}$. Notice that $t_2(y)^J = 0^J$ since $\mathcal{J}$ must satisfy $k_2(y) \approx 0$. Step 3 of the procedure recursively invokes `solve_T` on $\Gamma_1$, where:

$$
\begin{align*}
\Gamma_1 &\equiv \Gamma_0 \cup [A_4 \Rightarrow \psi_4[t_1, t_2/\ell_4, pt']]^* \\
&\equiv \Gamma_0 \cup \{A_4 \Rightarrow y \neq \text{nil} \Rightarrow (\{y\} \approx \{y\} \land \text{ite}(y \in \{y\}, 0 \approx 1, pt(y) \approx 1) \land y \neq \text{nil})\} \\
&\equiv \Gamma_0 \cup \{A_4 \Rightarrow y \neq \text{nil} \Rightarrow \perp\}
\end{align*}
$$

The set $\Gamma_1$ is T-unsatisfiable, since the added constraint contradicts $A_4 \wedge y \neq \text{nil}$. $\blacksquare$

<figure><img src="image_2.png" /></figure>

**5.1 Integration in DPLL(T)**

We have implemented the algorithm described in this section within the SMT solver CVC4 [2]. Our implementation accepts an extended syntax of SMT-LIB version 2 format [3] for specifying SL(T) formulae. In contrast to the presentation so far, our implementation does not explicitly introduce quantifiers, and instead treats SL atoms natively using an integrated subsolver that expands the semantics of these atoms in lazy fashion.

In more detail, given a SL(*T*) input φ, our implementation lazily computes the expansion of (φ ⋄ [ℓ, pt, C])↓ based on the translation rules in Figures 1 and 2 and the counterexample-guided instantiation procedure in Figure 3. This is accomplished by a module, which we refer to as the SL solver, that behaves analogously to a DPLL(*T*)-style theory solver, that is, a dedicated solver specialized for the *T*-satisfiability of a conjunction of *T*-constraints.

The DPLL(*T*) solving architecture [12] used by most modern SMT solvers, given as input a set of quantifier-free *T*-formulae Γ, incrementally constructs of set of literals over the atoms of Γ until either it finds a set *M* that entail Γ at the propositional level, or determines that such a set cannot be found. In the former case, we refer to *M* as a satisfying assignment for Γ. If *T* is a combination of theories *T*₁ ∪ ... ∪ *T*ₙ, then *M* is partitioned into *M*₁ ∪ ... ∪ *M*ₙ where the atoms of *M*ᵢ are either *T*ᵢ-constraints or (dis)equalities shared over multiple theories. We use a theory solver (for *T*ᵢ) to determine the *T*ᵢ-satisfiability of the set *M*ᵢ, interpreted as a conjunction. Given *M*ᵢ, the solver will either add additional formulae to Γ, or otherwise report that *M*ᵢ is *T*ᵢ-satisfiable.
For SL(T) inputs, we extend our input syntax with a set of functions:

$$ \begin{array}{lclcl} \mapsto: & \text{Loc} \times \text{Data} & \to & \text{Bool} & \quad \text{\*}^n: & \text{Bool}^n \to \text{Bool} & \quad \text{emp}: & \text{Bool} \\ \dashv: & \text{Bool} \times \text{Bool} & \to & \text{Bool} & \quad \text{lbl}: & \text{Bool} \times \text{Set}(\text{Loc}) & \to & \text{Bool} \end{array} $$

which we call *spatial functions*<fnref n="8" />. We refer to *lbl* as the *labeling predicate*, which can be understood as a placeholder for the ◁ transformation in Figures 1 and 2. We refer to *p(t)* as an *unlabeled spatial atom* if *p* is one of {emp, ↦, \*, \*, \*} and *t* is a vector of terms not containing *lbl*. If *a* is an unlabeled spatial atom, We refer to *lbl(a, ℓ)* as a *labeled spatial atom*, and extend these terminologies to literals. We assume that all occurrences of spatial functions in our input *ϕ* occur only in unlabeled spatial atoms. Moreover, during execution, our implementation transforms all spatial atoms into a *normal form*, by applying associativity to flatten nested applications of \*, and distributing Σ-formulae over spatial connectives, e.g. ((x ↦ y ∧ t ≈ u) \* z ↦ w) ⇐⇒ t ≈ u ∧ (x ↦ y \* z ↦ w).

When constructing satisfying assignments for *ϕ*, we relegate the set of all spatial literals $M_k$ to the SL solver. For all unlabeled spatial literals ($\neg$) *a*, we add to $\Gamma$ the formula $(a \Leftrightarrow \text{lbl}(a, \ell_0))$, where $\ell_0$ is a distinguished free constant of sort $\text{Set(Loc)}$. Henceforth, it suffices for the SL solver to only consider the labeled spatial literals in $M_k$. To do so, firstly, it adds to $\Gamma$ formulae based on the following criteria, which model one step of the reduction from Figure 1:

$$ \begin{array}{l@{\qquad}l} \text{lbl}(\text{emp}, \ell) & \Leftrightarrow \ell \approx \emptyset & \text{if } (\neg)\text{lbl}(\text{emp}, \ell) \in M_k \\ \text{lbl}(t \mapsto u, \ell) & \Leftrightarrow \ell \approx \{t\} \wedge \text{pt}(t) \approx u \wedge t \not\approx \text{nil} & \text{if } (\neg)\text{lbl}(t \mapsto u, \ell) \in M_k \\ \text{lbl}((\varphi_1 \ \dots \ \varphi_n), \ell) & \Rightarrow (\varphi_1[\ell_1] \wedge \dots \wedge \varphi_n[\ell_n]) & \text{if } \text{lbl}((\varphi_1 \ \dots \ \varphi_n), \ell) \in M_k \\ \neg\text{lbl}((\varphi_1 \ \neg\ \varphi_2), \ell) & \Rightarrow (\varphi_1[\ell_1] \wedge \neg\varphi_2[\ell_2]) & \text{if } \neg\text{lbl}((\varphi_1 \ \neg\ \varphi_2), \ell) \in M_k \end{array} $$

where each $\ell_i$ is a fresh free constant, and $\varphi_i[\ell_i]$ denotes the result of replacing each top-level spatial atom *a* in $\varphi_i$ with *lbl(a, $\ell_i$)*. These formulae are added eagerly when such literals are added to $M_k$. To handle negated \*-atoms and positive \*-atoms, the SL solver adds to $\Gamma$ formulae based on the criteria:

$$ \begin{array}{l@{\qquad}l} \neg\text{lbl}((\varphi_1 \ \dots \ \varphi_n), \ell) & \Rightarrow (\neg\varphi_1[t_1] \lor \dots \lor \neg\varphi_n[t_n]) & \text{if } \neg\text{lbl}((\varphi_1 \ \dots \ \varphi_n), \ell) \in M_k \\ \text{lbl}((\varphi_1 \ \neg\ \varphi_2), \ell) & \Rightarrow (\neg\varphi_1[t_1, f_1] \lor \varphi_2[t_2, f_2]) & \text{if } \text{lbl}((\varphi_1 \ \neg\ \varphi_2), \ell) \in M_k \end{array} $$

where each $t_i$ and $f_i$ is chosen based on the same criterion as described in Figure 3. For wand, we write $\varphi_i[t_i, f_i]$ to denote $\varphi'_i[t_i]$, where $\varphi'_i$ is the result of replacing all atoms of the form $t \mapsto u$ where $t \in t_1$ in $\varphi_i$ by $f_i(t) \approx u$.

CVC4 uses a scheme for incrementally checking the *T*-entailments required by *solveT*, as well as constructing models $\mathcal{J}$ satisfying the negated form of the literals in literals in $M_k$ before choosing such terms [20]. The formula of the above form are added to $\Gamma$ lazily, that is, after all other solvers (for theories $T_i$) have determined their corresponding sets of literals $M_i$ are $T_i$-satisfiable.

**Partial Support for Quantifiers** In many practical cases it is useful to check the validity of entailments between existentially quantified SL(T) formulae such as $\exists x . \phi(x)$ and $\exists y . \psi(y)$. Typically, this problem translates into a satisfiability query for an SL(T)

<footnote n="8">⁸ These functions are over the Bool sort. We refer to these functions as taking *formulae* as input, where formulae may be cast to terms of sort Bool through use of an if-then-else construct.</footnote>
formula $∃x∀y. φ(x) ∧ ¬ψ(y)$, with one quantifier alternation. A partial solution to this problem is to first check the satisfiability of $φ$. If $φ$ is not satisfiable, the entailment holds trivially, so let us assume that $φ$ has a model. Second, we check satisfiability of $φ ∧ ψ$. Again, if this is unsatisfiable, then the entailment cannot hold, because there exists a model of $φ$ which is not a model of $ψ$. Else, if $φ ∧ ψ$ has a model, we add an equality $x = y$ for each pair of variables $(x,y) ∈ x × y$ that are mapped to the same term in this model, the result being a conjunction $E(x,y)$ of equalities. Finally, we check the satisfiability of the formula $φ ∧ ¬ψ ∧ E$. If this formula is unsatisfiable, the entailment is valid, otherwise, the test is inconclusive. In section 6, we applied this method manually, to test entailments between existentially quantified variables — general procedure for quantifier instantiation for SL($T$) is envisaged in the near future.

# 6 Evaluation

We tested our implementation of the (SL, $T$)-satisfiability procedure in CVC4 (version 1.5 prerelease)<fnref n="9" /> on two kinds of benchmarks: (i) finite unfoldings of inductive predicates with data constraints, mostly inspired by existing benchmarks, such as SL-COMP'14 [22], and (ii) verification conditions automatically generated by applying the weakest precondition calculus of [15] to the program loops in Figure 4 several times. All experiments were run on a 2.80GHz Intel(R) Core(TM) i7 CPU machine with 8MB of cache<fnref n="10" />. For a majority of benchmarks, the runtime of CVC4 is quite low, with the exception of the $n = 4, 8$ cases of the entailments between $tree_1^n$ and $tree_2^n$ formulae, which resulted in a timeout after 300 seconds. For benchmarks where CVC4 times out, the performance bottleneck resides in its ground decision procedure for finite sets, indicating efficient support for this theory is important for our approach to separation logic.

<figure><img src="image_3.png" /><figcaption>Fig. 4. Program Loops</figcaption></figure>

The first set of experiments is reported in Table 1. We have considered inductive predicates commonly used as verification benchmarks [22]. Here we check the validity

<footnote n="9">⁹ Available at http://cvc4.cs.nyu.edu/web/.</footnote>

<footnote n="10">¹⁰ The CVC4 binary and examples used in these experiments are available at http://cvc4.cs.nyu.edu/papers/ATVA2016-seplog/.</footnote>
<table><caption>Table 1. Experimental results</caption><thead><tr><th>lhs</th><th>rhs</th><th>n = 1</th><th>n = 2</th><th>n = 3</th><th>n = 4</th><th>n = 8</th></tr></thead><tbody><tr><td colspan="7" style="text-align: center; font-weight: bold;">Unfoldings of inductive predicates</td></tr><tr><td>lseg<sub>1</sub>(x,y,a) &plusmn; emp &and; x=y &or; z &exist; b.<br/>x &rarr; (a,z) * lseg<sub>1</sub>(z,y,b) &and; b=a+10</td><td>lseg<sub>2</sub>(x,y,a) &plusmn; emp &and; x=y &or; z &exist; b.<br/>x &rarr; (a,z) * lseg<sub>2</sub>(z,y,b) &and; a &le; b</td><td>unsat<br/>&lt; 0.01s</td><td>unsat<br/>&lt; 0.01s</td><td>unsat<br/>&lt; 0.01s</td><td>unsat<br/>&lt; 0.01s</td><td>unsat<br/>&lt; 0.01s</td></tr><tr><td>tree<sub>1</sub>(x,a) &plusmn; emp &and; x= nil &or; y &exist; z &exist; b &exist; c.<br/>x &rarr; (a,y,z) * tree<sub>1</sub>(y,b) * tree<sub>1</sub>(z,c) &and;<br/>b=a-10 &and; c=a+10</td><td>tree<sub>2</sub>(x,a) &plusmn; emp &and; x= nil &or; y &exist; z &exist; b &exist; c.<br/>x &rarr; (a,y,z) * tree<sub>2</sub>(y,b) * tree<sub>2</sub>(z,c) &and;<br/>b &le; a &and; a &le; c</td><td>unsat<br/>&lt; 0.01s</td><td>unsat<br/>&lt; 0.06s</td><td>unsat<br/>&lt; 1.89s</td><td>timeout<br/>&gt; 300s</td><td>timeout<br/>&gt; 300s</td></tr><tr><td>pos<sub>1</sub>(x,a) &plusmn; x &rarr; a &or; y &exist; b.<br/>x &rarr; a * pos<sub>1</sub>(y,b)</td><td>neg<sub>1</sub>(x,a) &plusmn; x &rarr; a &or; y &exist; b.<br/>x &rarr; a * neg<sub>1</sub>(y,b)</td><td>unsat<br/>&lt; 0.02s</td><td>unsat<br/>&lt; 0.04s</td><td>unsat<br/>&lt; 0.11s</td><td>unsat<br/>&lt; 0.25 s</td><td>unsat<br/>&lt; 3.01s</td></tr><tr><td>pos<sub>1</sub>(x,a) &plusmn; x &rarr; a &or; y &exist; b.<br/>x &rarr; a * pos<sub>1</sub>(y,b)</td><td>neg<sub>2</sub>(x,a) &plusmn; x &rarr; a &or; y &exist; b.<br/>x &rarr; a * neg<sub>2</sub>(y,b)</td><td>unsat<br/>&lt; 0.01s</td><td>unsat<br/>&lt; 0.05s</td><td>unsat<br/>&lt; 0.11s</td><td>unsat<br/>&lt; 0.23s</td><td>unsat<br/>&lt; 2.10s</td></tr><tr><td>pos<sub>1</sub>(x,a) &plusmn; x &rarr; a &or; y &exist; b.<br/>x &rarr; a * pos<sub>1</sub>(y,b)</td><td>neg<sub>3</sub>(x,a) &plusmn; x &rarr; a &or; y &exist; b.<br/>x &rarr; a * neg<sub>3</sub>(y,b)</td><td>unsat<br/>&lt; 0.02s</td><td>unsat<br/>&lt; 0.07s</td><td>unsat<br/>&lt; 0.24s</td><td>unsat<br/>&lt; 0.46s</td><td>unsat<br/>&lt; 4.05s</td></tr><tr><td>pos<sub>1</sub>(x,a) &plusmn; x &rarr; a &or; y &exist; b.<br/>x &rarr; a * pos<sub>1</sub>(y,b)</td><td>neg<sub>4</sub>(x,a) &plusmn; x &rarr; a &or; y &exist; b.<br/>x &rarr; a * neg<sub>4</sub>(y,b)</td><td>unsat<br/>&lt; 0.05s</td><td>sat<br/>&lt; 0.24s</td><td>unsat<br/>&lt; 0.33s</td><td>sat<br/>&lt; 2.77s</td><td>sat<br/>&lt; 24.72s</td></tr><tr><td>pos<sub>2</sub>(x,a) &plusmn; x &rarr; a &or; y.<br/>x &rarr; a * pos<sub>2</sub>(a,y)</td><td>neg<sub>5</sub>(x,a) &plusmn; x &rarr; a &or; y.<br/>x &rarr; a * neg<sub>5</sub>(a,y)</td><td>unsat<br/>&lt; 0.02s</td><td>unsat<br/>&lt; 0.05s</td><td>unsat<br/>&lt; 0.14s</td><td>unsat<br/>&lt; 0.32s</td><td>unsat<br/>&lt; 3.69s</td></tr><tr><td>pos<sub>2</sub>(x,a) &plusmn; x &rarr; a &or; y.<br/>x &rarr; a * pos<sub>2</sub>(a,y)</td><td>neg<sub>6</sub>(x,a) &plusmn; x &rarr; a &or; y.<br/>x &rarr; a * neg<sub>6</sub>(a,y)</td><td>sat<br/>&lt; 0.02s</td><td>unsat<br/>&lt; 0.04s</td><td>unsat<br/>&lt; 0.13s</td><td>unsat<br/>&lt; 0.27s</td><td>unsat<br/>&lt; 2.22s</td></tr><tr><td colspan="7" style="text-align: center; font-weight: bold;">Verification conditions</td></tr><tr><td>ls<sup>n</sup>(w)</td><td>wp(disp,ls<sup>n-1</sup>(w))</td><td>&lt; 0.01s</td><td>0.02s</td><td>0.05s</td><td>0.12s</td><td>1.97s</td></tr><tr><td>ls<sup>n</sup>(w)</td><td>wp<sup>n</sup>(disp,emp &and; w= nil)</td><td>&lt; 0.01s</td><td>0.02s</td><td>0.12s</td><td>0.41s</td><td>22.97s</td></tr><tr><td>zls<sup>n</sup>(w)</td><td>wp(zdisp,zls<sup>n-1</sup>(w))</td><td>0.01s</td><td>0.02s</td><td>0.05s</td><td>0.11s</td><td>1.34s</td></tr><tr><td>zls<sup>n</sup>(w)</td><td>wp<sup>n</sup>(zdisp,emp &and; w= nil)</td><td>0.01s</td><td>0.02s</td><td>0.11s</td><td>0.43s</td><td>24.13s</td></tr><tr><td>ls<sup>n</sup>(u) * ls<sup>0</sup>(v)</td><td>wp(rev,ls<sup>n-1</sup>(u) * ls<sup>1</sup>(v))</td><td>0.06s</td><td>0.08s</td><td>0.14s</td><td>0.30s</td><td>2.83s</td></tr><tr><td>ls<sup>n</sup>(u) * ls<sup>0</sup>(v)</td><td>wp<sup>n</sup>(rev,u= nil &and; ls<sup>n</sup>(v))</td><td>0.06s</td><td>0.12s</td><td>0.56s</td><td>1.75s</td><td>27.82s</td></tr><tr><td>zls<sup>n</sup>(u) * zls<sup>0</sup>(v)</td><td>wp(zrev,zls<sup>n-1</sup>(u) * zls<sup>1</sup>(v))</td><td>0.22s</td><td>0.04s</td><td>0.12s</td><td>0.25s</td><td>2.16s</td></tr><tr><td>zls<sup>n</sup>(u) * zls<sup>0</sup>(v)</td><td>wp<sup>n</sup>(zrev,u= nil &and; zls<sup>n</sup>(v))</td><td>0.04s</td><td>0.10s</td><td>0.41s</td><td>1.27s</td><td>20.26s</td></tr></tbody></table>

of the entailment between `lhs` and `rhs`, where both predicates are unfolded $n = 1, 2, 3, 4, 8$ times. The second set of experiments, reported in Table 1, considers the verification conditions of the forms $\varphi \Rightarrow \text{wp}(\mathbf{l}, \phi)$ and $\varphi \Rightarrow \text{wp}^n(\mathbf{l}, \phi)$, where $\text{wp}(\mathbf{l}, \phi)$ denotes the weakest precondition of the SL formula $\phi$ with respect to the sequence of statements `l`, and $\text{wp}^n(\mathbf{l}, \phi) = \text{wp}(\mathbf{l}, \dots, \text{wp}(\mathbf{l}, \text{wp}(\mathbf{l}, \phi)))$ denotes the iterative application of the weakest precondition $n$ times in a row. We consider the loops depicted in Figure 4, where, for each loop `l` we consider the variant `zl` as well, which tests that the data values contained within the memory cells are 0, by the assertions on line 2. The postconditions are specified by finite unfoldings of the inductive predicates `ls` and `zls` (Figure 4).

## 7 Conclusions

We have presented a decision procedure for quantifier-free SL(T) formulas that relies on an efficient, counterexample-guided approach for establishing the T-satisfiability of formulas having quantification over bounded sets. We have described an implementation of the approach as an integrated subsolver in the DPLL(T)-based SMT solver CVC4, showing the potential of the procedure as a backend for tools reasoning about low-level pointer and data manipulations.
References

1. Bansal, K.: Decision Procedures for Finite Sets with Cardinality and Local Theory Extensions. Ph.D. thesis, New York University (2016)

2. Barrett, C., Conway, C., Deters, M., Hadarean, L., Jovanovic, D., King, T., Reynolds, A., Tinelli, C.: Cvc4. In: CAV'11. pp. 171–177 (2011)

3. Barrett, C., Fontaine, P., Tinelli, C.: The SMT-LIB 2.5 standard. Tech. rep., The University of Iowa (2015), http://smt-lib.org/

4. Berdine, J., Calcagno, C., Cook, B., Distefano, D., O'Hearn, P., Wies, T., Yang, H.: Shape analysis for composite data structures. In: CAV'07. LNCS, vol. 4590, pp. 178–192 (2007)

5. Bjørner, N., Janota, M.: Playing with quantified satisfaction. In: LPAR'15. EPIC, vol. 35, pp. 15–27 (2015)

6. Brotherston, J., Gorogiannis, N., Petersen, R.L.: A generic cyclic theorem prover. In: APLAS'12. pp. 350–367 (2012)

7. Calcagno, C., Distefano, D.: Infer: An automatic program verifier for memory safety of c programs. In: Proc. of NASA Formal Methods'11. LNCS, vol. 6617 (2011)

8. Calcagno, C., Gardner, P., Hague, M.: From separation logic to first-order logic. In: FOS-SACS'05. pp. 395–409 (2005)

9. Calcagno, C., Yang, H., Ohearn, P.W.: Computability and complexity results for a spatial assertion language for data structures. In: FSTTCS'01. pp. 108–119 (2001)

10. Enea, C., Sighireanu, M., Wu, Z.: On automated lemma generation for separation logic with inductive definitions. In: ATVA'15. pp. 80–96 (2015)

11. Galmiche, D., Méry, D.: Tableaux and resource graphs for separation logic. Journal of Logic and Computation 20(1), 189–231 (2010)

12. Ganzinger, H., Hagen, G., Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Dpll(t): Fast decision procedures. In: CAV'04, pp. 175–188 (2004)

13. Ge, Y., de Moura, L.: Complete instantiation for quantified formulas in satisfiability modulo theories. In: CAV'09. LNCS, vol. 5643 (2009)

14. Iosif, R., Rogalewicz, A., Vojnar, T.: Slide: Separation logic with inductive definitions, URL: http://www.fit.vutbr.cz/research/groups/verifit/tools/slide/

15. Ishtiaq, S.S., O'Hearn, P.W.: BI as an assertion language for mutable data structures. In: ACM SIGPLAN Notices. vol. 36, pp. 14–26 (2001)

16. Navarro Pérez, J.A., Rybalchenko, A.: Separation logic + superposition calculus = heap theorem prover. ACM SIGPLAN Notices 46(6), 556–566 (2011)

17. Piskac, R., Wies, T., Zufferey, D.: Automating separation logic using SMT. In: CAV'13. pp. 773–789 (2013)

18. Piskac, R., Wies, T., Zufferey, D.: Automating separation logic with trees and data. In: CAV'14. pp. 711–728 (2014)

19. Reynolds, A., Deters, M., Kuncak, V., Barrett, C.W., Tinelli, C.: Counterexample guided quantifier instantiation for synthesis in CVC4. In: CAV'15. pp. 198–216 (2015)

20. Reynolds, A., King, T., Kuncak, V.: An instantiation-based approach for solving quantified linear arithmetic. CoRR abs/1510.02642 (2015)

21. Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: Logic in Computer Science. pp. 55–74. LICS'02 (2002)

22. Sighireanu, M., Cok, D.: Report on SL-COMP 2014. Journal on Satisfiability, Boolean Modeling and Computation 1, 173–186 (2014)

23. Suter, P., Steiger, R., Kuncak, V.: Sets with cardinality constraints in satisfiability modulo theories. In: VMCAI'11, pp. 403–418 (2011)

24. Yang, H.: Local Reasoning for Stateful Programs. Ph.D. thesis, University of Illinois at Urbana-Champaign (2001)