# Quantitative Separation Logic and Programs with Lists

Radu Iosif, Dorel Marius Bozga, Swann Perarnau

► To cite this version:

Radu Iosif, Dorel Marius Bozga, Swann Perarnau. Quantitative Separation Logic and Programs with Lists. Journal of Automated Reasoning, 2010, 45 (2), pp.131-156. 10.1007/s10817-010-9179-9. hal-01418870

HAL Id: hal-01418870

https://hal.science/hal-01418870

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
Quantitative Separation Logic and Programs with Lists

Marius Bozga · Radu Iosif · Swann Perarnau

Received: date / Accepted: date

**Abstract** This paper presents an extension of a decidable fragment of Separation Logic for singly-linked lists, defined by Berdine, Calcagno and O'Hearn [8]. Our main extension consists in introducing atomic formulae of the form $ls^k(x,y)$ describing a list segment of length $k$, stretching from $x$ to $y$, where $k$ is a logical variable interpreted over positive natural numbers, that may occur further inside Presburger constraints. We study the decidability of the full first-order logic combining unrestricted quantification of arithmetic and location variables. Although the full logic is found to be undecidable, validity of entailments between formulae with the quantifier prefix in the language $∃^*{∃_N; ∀_N}^*$ is decidable. We provide here a model theoretic method, based on a parametric notion of shape graphs. We have implemented our decision technique, providing a fully automated framework for the verification of quantitative properties expressed as pre- and post-conditions on programs working on lists and integer counters.

**Keywords** Separation Logic · List structures · Program verification

Marius Bozga
VERIMAG,CNRS,University of Grenoble,
2 Avenue de Vignate, 38610, Gières, France
Tel.: +33 4 56 52 04 35
Fax: +33 4 56 52 03 44
E-mail: Marius.Bozga@imag.fr

Radu Iosif
VERIMAG,CNRS,University of Grenoble,
2 Avenue de Vignate, 38610, Gières, France
Tel.: +33 4 56 52 04 33
Fax: +33 4 56 52 03 44
E-mail: Radu.Iosif@imag.fr

Swann Perarnau
LIG,Grenoble INP,
ZIRST 51, Avenue Jean Kuntzmann, 38330, Montbonnot Saint Martin, France
Tel.: +33 4 76 61 20 35
E-mail: Swann.Perarnau@imag.fr
# 1 Introduction

Separation Logic [12,18] has recently become a widespread formalism for the specification of programs with dynamic data structures. Due to the intrinsic complexity of the heap structures allocated and manipulated by such programs, any attempt to formalize their correctness has to be aware of the inherent bounds of undecidability. Indeed, even programs working on simple acyclic lists have the power of Turing machines, and it is expected that a general logic describing sets of configurations reached in such programs has an undecidable satisfiability (or validity) problem. An interesting problem is to define decidable logics that are either specialized for a certain kind of recursive data structures (e.g. lists, trees), or that are restricted by the quantifier prefix.

This paper presents an extension of a decidable fragment of Separation Logic for singly-linked lists, defined by Berdine, Calcagno and O'Hearn [8] and used as an internal representation for sets of states in the Smallfoot tool [4]. Our main extension consists in introducing atomic formulae of the form $ls^k(x,y)$ describing a list segment of length $k$, stretching from $x$ to $y$, where $k$ is a logical variable interpreted over positive natural numbers, that may occur further inside Presburger constraints. This is motivated by the need to reason about programs that work on both singly-linked list structures and integer variables (counters). We denote the extended logic as Quantitative Separation Logic (QSL).

In reality, many programs would traverse a list structure, while performing some iterative computation on the integer variables. The result of this computation usually depends on the number of steps, which, in turn, depends of the length of the list. A specification of the correct behavior for such a program needs to take into account both the lengths of the lists and the values of the counters.

We study the decidability properties of the full first-order logic combining unrestricted quantification of arithmetic and location variables. Although the full logic is found to be undecidable, validity of entailments between formulae with the quantifier prefix in the language $∃*{∃_N, ∀_N}^*$ is decidable. We provide here a model theoretic method for decidability, based on a parametric notion of shape graphs. As a byproduct, we obtain a decision procedure for the fragment of Separation Logic considered in [8].

The decision procedure for a fragment of QSL is currently implemented in the L2CA tool [3], a tool for translating programs with singly-linked lists into bisimilar counter automata, according to the method of [9], which opens the possibility of using well-known counter automata techniques and tools, e.g. [6,19,5], in order to verify pre- and post- conditions expressed in QSL, on programs working on both singly-linked lists and integer variables.

## 1.1 Related Work

The saga of logics for describing heap structures has its roots in the early work of Burstall [10]. Later on, work by Benedikt, Reps and Sagiv [7], Reynolds [18] and Ishtiaq and O'Hearn [12], has brought the subject into focus, whereas recent advances have been made in tackling the decidability problem [11,8,20]. The work that is closest to ours is the one of Berdine, Calcagno and O'Hearn [8], which defines a decidable subset of Separation Logic [18] interpreted over singly-linked heap models. The work in this paper is in fact an extension of the logic in [8] with integer variables representing list lengths. One of the main challenges in the present paper was to adapt the model of parametric shape graphs in order to cope with
the notion of disjunctive heaps, which is the essence of the semantic model for Separation Logic.

Recently, Magill et al. [14] report on a program analysis technique that uses Separation Logic [18] extended with first-order arithmetic. However, the main emphasis of [14] is a program analysis based on counterexample-driven abstraction refinement, whereas our work focuses on distinguishing decidable from undecidable when combining Separation Logic with first-order arithmetic. As a matter of fact, [14] claims that validity of entailments in the purely existential fragment of Separation Logic with the $ls^k(x,y)$ predicate and linear constraints is decidable, without giving the proof, by analogy to the proof-theoretic method from [8]. We extend their result by showing decidability of the validity of entailments in the $∃^*\{∃_N, ∀_N\}^*$ fragment, versus undecidability of satisfiability in the $∃^*∃_N^*(∀|∀_N)∃^*∃_N^*$ fragment (or equivalently, validity in the $∀^*∀_N^*(∃|∃_N)∀^*∀_N^*$ fragment).

## 2 Definitions

In the rest of the paper, for a set $A$ we denote by $A_⊥$ the set $A \cup \{⊥\}$. For a function $f: A \to B$, we denote by $dom(f) = \{x \in A | f(x) \neq ⊥\}$ its domain and by $img(f) = \{y \in B | ∃x \in A. f(x) = y\}$ we denote its image. The element $⊥$ is used to denote that a (partial) function is undefined at a given point, e.g. $f(x) = ⊥$. For a function $f: A \to B$ and a set $S \subseteq A$, we denote by $f|_S$ the restriction of $f$ to $S$. Sometimes we shall use the graph notation for functions, i.e. $f = \{(a,b),...\}$ if $f(a) = b, ...,$. The notation $\lambda x : A.y$ stands for the function $\{(x,y) | x \in A\}$, and $\lambda x : A.⊥$ is the empty function $\emptyset$, by convention. Let $Part(S)$ denote the set of all partitions of the set $S$.

We denote by $\mathbb{N}$ the set of positive integer numbers, including zero. By $\mathcal{T}(X)$ we denote the set of all terms build using variables $x \in X$. For a term (formula) $\tau(X)$ and a mapping $\mu: X \to \mathcal{T}(X)$, we denote by $\tau[\mu]$ the term (formula) in which each occurrence of $x$ is replaced with $\mu(x)$. For a formula $\varphi$, we denote as $FV(\varphi)$ the set of its free variables. If we denote a formula by $\varphi(\mathbf{x})$ then we implicitly assume that $\mathbf{x} \subseteq FV(\varphi)$. If $\varphi$ is a formula of the first-order arithmetic of integers, and $\nu: FV(\varphi) \to \mathbb{N}$ is an interpretation of its free variables, we denote by $\nu|\varphi$ the fact that $\varphi[\nu]$ is a valid formula.

Presburger arithmetic $\langle \mathbb{N}, +, 0, 1 \rangle$ is the theory of first-order logic of addition and successor function [17]. The interpretation of logical variables is the set of natural numbers $\mathbb{N}$, and the meaning of the function symbols $0, 1, +$ is the natural one. It is well-known that the satisfiability problem for Presburger arithmetic is decidable [17].

<table><caption>**Fig. 1** Separation Logic with Presburger Arithmetic</caption><tr><td>u, v, ... ∈ PVar</td><td>program variables</td></tr><tr><td>x, y, ... ∈ LVar</td><td>location variables</td></tr><tr><td>k, l, ... ∈ IVar</td><td>integer variables</td></tr><tr><td>L</td><td>:= nil | u | x</td><td>location expressions</td></tr><tr><td>I</td><td>:= n ∈ N | k | I + I</td><td>integer expressions</td></tr><tr><td>A</td><td>:= I = I | L = L | emp | L ↦→ L | ls<sup>I</sup>(L, L)</td><td>atomic propositions</td></tr><tr><td>F</td><td>:= T | A | ¬F | F ∧ F | F * F | ∃x. F | ∃<sub>N</sub> k. F</td><td>formulae</td></tr></table>

The syntax of QSL is given in Figure 1. Notice the difference between *program variables* $PVar$ and *location variables* $LVar$, the former being logical constants, whereas the
latter may occur within the scope of a quantifier (∃). The logic uses a third kind of variables, namely *integer variables*, quantified over natural numbers (∃<sub>N</sub>). For a formula φ of QSL, we denote by *LFV*(*φ*) = *FV*(*φ*) ∩ *LVar* the set of free location variables, and by *IFV*(*φ*) = *FV*(*φ*) ∩ *IVar* the set of free integer variables.

As usual, we define φ ∨ ψ ≜ ¬(¬φ ∧ ¬ψ), φ ⇒ ψ ≜ ¬φ ∨ ψ, ∀x . φ ≜ ¬∃x . ¬φ and
∀<sub>N</sub> k . φ ≜ ¬∃<sub>N</sub> k' . ¬φ. Moreover, we write k ≤ l and ls(x,y) as shorthands for ∃<sub>N</sub> k' . k + k' = l
and ∃<sub>N</sub> k . ls<sup>k</sup>(x,y), respectively. F is a shorthand for ¬T. The bounded quantifiers ∃<sub>N</sub> m ≤
n . φ(m) and ∀<sub>N</sub> m ≤ n . φ(m) are used instead of ∃<sub>N</sub> m . m ≤ n ∧ φ(m) and ∀<sub>N</sub> m . m ≤ n ⇒
φ(m), respectively. We shall also deploy some of the classical shorthands in Separation
Logic: x ↦→ ... ≜ ∃y . x ↦→ y, and x ↔ y ≜ x ↦→ y ∗ T, where y is either a location variable or
nil. For list segment formulae we define l̃s<sup>k</sup>(x,y) ≜ ls<sup>k</sup>(x,y) ∗ T and l̃s(x,y) ≜ ls(x,y) ∗ T.

The semantics of QSL formulae is given in terms of heaps. A *heap* is a rooted graph in which each node has at most one successor. Let *Loc* denote the set of *locations*. We assume henceforth that *Loc* is an infinite, countable set, with a designated element *nil* ∈ *Loc*.

Remark We identify heaps that differ only by a renaming of their locations.

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

**Definition 1** A heap is a pair $H = (s, h)$, where $s: PVar \cup LVar \to Loc_\perp$ associates variables with locations, and $h: Loc \to Loc_\perp$ is the partial successor mapping. In particular, we have $h(nil) = \perp$. We denote by $\mathcal{H}$ the set of all heaps with variables from $PVar \cup LVar$ and locations from $Loc$.

If $H = (s, h)$ is a heap, $x \in LVar$ a location variable and $l \in Loc_\perp$, we denote as $H[x \leftarrow l] = \langle s[x \leftarrow l], h \rangle$ the heap in which $x$ is assigned $l$. The interpretation of a formula is given in terms of a forcing relation $|=$ between pairs $\langle H, l \rangle$, where $H \in \mathcal{H}$ is a heap and $l: IVar \to \mathbb{N}$ is a valuation of integer variables. For a logical term $t$, we denote by $\mathcal{V}_{\langle H,l \rangle}(t)$ the valuation of $t$ in $\langle H, l \rangle$. The semantics of QSL formulae is given below, for a given heap $H = (s, h)$:

$$
\mathcal{V}_{\langle H, l \rangle}(u) = s(u), \quad \mathcal{V}_{\langle H, l \rangle}(x) = s(x), \quad \mathcal{V}_{\langle H, l \rangle}(\text{nil}) = \text{nil}
$$

<table>
  <tr>
    <td>&lt;H, 1&gt; &harr; T</td>
    <td>always</td>
  </tr>
  <tr>
    <td>&lt;H, 1&gt; &harr; L<sub>1</sub> = L<sub>2</sub></td>
    <td>&#x2212;V<sub>&lt;H,1&gt;</sub>(L<sub>1</sub>) &ne; &perp;, &#x2212;V<sub>&lt;H,1&gt;</sub>(L<sub>2</sub>) &ne; &perp; and<br/>&#x2212;V<sub>&lt;H,1&gt;</sub>(L<sub>1</sub>) = &#x2212;V<sub>&lt;H,1&gt;</sub>(L<sub>2</sub>)</td>
  </tr>
  <tr>
    <td>&lt;H, 1&gt; &harr; emp</td>
    <td>h = &empty;</td>
  </tr>
  <tr>
    <td>&lt;H, 1&gt; &harr; L<sub>1</sub> &mapsto; L<sub>2</sub></td>
    <td>&#x2212;V<sub>&lt;H,1&gt;</sub>(L<sub>1</sub>) &ne; &perp;, &#x2212;V<sub>&lt;H,1&gt;</sub>(L<sub>2</sub>) &ne; &perp; and<br/>h = {&lt; &#x2212;V<sub>&lt;H,1&gt;</sub>(L<sub>1</sub>), &#x2212;V<sub>&lt;H,1&gt;</sub>(L<sub>2</sub>) &gt;}</td>
  </tr>
  <tr>
    <td>&lt;H, 1&gt; &harr; &not;&phi;</td>
    <td>&lt;H, 1&gt; &ne; &phi;</td>
  </tr>
  <tr>
    <td>&lt;H, 1&gt; &harr; &phi; &and; &psi;</td>
    <td>&lt;H, 1&gt; &harr; &phi; and &lt;H, 1&gt; &harr; &psi;</td>
  </tr>
  <tr>
    <td>&lt;H, 1&gt; &harr; &phi; * &psi;</td>
    <td>there exist H<sub>1</sub>, H<sub>2</sub> such that H = H<sub>1</sub> &bull; H<sub>2</sub><br/>and &lt;H<sub>1</sub>, 1&gt; &harr; &phi;, &lt;H<sub>2</sub>, 1&gt; &harr; &psi;</td>
  </tr>
  <tr>
    <td>&lt;H, 1&gt; &harr; &exists;x . &phi;</td>
    <td>&lt;H[x &leftarrow; l], 1&gt; &harr; &phi; for some l &isin; Loc</td>
  </tr>
</table>

Here $H_1 \bullet H_2$ denotes the disjoint union of $H_1 = \langle s, h_1 \rangle$ and $H_2 = \langle s, h_2 \rangle$, i.e, $dom(h_1) \cap dom(h_2) = \emptyset$, $h = h_1 \cup h_2$. The above definitions are standard in Separation Logic [18]. The rules below are specific to our extension:
$$ \mathcal{V}_{\langle H, \mathfrak{t} \rangle}(I) = I[\mathfrak{t}] $$

<table>
  <tr>
    <td>⟨H, t⟩ ⊨ I<sub>1</sub> = I<sub>2</sub></td>
    <td>iff</td>
    <td>V<sub>⟨H,t⟩</sub>(I<sub>1</sub>) = V(I<sub>2</sub>)<sub>⟨H,t⟩</sub></td>
  </tr>
  <tr>
    <td>⟨H, t⟩ ⊨ ls<sup>0</sup>(L<sub>1</sub>, L<sub>2</sub>)</td>
    <td>iff</td>
    <td>⟨H, t⟩ ⊨ L<sub>1</sub> = L<sub>2</sub> ∧ emp</td>
  </tr>
  <tr>
    <td>⟨H, t⟩ ⊨ ls<sup>n+1</sup>(L<sub>1</sub>, L<sub>2</sub>)</td>
    <td>iff</td>
    <td>⟨H, t⟩ ⊨ ∃x . ls<sup>n</sup>(L<sub>1</sub>, x) * x ↦→ L<sub>2</sub></td>
  </tr>
  <tr>
    <td>⟨H, t⟩ ⊨ ls<sup>t</sup>(L<sub>1</sub>, L<sub>2</sub>)</td>
    <td>iff</td>
    <td>⟨H, t⟩ ⊨ ls<sup>V<sub>⟨H,t⟩</sub>(I)</sup>(L<sub>1</sub>, L<sub>2</sub>)</td>
  </tr>
  <tr>
    <td>⟨H, t⟩ ⊨ ∃<sub>N</sub> k . φ</td>
    <td>iff</td>
    <td>⟨H, t[k ← n]⟩ ⊨ φ, for some n ∈ N</td>
  </tr>
</table>

There are two types of quantifiers, $∃$ ranges over locations *Loc*, and $∃_N$ over natural numbers $N$. A pair $⟨H, t⟩$ is said to be a model of $φ$ iff $⟨H, t⟩ ⊨ φ$. If $IFV(φ) = \emptyset$, we denote the fact that $H$ is a model of $φ$ simply as $H ⊨ φ$.

An *entailment* is a formula of type $φ \Rightarrow ψ$. Given such an entailment, the validity problem asks if it holds for any pair $⟨H, t⟩$, i.e. if any model of $φ$ is also a model of $ψ$. Theorem 2 proves the decidability of entailments between formulae in the $∃^*\{∃_N, ∀_N\}^*$ fragment of QSL, i.e. formulae of the form $∃x_1...∃x_n Q_1 k_1...Q_m k_m$. $θ(x_1...x_n, k_1...k_m)$, where $θ$ is a quantifier-free formula, and $Q_1, ..., Q_m ∈ \{∃_N, ∀_N\}$.

Given a heap $H = ⟨s, h⟩$ and a set of location variables $x \subseteq LVar$, a location $l \in dom(h)$ is said to be reachable from $x$ in $H$ if and only if there exists a finite sequence of locations $l_0, l_1, ..., l_n$ such that $l_0 \in s(x)$ for some $x \in x$, $l_n = l$ and $h(l_i) = l_{i+1}$, for all $0 \le i < n$. Let $\mathcal{R}_x(H)$ be the set of locations reachable from $x$ in $H$. We denote by $H↓_x$ the heap $⟨s, h↓_{\mathcal{R}_x(H)}⟩$. The following Lemma is needed for technical reasons.

**Lemma 1** Let $x = \{x_1, ..., x_n\}$ be a set of location variables and $k = \{k_1, ..., k_m\}$ be a set of integer variables. Given a heap $H \in \mathcal{H}$, and a quantifier-free formula $θ(x, k)$, then for all $Q_1, ..., Q_m \in \{∃_N, ∀_N\}$, $H \models Q_1 k_1 ... Q_m k_m$. $θ(x, k)$ if and only if $H↓_x \models Q_1 k_1 ... Q_m k_m$. $θ(x, k)$.

*Proof* It is sufficient to prove that, for all valuations $t: k \to N$:

$$ ⟨H, t⟩ \models \theta \iff ⟨H↓_x, t⟩ \models \theta $$

By induction on the structure of $θ$:

- the cases where $θ$ is $T$ or emp are trivial.

- the cases where $θ$ is either $x = y$, $x \mapsto y$ or $ls^t(x, y)$, for $x \in x$ and $t$ being an arithmetic term, are immediate, since $V_{⟨H,t⟩}(x) \neq \emptyset$, $V_{⟨H,t⟩}(y) \neq \emptyset$, and all locations on the path from $V_{⟨H,t⟩}(x)$ to $V_{⟨H,t⟩}(y) \neq \emptyset$ are reachable from $x$.

- the cases where $θ$ is either $x = \text{nil}$, $x \mapsto \text{nil}$ or $ls^t(x, \text{nil})$ are similar to the above point.

- if $θ = \neg φ$, $⟨H, t⟩ \models \neg φ \iff ⟨H, t⟩ \nvDash φ \iff ⟨H↓_x, t⟩ \nvDash φ \iff ⟨H↓_x, t⟩ \models \neg φ$. We have used the induction hypothesis.

- if $θ = φ_1 \wedge φ_2$, let $x_1 = LFV(φ_1)$ and $x_2 = LFV(φ_2)$. By induction hypothesis $⟨H, t⟩ \models φ_1 \iff ⟨H↓_{x_1}, t⟩ \models φ_1$ and $⟨H, t⟩ \models φ_2 \iff ⟨H↓_{x_2}, t⟩ \models φ_2$. Since the variables from $x_2 \setminus x_1$ do not appear in $φ_1$, we also have $⟨H, t⟩ \models φ_1 \iff ⟨H↓_x, t⟩ \models φ_1$, and similar for $φ_2$. Hence the conclusion follows.

- if $θ = φ_1 * φ_2$

☐
**Remark** Consequently, a formula $\varphi$ from the $∃^*\{∃_N, ∀_N\}^*$ fragment of QSL has a model if and only if it has a model in which all locations are reachable from at most *n* locations (that we will subsequently call *roots*), where *n* is the size of the existential prefix of $\varphi$. □

The following notion of dangling location is essential for the semantics of Separation Logic on heaps [12],[18]. To understand this point, consider the formula $\varphi: u \mapsto v * v \mapsto \text{nil}$, describing a heap $H = \langle s, h \rangle$, in which $u$ and $v$ are allocated to two different cells, i.e. $s(u) = l_1$, $s(v) = l_2$, and nothing else is in the domain of the heap, i.e. $h = \{\langle l_1, l_2 \rangle, \langle l_2, \text{nil} \rangle\}$. The reason for which $H \models \varphi$, is that there exists two disjoint heaps, namely $H_1 = \langle s, \{\langle l_1, l_2 \rangle\} \rangle$ and $H_2 = \langle s, \{\langle l_2, \text{nil} \rangle\} \rangle$, such that $H_1 \models u \mapsto v$ and $H_2 \models v \mapsto \text{nil}$. Notice the role of the location $l_2$, pointed to by the variable $v$, which is referenced by the first heap, but allocated in the second one. This location ensures that the disjoint union of $H_1$ and $H_2$ is defined, and that $H_1 \bullet H_2 \models u \mapsto v * v \mapsto \text{nil}$.

**Definition 2** A location $l \in \text{Loc} \setminus \{\text{nil}\}$ is said to be dangling in a heap $H = \langle s, h \rangle$ iff $l \in (\text{img}(s) \cup \text{img}(h)) \setminus \text{dom}(h)$.

In the following, we denote by $dng(H)$ the set of all dangling nodes of $H$, and by $\text{loc}(H) = \text{img}(s) \cup \text{dom}(h) \cup \text{img}(h)$ the set of all locations, either defined or dangling, in $H$.

### 3 Motivating Example

Let us consider the program in Figure 2. The loop on the left hand side inserts elements into the list pointed to by $u$, while incrementing the $c$ counter, and the loop on the right removes the elements in reversed order, while decrementing $c$. The pre- and post-condition of the program are inserted as Hoare-style annotations. Both initially and finally, the value of $c$ is zero and the heap is empty.

```
{c = 0 ∧ emp ∧ u = nilo}
1: while ... do
{c ≥ 0 ∧ c = k ∧ ls^k(u, nil)}
2:     t := new;
3:     t.next := u;
4:     u := t;
5:     c := c + 1;
6: od
7: while c ≠ 0 do
{c > 0 ∧ c = k ∧ ls^k(u, nil)}
8:     u := u.next;
9:     c := c - 1;
10: od
{c = 0 ∧ emp}
```

<caption>**Fig. 2** Program verification using QSL</caption>

In order to prove that the program terminates without a null pointer dereferencing, and moreover ensuring that the post-condition holds, one needs to relate the value of $c$ to the length of the list pointed to by $u$, as it is done in the invariants of the left and right hand side : $c = k ∧ ls^k(u, nil)$. This example could not be handled using standard Separation Logic, since we explicitly need the ability of reasoning about both list lengths and integer variables.
## 4 Undecidability of QSL

In this section we prove the undecidability of the QSL logic. Namely the class of formulae with quantifier prefix in the language $∃^*∃_N^*(\forall | ∀_N)∃^*∃_N^*$ are shown to have an undecidable satisfiability problem. It is to be noticed that undecidability of QSL is not a direct consequence of the undecidability of Separation Logic [16], since the proof in [16] uses multiple selector heaps, while in this case we consider only heaps composed of singly-linked lists. Our result is non-trivial since it is well-known also that, e.g. FOL, MSOL are decidable when interpreted over singly-linked lists, and become quickly undecidable when interpreted over grid-like, and more general graph structures.

**Theorem 1** The set of QSL formulae which, written in prenex normal form, have the quantifier prefix in the language $∃^*∃_N^*(\forall | ∀_N)∃^*∃_N^*$, is undecidable.

*Proof* The proof is by reduction from the halting problem for 2-counter machines. A 2-counter machine $M$ [15] with non-negative counters $c_1, c_2$ is a sequential program:

$$0 : ins_1; 1 : ins_2; \dots; n-1 : ins_n;$$

where $ins_n$ is a halt instruction and $ins_i$ with $i = 1, 2, \dots, n-1$ are instructions of the following two types, for $0 \le k, k_1, k_2 < n$, and $j = 1, 2$:

1. $c_j = c_j + 1$; goto $k$;

2. if $c_j = 0$ then goto $k_1$ else ($c_j = c_j - 1$; goto $k_2$);

The machine starts executing at label 0 with values $c_1 = c_2 = 0$. When it reaches the control location $k-1$, it executes the instruction $ins_k$ i.e, it modifies the values of the counter and jumps to the next label according to the instruction. Formally, we use the relation $\langle q, v_1, v_2 \rangle \vdash_M \langle q', v_1, v_2 \rangle$ to describe a one-step transition of $M$ between two configurations, where $q, q' \in \{0, \dots, n-1\}$ are the control labels, $v_1, v_2$ and $v'_1, v'_2$ are the values of the counters before and after the transition. The machine halts when it reaches the halt instruction at label $n$. It is undecidable whether a given 2-counter machine halts [15].

Given a 2-counter machine $M$, we build a closed formula $\Psi_M$ in the language of QSL, describing any terminating computation of $M$. It follows that $M$ halts if and only if $\Psi_M$ is satisfiable, i.e. there exists $\langle s, h \rangle \in (LVar \mapsto Loc_\perp) \times (Loc \mapsto Loc_\perp)$ such that $\langle s, h \rangle \models \Psi_M$. Let $\Psi_M$ be the following formula:

$$ \exists x, x' \exists_N n . x \mapsto x' * \tilde{l}s^n (x', \text{nil}) \wedge \forall_N m < n . \exists y, y', q, q', c_1, c'_1, c_2, c'_2 \exists_N l, l', v_1, v'_1, v_2, v'_2 . \\ \tilde{l}s^m (x', y) * y \mapsto y' * ls^l (q, y) * ls^{v_1} (c_1, y) * ls^{v_2} (c_2, y) * ls^{l'} (q', y') * ls^{v'_1} (c'_1, y') * ls^{v'_2} (c'_2, y') \\ \wedge \bigvee_i^n \tau_i (l, v_1, v_2, l', v'_1, v'_2) $$

The intuition behind this formula is given in Figure 3. Here $x$ points to a list segment of length $n$ that represents a halting computation of $M$. Each element $y$ in this list represents a configuration $\langle l, v_1, v_2 \rangle$ of $M$, where $l$ is encoded by a list segment $ls^l(q, y)$, and $v_1, v_2$ by the list segments $ls^{v_1}(c_1, y)$ and $ls^{v_2}(c_2, y)$, respectively. The spatial formula $x \mapsto x'$ states the initial condition $l = v_1 = v_2 = 0$, i.e. no other list is pointing to $x$, while the halting condition is captured by $\tilde{l}s^n(x', \text{nil})$, which ensures that the list is of finite length. The transition relation between any two intermediate configurations, represented by the adjacent locations $y$ and $y'$, is captured by the $\tau_i(l, v_1, v_2, l', v'_1, v'_2)$ formulae, given by the description of $M$. Namely, if:

$$- ins_i \text{ is } [c_j = c_j + 1; \text{goto } k], \text{ then } \tau_i : l = i \wedge l' = k \wedge v'_j = v_j + 1,$$
<figure><img src="image_2.png" /><figcaption>Fig. 3</figcaption></figure>

- $ins_i$ is $[\text{if } c_j = 0 \text{ then goto } k_1 \text{ else } (c_j = c_j - 1; \text{ goto } k_2)], \text{ then } \tau_i : l = i \land ((v_j = 0 \Rightarrow l' = k_1) \land (v_j \neq 0 \Rightarrow (v'_j + 1 = v_j \land l' = k_2)))$.

By taking a closer look at the form of $\Psi_M$, one can notice that the undecidability of the $∃^*∃_N^*∀_N∃^*∃_N^*$ fragment of QSL has been proved. The cause for undecidability is the alternation between (existential) location and (universal) integer quantifiers, which enables arbitrarily large and complex models to be described. Using a similar argument, we can establish undecidability of the $∃^*∃_N^*∀∃^*∃_N^*$ fragment of QSL, by changing the above formula into:

$$ \exists x, x'∃_N n . x \mapsto x' * \tilde{l}s^n(x', \text{nil}) \land \forall y . \tilde{l}s(x', y) \Rightarrow ∃y', q, q', c_1, c'_1, c_2, c'_2∃_N l, l', v_1, v'_1, v_2, v'_2 . \\ y \leftrightarrow y' * ls^l(q, y) * ls^{v_1}(c_1, y) * ls^{v_2}(c_2, y) * ls^{l'}(q', y') * ls^{v'_1}(c'_1, y') * ls^{v'_2}(c'_2, y') \land \\ \bigvee_i^n \tau_i(l, v_1, v_2, l', v'_1, v'_2) $$

□

In the following developments, we shall prove that logical entailment in the $∃^*∃_N^*∀_N∃^*∃_N^*$ fragment of QSL is decidable. We have found no argument for (un)decidability concerning the quantifier prefix fragment $\{∃, ∀\}^*\{∃_N, ∀_N\}^*$. In particular, all attempts to reduce (from) to known fragments of MSO with cardinality constraints [13] have failed.

## 5 Model Theoretic Method

The validity of an entailment $\varphi \Rightarrow \psi$ is equivalent to the non-satisfiability of the formula $\varphi \land \neg \psi$, i.e. there should be no tuples $(H, v, i)$ such that $\langle H, v, i \rangle \models \varphi$ and $\langle H, v, i \rangle \not\models \psi$. Our main result, leading immediately to decidability of entailments, is that, if $\varphi$ is of the form $∃x_1...∃x_nQ_1l_1...Q_m l_m . \theta(x, l)$, with $Q_i \in \{∃_N, ∀_N\}$ and $\theta$ is a boolean combination of predicates with $¬$, $∧$ and $*$, all models $(H, v, i)$ of $\varphi$ can be represented using a finite number of (finite) structures called symbolic graph representations (SGR).

The decision procedure for the validity of a QSL entailment $\varphi \Rightarrow \psi$ is based on the following idea. We first define operators on sets of SGRs that are the counterparts of the logical connectives $\vee$, $∧$, $*$ and the existential quantifiers $∃x, ∃_N x$. Second, for each existential QSL formula $\varphi$, we compute a set $[[\varphi]]$ of SGRs that represent all models of $\varphi$. The construction of this set is recursive, on the structure of $\varphi$. The entailment $\varphi \Rightarrow \psi$ is valid iff the set $[[\varphi]] \ominus [[\psi]]$ is empty, where $\ominus$ is an operator defined on SGRs, that computes the representation of the difference between the set of concrete models of the $\varphi$ and the one of $\psi$. Last, the emptiness problem for sets of SGRs is shown to be decidable, by reduction to the satisfiability problem for the Presburger arithmetic.
## 5.1 Symbolic Shape Graphs

In this section we define a finite representation of (possibly infinite) sets of heaps, called symbolic shape graphs (SSG), which is the essence of our decision method. The next section defines the SGR representation for sets of heaps, which is based on SSGs and arithmetic constraints.

**Definition 3** Given a heap $H = \langle s, h \rangle \in \mathcal{H}$, a location $l \in \text{Loc}$ is said to be a cut point in $H$ if either $l \in \text{img}(s)$, (2) $l$ is dangling or `nil`, or (3) $l$ has more than one predecessor in the heap. We denote by $l_1 \succcurlyeq_H l_2$ the fact that $h(l_1) = l_2$ and $l_2 \neq \perp$ is not a cut point in $H$. Let $\sim_H$ denote the reflexive, symmetric and transitive closure of the $\succcurlyeq_H$ relation, i.e. the smallest equivalence relation that includes $\succcurlyeq_H$, and $[l]_{\sim}$ be the equivalence class of $l \in \text{Loc}$ w.r.t. $\sim_H$. We also refer to these equivalence classes as to *list segments*. By convention, we have $[\perp]_{\sim} = \perp$. Let $H_{/\sim} = \langle s_{/\sim}, h_{/\sim} \rangle$ be the *quotient heap*, where:

- $s_{/\sim}: PVar \cup LVar \to Loc_{/\sim_{\perp}}$ and $s_{/\sim}(u) = [s(u)]_{\sim}$, for all $u \in PVar$,

- $h_{/\sim}: Loc_{/\sim} \to Loc_{/\sim_{\perp}}$ and for all $l \in \text{dom}(h)$, if $h(l) = l'$ and $l'$ is either $\perp$ or a cut point in $\langle s, h \rangle$, then $h_{/\sim}([l]) = [l']_{\sim}$. In particular, $h_{/\sim}([l]) = \perp$, for all $l \notin \text{dom}(h)$.

Note that $s_{/\sim}$ and $h_{/\sim}$ are well-defined functions. We extend the rest of notations to quotient heaps, i.e. $\text{dng}(H_{/\sim}) = \{[l]_{\sim} | l \in \text{dng}(H)\}$ and $\text{loc}(H/\sim) = \{[l]_{\sim} | l \in \text{loc}(H)\}$.

For example, in the heap from Figure 4 (a), the cut points are marked by hollow nodes and the $\sim$-equivalence classes are enclosed in solid boxes. The quotient heap is the heap in which these boxes are taken as nodes, instead of the individual locations.

**Definition 4** Given a set $PVar$ of program variables, a set $LVar$ of location variables, and a set of counters $Z = \{z_1, \dots, z_n\}$, a *symbolic shape graph (SSG)* is a tuple $G = \langle N, D, R, Z, S, V \rangle$, where:

- $N$ is a finite set of symbolic nodes, with a designated node $\text{Nil} \in N$,

- $D \subseteq N$ is a set of symbolic dangling nodes,

- $R \subseteq N$ is a set of symbolic root nodes,

- $Z: N \setminus D \to Z$ is an injective function assigning each node to a counter,

- $S: N \to N_{\perp}$ is the successor function, where:

- $S(\text{Nil}) = \perp$ and $S(d) = \perp$, for all $d \in D$,

- $S(n) \notin R$, for all $n \in N$,

- $S(n) \in N$, for all $n \in N \setminus (D \cup \{\text{Nil}\})$.

- $V: PVar \cup LVar \to N$ assigns program and location variables with nodes.

Intuitively, each node of a SSG represents a list segment of a concrete heap. The node `Nil` stands for the concrete `nil` location, and each symbolic dangling node represents one dangling location.

**Definition 5** An SSG $G = \langle N, D, R, Z, S, V \rangle$ is said to be in normal form if:

- each node in $n \in N \setminus \{\text{Nil}\}$ is reachable either from $V(u)$, for some $u \in PVar \cup LVar$, or from some symbolic root $r \in R$, and

- either $n \in \text{img}(V) \cup D \cup \{\text{Nil}\}$, or there exist two distinct nodes $n_1, n_2 \in N$ such that $S(n_1) = S(n_2) = n$.
$S_k$ denotes the set of SSGs in normal form, with $|R| \le k$ and $\mathrm{img}(V) \subseteq PVar \cup LVar$.

Sometimes we denote by $\mathcal{S}$ the union $\bigcup_{k \in \mathbb{N}} S_k$. We identify SSGs which are equivalent under renaming of nodes and counters. The following was proved in [9]:

**Lemma 2** Let $G = \langle N, D, R, Z, S, V \rangle \in S_k$ be a normal form SSG. Then, $|N| \le 2(|dom(V)| + |R|)$. As a consequence, the number of such SSGs is bounded asymptotically by $2(|PVar| + |LVar| + k)^{2(|PVar|+|LVar|+k)}$, and the bound is tight.

The following definition relates the notions of heap and SSG.

**Definition 6** Let $G = \langle N, D, R, Z, S, V \rangle \in \mathcal{S}$ be a SSG, $v : dom(V) \cap LVar \to dom(h)$ a valuation of the location variables of $G$, and $l : img(Z) \to \mathbb{N}^+$ a valuation of the counters in $G$. Let $H = \langle s, h \rangle \in \mathcal{H}$ be a heap such that $dom(s) = dom(V) \cap PVar$, and $H_{/\sim} = \langle s_{/\sim}, h_{/\sim} \rangle$ be the quotient of $H$ with respect to $\sim_H$. We say that $H$ is the $\langle v, l \rangle$-concretization of $G$ iff there exists a bijective mapping $\eta : N_{\perp} \to (loc(h_{/\sim}) \cup \{nil, \perp\})$ such that:

- $\eta(\mathit{Nil}) = \{\mathit{nil}\}$ and $\eta(\perp) = \perp$,

- $\eta(V(u)) = s_{/\sim}(u)$, for all $u \in PVar$,

- $\eta(S(n)) = h_{/\sim}(\eta(n))$, for all $n \in N \setminus D$,

- $\eta(n) \in \mathrm{dng}(H_{/\sim})$, for all $n \in D$,

- $\eta(n) \notin \{\mathit{nil}, \perp\}$ and $l(Z(n)) = |\eta(n)|$, for all $n \in N \setminus D$.

We recall upon the fact that heaps are identical, up to isomorphism, which implies that the $\langle v, l \rangle$-concretization is uniquely defined. We say that $H$ is a concretization of $G$ if there exist $v, l$ such that $H$ is the $\langle v, l \rangle$-concretization of $G$. Roughly speaking, the $\langle v, l \rangle$-concretization of a SSG $G$ is the heap obtained by replacing each node $n$ of $G$ with a list segment whose length equals the value of the counter $Z(n)$. Moreover, if $G$ has a $\langle v, l \rangle$-concretization, we must have $l(Z(n)) > 0$, for all non-dangling symbolic nodes $n \in N \setminus D$. Notice also that dangling locations are represented by symbolic dangling nodes. We denote by $\gamma_{v,l}(G)$ the $\langle v, l \rangle$-concretization of $G$ and by $\Gamma(G)$ the set of all concretizations of $G$.

<figure><img src="image_3.png" /><figcaption>**Fig. 4** SSG and Concretization</figcaption></figure>

For example, the SSG in Figure 4 (b) has as $\langle v, l \rangle$-concretization the heap in Figure 4 (a), for the valuations:

- $v(x) = l_3$, $v(y) = l_{10}$, and

- $l(z_1) = 2$, $l(z_2) = 1$, $l(z_3) = 3$, $l(z_4) = 2$, $l(z_5) = 1$, $l(z_6) = 3$.

Notice that the symbolic dangling node pointed to by $w$ corresponds to a dangling location pointed to by $v$ in Figure 4 (a).

The following result expresses the fact that one heap may not be the concretization of two different (non-isomorphic) SSGs:
**Lemma 3** For two non-isomorphic SSGs $G_1, G_2 \in S$, we have $\Gamma(G_1) \cap \Gamma(G_2) = \emptyset$.

*Proof* By contradiction, assume that there exists $H \in \Gamma(G_1) \cap \Gamma(G_2)$. By definition 6, $H/\sim$ is isomorphic to both $G_1$ and $G_2$, thus contradicting the hypothesis that $G_1$ and $G_2$ are non-isomorphic. $\square$

## 5.2 Symbolic Graph Representations

In this section we introduce the notion of symbolic graph representation (SGR) together with a number of operators on these structures. In the next section, we shall provide a stepwise translation of a QSL formula with quantifier prefix $\exists^*\{\exists_N, \forall_N\}^*$ into a set of symbolic graph representations.

A symbolic graph representation is a pair $\langle G, \phi \rangle$, where $G = \langle N, D, R, Z, S, V \rangle$ is a SSG in normal form and $\phi$ an open formula over the counters of $G$, i.e. $FV(\phi) \subseteq img(Z)$. By $G$ we denote the set of all SGRs $\langle G, \phi \rangle$, where $G \in S$ and the set of counters in each $G$ is a subset of $Z$.

A heap $H = \langle s, h \rangle$ is the $\langle v, t \rangle$-concretization of $\langle G, \phi \rangle$ iff $v: dom(V) \cap LVar \to dom(h)$ is a valuation of the location variables of $G$, and $t: img(Z) \to N^+$ is a valuation of the counters in $G$ that satisfies $\phi$, i.e. $t \models \phi$. This is denoted in the following as $H = \gamma_{v,t}(\langle G, \phi \rangle)$. $\Gamma(\langle G, \phi \rangle)$ denotes the set of all $\langle v, t \rangle$-concretizations of $\langle G, \phi \rangle$. The notation is lifted to finite sets of SGRs in the obvious way: $\Gamma(\{R_1, \dots, R_n\}) = \bigcup_{i=1}^n \Gamma(R_i)$.

We introduce now three operators on finite sets of SGRs, that correspond to the boolean operators of union, intersection and set difference. Let $S_1, S_2 \subseteq G$ be two finite sets of SGRs.

$$S_1 \sqcup S_2 = \{ \langle G, \phi_1 \vee \phi_2 \rangle \mid \langle G, \phi_1 \rangle \in S_1 \text{ and } \langle G, \phi_2 \rangle \in S_2 \} \cup \{ \langle G, \phi \rangle \in S_1 \mid \langle G, \neg \phi \rangle \notin S_2 \} \cup \{ \langle G, \phi \rangle \in S_2 \mid \langle G, \neg \phi \rangle \notin S_1 \}$$

$$S_1 \sqcap S_2 = \{ \langle G, \phi_1 \wedge \phi_2 \rangle \mid \langle G, \phi_1 \rangle \in S_1 \text{ and } \langle G, \phi_2 \rangle \in S_2 \}$$

$$S_1 \ominus S_2 = \{ \langle G, \phi_1 \wedge \neg \phi_2 \rangle \mid \langle G, \phi_1 \rangle \in S_1 \text{ and } \langle G, \phi_2 \rangle \in S_2 \} \cup \{ \langle G, \phi \rangle \in S_1 \mid \langle G, \neg \phi \rangle \notin S_2 \}$$

Here the notation $\langle G, \neg \phi \rangle$ stands for any SGR pair having $G$ as its first component. Let $G = \langle N, D, R, Z, S, V \rangle$ and notice that, since $FV(\phi_1) \subseteq img(Z)$ and $FV(\phi_2) \subseteq img(Z)$, then $FV(\phi_1 \vee \phi_2), FV(\phi_1 \wedge \phi_2)$ and $FV(\phi_1 \wedge \neg \phi_2)$ are also subsets of $img(Z)$.

**Lemma 4** SGRs are effectively closed under union, intersection and difference. In particular, we have $\Gamma(S_1 \sqcup S_2) = \Gamma(S_1) \cup \Gamma(S_2)$, $\Gamma(S_1 \sqcap S_2) = \Gamma(S_1) \cap \Gamma(S_2)$ and $\Gamma(S_1 \ominus S_2) = \Gamma(S_1) \setminus \Gamma(S_2)$.

*Proof* We give the proof only for $\sqcup$, the proofs for $\sqcap$ and $\ominus$ being similar. "$\subseteq$" Let $H \in \Gamma(S_1 \sqcup S_2)$. Then either:

- $H \in \Gamma(\langle G, \phi_1 \vee \phi_2 \rangle)$ for some SGRs $\langle G, \phi_1 \rangle \in S_1$ and $\langle G, \phi_2 \rangle \in S_2$. Then either $H \in \Gamma(\langle G, \phi_1 \rangle)$ or $H \in \Gamma(\langle G, \phi_2 \rangle)$. Hence $H \in \Gamma(S_1) \cup \Gamma(S_2)$.

- $H \in \Gamma(\langle G, \phi \rangle)$ for some SGR $\langle G, \phi \rangle \in S_1$. Then obviously $H \in \Gamma(S_1) \cup \Gamma(S_2)$.

- $H \in \Gamma(\langle G, \phi \rangle)$ for some SGR $\langle G, \phi \rangle \in S_2$. This case is symmetric to the above.

"$\supseteq$" Let $H \in \Gamma(S_1) \cup \Gamma(S_2)$. Suppose $H \in \Gamma(S_1)$, the case $H \in \Gamma(H_2)$ being symmetric. Then there exists a SGR $\langle G, \phi \rangle \in S_1$ such that $H \in \Gamma(\langle G, \phi \rangle)$. There are two cases:
1. $\langle G, \psi \rangle \in S_2$ for some $\psi$. Then $\langle G, \phi \lor \psi \rangle \in S_1 \sqcup S_2$, and $H \in \Gamma(\langle G, \phi \lor \psi \rangle)$, which leads to $H \in \Gamma(S_1 \sqcup S_2)$.

2. $\langle G, \psi \rangle \notin S_2$, for any $\psi$. Then $\langle G, \psi \rangle \in S_1 \sqcup S_2$, and $H \in \Gamma(\langle G, \psi \rangle)$, which leads to $H \in \Gamma(S_1 \sqcup S_2)$.

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

The $\oplus$ operator is defined on SGRs with the following meaning : for two SGRs $R_1$ and $R_2$, we have $\Gamma(R_1 \oplus R_2) = \{H_1 \bullet H_2 \mid H_1 \in \Gamma(R_1) \text{ and } H_2 \in \Gamma(R_2)\}$. In other words, $\oplus$ is the SGR counterpart of the disjoint union operator on heaps. However, $\oplus$ is not a total operator, i.e. it is not defined for any pair of SGRs, but only for the ones complying with the following definition:

**Definition 7** Two SSGs $G_i = \langle N_i, D_i, R_i, Z_i, S_i, V_i \rangle$, $i = 1, 2$ are said to match iff there exists a mapping $\mu : D_1 \cup D_2 \to (N_1 \cup N_2)_\perp$ such that, for all $u \in \text{dom}(V_1) \cap \text{dom}(V_2)$, either:

- $V_1(u) \in D_1$ and $\mu(V_1(u)) = V_2(u)$, or

- $V_2(u) \in D_2$ and $\mu(V_2(u)) = V_1(u)$.

and $\mu(d) = \perp$, for all $d \in (D_1 \cup D_2) \setminus (\text{dom}(V_1) \cap \text{dom}(V_2))$.

Intuitively, two SSGs match if it is possible to relate any dangling node pointed to by a program variable in one SSG to a node pointed to by the same variable in the other SSG. Note that two SSGs do not match if the same variable points to some non-dangling node in both. Figure 5 gives an example of two matching SSGs (a) and (b) together with the mapping $\mu$ between their nodes (in dotted lines). According to Definition (7), the choice of $\mu$ is not unique.

<figure><img src="image_5.png" /><figcaption>**Fig. 5** Matching SSGs</figcaption></figure>

Given two SGRs $R_1 = \langle G_1, \phi_1 \rangle$ and $R_2 = \langle G_2, \phi_2 \rangle$, with matching underlying SSGs $G_i = \langle N_i, D_i, R_i, Z_i, S_i, V_i \rangle$, (for the purposes of this definition, we can assume w.l.o.g. that $N_1 \cap N_2 = \{\text{Nil}\}$ and $\text{img}(Z_1) \cap \text{img}(Z_2) = \emptyset$), we define $R_1 \oplus R_2 = \langle G, \phi_1 \land \phi_2 \rangle$, $G = \langle N, D, R, Z, S, V \rangle$, where:

- $N = (N_1 \cup N_2) \setminus \text{dom}(\mu)$,

- $D = (D_1 \cup D_2) \setminus \text{dom}(\mu)$,

- $R = (R_1 \cup R_2) \setminus \text{dom}(\mu)$,

- $Z = Z_1 \cup Z_2$,

- for all $n \in N$:

$$S(n) = \begin{cases} S_i(n) & \text{if } n \in N_i \text{ and } S_i(n) \notin \text{dom}(\mu) \\ \mu(S_i(n)) & \text{if } n \in N_i \text{ and } S_i(n) \in \text{dom}(\mu) \end{cases} \quad i = 1, 2$$
- for all $u \in \text{dom}(V_1) \cup \text{dom}(V_2)$:

$$V(u) = \begin{cases} V_i(u) & \text{if } V_i(u) \notin \text{dom}(\mu) \\ \mu(V_i(u)) & \text{if } V_i(u) \in \text{dom}(\mu) \end{cases} \quad i = 1, 2$$

For example, the SSG in Figure 5 (c) is the result of the ⊗-composition of the SSGs in Figure 5 (a) and (b).

The ⊗ operator is undefined, if $G_1$ and $G_2$ do not match. Notice that if $G_1 \in S_{k_1}$, $G_2 \in S_{k_2}$ and $\langle G, \phi_1 \rangle = \langle G_1, \phi_1 \rangle \otimes \langle G_2, \phi_2 \rangle$, then $G \in S_{k_1+k_2}$. The correctness of the definition is captured by the following Lemma:

**Lemma 5** Given two SGRs $R_1 = \langle G_1, \phi_1 \rangle$ and $R_2 = \langle G_2, \phi_2 \rangle$, such that $G_1$ and $G_2$ match, we have $\Gamma(R_1 \otimes R_2) = \{H_1 \bullet H_2 | H_1 \in \Gamma(R_1), H_2 \in \Gamma(R_2)\}$.

*Proof* Let $G_i = \langle N_i, D_i, R_i, Z_i, S_i, V_i \rangle$, $i = 1, 2$ and $R_1 \otimes R_2 = \langle G, \phi_1 \wedge \phi_2 \rangle$, where $G = \langle N, D, R, Z, S, V \rangle$. W.l.o.g. we assume that $N_1 \cap N_2 = \{\text{Nil}\}$ and $\text{img}(Z_1) \cap \text{img}(Z_2) = \emptyset$. Since $R_1 \otimes R_2$ is defined, there exists a mapping $\mu : D_1 \cup D_2 \to (N_1 \cup N_2)_\perp$, satisfying the conditions of Definition (7).

“$\subseteq$” Assume $H = \langle s, h \rangle \in \Gamma(\langle G, \phi_1 \wedge \phi_2 \rangle)$. Then there exists $v : \text{dom}(V) \cap \text{LVar} \to \text{dom}(h)$ and $t : \text{dom}(Z) \to \mathbb{N}^+$, meeting the conditions of Definition (6). In particular, we have that $t \models \phi_1 \wedge \phi_2$. Let $H_{t/\sim} = \langle s_{t/\sim}, h_{t/\sim} \rangle$ be the quotient of $H$ w.r.t. $\sim_H$. There exists a bijective mapping $\eta : N_\perp \to (\text{loc}(h_{t/\sim}) \cup \{\text{nil}, \perp\})$ meeting the conditions of Definition (6). Let $H_i = \langle s_i, h_i \rangle$, $i = 1, 2$ be the heaps defined as follows:

- $\text{dom}(h_i) = \bigcup_{n \in N_i \setminus \text{dom}(\mu)} \eta(n)$, $h_i(l) = h(l)$, if $l \in \text{dom}(h_i)$, and $h_i(l) = \perp$ otherwise,

- $s_i(u) = s(u)$, for all $u \in \text{PVar}$.

We show that $H_i$ is the $\langle v, t \rangle$-concretization of $G_i$, by considering the bijective mappings $\eta_i$, defined as the restriction of $\eta$ to $N_i$, $i = 1, 2$. Since $t \models \phi_i$, we obtain that $H_i \in \Gamma(\langle G_i, \phi_i \rangle)$. The fact that $H = H_1 \bullet H_2$ is an easy check, based on the facts that $(1) \text{dom}(h_1) \cap \text{dom}(h_2) = \emptyset$, and (2) that all dangling locations of $H_1$ are defined in $H_2$, and viceversa.

“$\supseteq$” let $H = H_1 \bullet H_2$, with $H_i = \langle s_i, h_i \rangle \in \Gamma(\langle G_i, \phi_i \rangle)$, $i = 1, 2$ where $\text{dom}(h_1) \cap \text{dom}(h_2) = \emptyset$. By Definition (6) there exist $v_i : \text{dom}(V_i) \cup \text{LVar} \to \text{dom}(h_i)$ and $t_i : \text{img}(Z_i) \to \mathbb{N}^+$ such that $t_i \models \phi_i$, $i = 1, 2$. Since we assumed $\text{img}(Z_1) \cap \text{img}(Z_2) = \emptyset$, we have $t_1 \cup t_2 \models \phi_1 \wedge \phi_2$. Let $H'_i = \text{Reach}_{v_i}(H)$ and $H'_{i/\sim}$ be as before. There exist two bijective mappings $\eta_i : N_i_\perp \to (\text{loc}(h'_{i/\sim}) \cup \{\text{nil}, \perp\})$ meeting the conditions of Definition (6). Let $\eta$ be the following mapping:

$$\eta(n) = \begin{cases} \eta_1(n) & \text{if } n \in N_1 \setminus \text{dom}(\mu) \\ \eta_2(n) & \text{if } n \in N_2 \setminus \text{dom}(\mu) \\ \perp & \text{otherwise} \end{cases}$$

It is easily checked that $\eta$ is bijective. Now it is left to be checked that $\eta$ satisfies the conditions of Definition (6) in order to conclude that $H \in \Gamma(\langle G, \phi_1 \wedge \phi_2 \rangle)$:

- $\eta(\text{Nil}) = \eta_1(\text{Nil}) = \eta_2(\text{Nil}) = \{\text{nil}\}$ and $\eta(\perp) = \eta_1(\perp) = \eta_2(\perp) = \perp$.

- for all $u \in \text{dom}(V) = \text{dom}(V_1) \cup \text{dom}(V_2)$, for $i = 1, 2$ either:

1. $u \in \text{dom}(V_i)$ and $V_i(u) \notin \text{dom}(\mu)$, then $\eta(V(u)) = \eta_i(V_i(u)) = s_{i/\sim}(u)$. Since $\text{dom}(h_1) \cap \text{dom}(h_2) = \emptyset$, we have $s_{i/\sim}(u) = s_{i/\sim}(u)$.

2. $u \in \text{dom}(V_i)$ and $V_i(u) \in \text{dom}(\mu)$, then $\eta(V(u)) = \eta(\mu(V_i(u))) = \eta_{(i \mod 2)+1}(V_{(i \mod 2)+1}(u)) = s_{(i \mod 2)+1/\sim}(u)$. By the same argument as above, we obtain $\eta(V(u)) = s_{i/\sim}(u)$.

- for all $n \in N = (N_1 \cup N_2) \setminus \text{dom}(\mu)$, for $i = 1, 2$ either:
1. $n \in N_i$ and $S_i(n) \in N_i \setminus dom(\mu)$ then $\eta(S(n)) = \eta_i(S_i(n)) = h_{i/\sim}(\eta_i(n))$. Since $dom(h_1) \cap dom(h_2) = \emptyset$, we have $h_{i/\sim}(\eta_i(n)) = h_{i/\sim}(\eta(n))$.

2. $n \in N_i$ and $S_i(n) \in N_i \cap dom(\mu)$. Then there exists $u \in dom(V_1) \cap dom(V_2)$ such that $S_i(n) = V_i(u) \in D_i$ and $\mu(V_i(u)) = V_{(i \mod 2)_+1}(u)$. In this case we have $S(n) = \mu(S_i(n)) = V_{(i \mod 2)_+1}(u)$. Since $S_i(n) = V_i(u) \in D_i$, by Definition (6) we have $h_{i/\sim}(\eta(n)) = s_{i/\sim}(u) = s_{i \mod 2+1/\sim}(u) = \eta(S(n))$. Since $dom(h_1) \cap dom(h_2) = \emptyset$, we have $h_{i/\sim}(\eta_i(n)) = h_{i/\sim}(\eta(n))$.

- if $n \in D$ then $n \in D_i$ for some $i = 1, 2$. In either case we have $\eta(n) \in dng(H_{i/\sim}) \subseteq H_{i/\sim}$.

- if $n \in N \setminus D$ then $n \in N_i \setminus D_i$, for some $i = 1, 2$. In either case we have $\iota(Z(n)) = \iota_i(Z_i(n)) = |\eta_i(n)| = |\eta(n)|$.

□

The following projection operator captures the effect of dropping one location variable out of the heap. Let $R = \langle G, \phi \rangle$ be an SGR, where $G = \langle N, D, R, Z, S, V \rangle$ is the underlying SSG, and $x \in img(V) \cap LVar$ be a location variable occurring in $G$. For an arbitrary symbolic node $n \in N$, let $prec_G(n) = \{m \in N \mid m \neq n, S(m) = n\}$ be the set of predecessors of $n$, different from itself, in $G$.

We define $R|_x$ to be the SGR, having a normal-form underlying SSG (cf. Definition 4), from which $x$ is missing. Formally, let $R|_x = \langle G', \phi' \rangle$, where:

1. if $x \notin dom(V)$ then $G' = G$ and $\phi' = \phi$.

2. else, if $x \in dom(V)$ and either:

(a) there exists $u \in dom(V) \setminus \{x\}$ such that $V(u) = V(x)$, or

(b) there exist $m_1, m_2 \in dom(S)$ s.t. $m_1 \neq m_2$ and $S(m_1) = S(m_2) = V(x)$
then $G' = \langle N, D, R, Z, S, V[x \leftarrow \perp] \rangle$ and $\phi' = \phi$.

3. else, if $x \in dom(V)$, $V(x) = n$, and for all $u \in dom(V) \setminus \{x\}$, we have $V(u) \neq n$, and either:

(a) $prec_G(n) = \emptyset$, then $G' = \langle N, D, R \cup \{n\}, Z, S, V[x \leftarrow \perp] \rangle$ and $\phi' = \phi$, or

(b) $n \in D$ and $prec_G(n) \neq \emptyset$, then $G' = \langle N, D, R, Z, S, V[x \leftarrow \perp] \rangle$ and $\phi' = \phi$,

(c) $n \notin D$ and $m \in prec_G(n)$, where $Z(m) = k_1$ and $Z(n) = k_2$, then
$G' = \langle N \setminus \{n\}, D, R, Z[m \leftarrow k_3][n \leftarrow \perp], S[m \leftarrow S(n)][n \leftarrow \perp], V[x \leftarrow \perp] \rangle$ and $\phi' = \exists k_1 \exists k_2$. $\phi \wedge k_3 = k_1 + k_2$, where $k_3 \notin img(Z)$ is a fresh counter name.

Notice the effect of the case (3.a) which increases the number of roots in $G$ by one. The correctness of this definition is captured in the following Lemma:

**Lemma 6** Let $R = \langle G, \phi \rangle$ be a SGR, $G = \langle N, D, R, Z, S, V \rangle$ be its underlying SSG, and $x \in LVar$ be a location variable. Then $\Gamma(R|_x) = \{\langle s[x \leftarrow \perp], h \rangle \mid \langle s, h \rangle \in \Gamma(R)\}$.

*Proof* By case splitting, following the cases in the definition. □

Given a set $S$ of SGRs, the emptiness problem $\Gamma(S) = \emptyset$ is effectively decidable if all constraints $\phi$ occurring within elements $\langle G, \phi \rangle \in \mathcal{G}$ are written in a logic decidable for satisfiability. In our case, this logic is the Presburger arithmetic, for which the satisfiability problem is known to be decidable [17].

## 5.3 From Formulae to Sets of SGR

We are now ready to describe the construction of a set of SGRs for a given formula :

$$ \phi : \exists x_1 \dots \exists x_n Q_1 l_1 \dots Q_m l_m \cdot \theta(\mathbf{x}, \mathbf{l}) $$
where $Q_i \in \{\exists_N, \forall_N\}$ and $\theta$ is a quantifier-free QSL formula. The construction is performed incrementally, following the structure of the abstract syntax tree of $\theta$. The set $\mathbf{x} = \{x_1, \dots, x_n\}$ is called the *support set* of $\theta$. Without losing generality, we consider that the leaves of this tree are atomic propositions of one of the forms: $\mathbb{T}$, emp, $x = y$, $x \mapsto y$ and $ls^l(x, y)$, where $x \in \mathbf{x} \cup PVar$ and $y \in \mathbf{x} \cup PVar \cup \{\text{nil}\}$.

From now on, let $S_k(\mathbf{x})$ be the set of all SSGs with at most $k$ root nodes, support variables from $PVar \cup \mathbf{x}$, and counters from a fixed given set $\mathcal{Z}$. Given a formula $\varphi$, we denote by $[[\varphi]]_\mathbf{x}(k)$ the set of SGRs with at most $k$ root nodes, over the support set $\mathbf{x}$, defining the models of $\varphi$.

For atomic spatial propositions, $[[\varphi]]_\mathbf{x}(k)$ is computed according to the definitions from Table 1. In the definition of $[[\text{emp}]]_\mathbf{x}(k)$ we consider as parameter the partition $\langle Y_1, \dots, Y_p \rangle \in \text{Part}(\mathbf{x})$. That is $[[\text{emp}]]_\mathbf{x}(k) = \bigcup_{\langle Y_1, \dots, Y_p \rangle \in \text{Part}(\mathbf{x})} [[\text{emp}]]^{Y_1, \dots, Y_p}$, where $[[\text{emp}]]^{Y_1, \dots, Y_p}$ is defined in Table 1. Intuitively, $Y_i$, $1 \le i \le p$ is the set of variables that are aliased, pointing to the same dangling node $d_i$, in the empty heap. In Table 1, let $D = \{d_1, \dots, d_{p-1}\}$, $R = \emptyset$ and $\Delta = \bigcup_{i=1}^{p-1} \lambda x : Y_i \cdot d_i \cup \lambda x : Y_p \cdot \text{Nil}$.

In the definition of $[[\varphi]]_\mathbf{x}(k)$ for $x \mapsto \text{nil}$ and $x \mapsto y$, we consider two parameters: (1) a set $Z \subseteq \mathbf{x} \cup \{x\}$, such that $x \in Z$, and (2) a partition $\langle Y_1, \dots, Y_p \rangle \in \text{Part}(\mathbf{x} \setminus Z)$. In other words, we have $[[\varphi]]_\mathbf{x}(k) = \bigcup \{[[\varphi]]_Z^{Y_1, \dots, Y_p} \mid Z \subseteq \mathbf{x} \cup \{x\}, x \in Z, \langle Y_1, \dots, Y_p \rangle \in \text{Part}(\mathbf{x} \setminus Z)\}$, where $[[\varphi]]_Z^{Y_1, \dots, Y_p}$ is defined in Table 1. Intuitively, $Z$ corresponds to the set of support variables that are aliased with $x$ in some concrete model.

In the definition of $[[ls^l(x, \text{nil})]]_\mathbf{x}(k)$ we consider an ordered sequence of disjoint subsets of $\mathbf{x}$, namely $Z_1, \dots, Z_k$, where $X_i \subseteq \mathbf{x} \cup \{x\}$, $1 \le k \le n$, such that $x \in Z_1$, and $X_i \cap X_j = \emptyset$, for all $1 \le i < j \le k$. Similarly, in the definition of $[[ls^l(x, y)]]_\mathbf{x}(k)$ we consider sets $Z_1, \dots, Z_k$ where $X_i \subseteq \mathbf{x} \cup \{x, y\}$, $1 \le k \le n$, such that $x \in Z_1$, $y \in Z_k$, and $X_i \cap X_j = \emptyset$, for all $1 \le i < j \le k$. In both cases we consider also a partition $\langle Y_1, \dots, Y_p \rangle \in \text{Part}(\mathbf{x} \setminus (\bigcup_{i=1}^k Z_i))$.

<table><caption>**Table 1** SGR for atomic spatial propositions</caption><thead><tr><th></th><th>[[emp]]<sup>Y<sub>1</sub>...Y<sub>p</sub></sup><br/>[x &mapsto; nil]<sup>Y<sub>1</sub>...Y<sub>p</sub></sup></th><th>[[x &mapsto; y]]<sup>Y<sub>1</sub>...Y<sub>p</sub></sup></th><th>[[ls<sup>l</sup>(x, nil)]<sup>Y<sub>1</sub>...Y<sub>p</sub></sup><br/>Z<sub>1</sub>...Z<sub>k</sub>]</th><th>[[ls<sup>l</sup>(x, y)]<sup>Y<sub>1</sub>...Y<sub>p</sub></sup><br/>Z<sub>1</sub>...Z<sub>k</sub>]</th></tr></thead><tbody><tr><td>N</td><td>D &cup; {Nil}</td><td>D &cup; {n, Nil}</td><td>D &cup; {n, Nil}</td><td>D &cup; {n<sub>1</sub>, ..., n<sub>k</sub>, Nil}</td></tr><tr><td>Z</td><td>&empty;</td><td>{n, z<sub>1</sub>}</td><td>{n, z<sub>1</sub>}</td><td>{n<sub>i</sub>, z<sub>i</sub>}</td></tr><tr><td>S</td><td>&empty;</td><td>{n, Nil}</td><td>{n, d<sub>k</sub>}, if y &in; Y<sub>k</sub></td><td>{n<sub>i</sub>, n<sub>i+1</sub>}</td></tr><tr><td>V</td><td>&Delta;</td><td>&lambda;x : Z.n &cup; &Delta;</td><td>&lambda;x : Z.n &cup; &Delta;</td><td>&cup;<sub>i=1</sub><sup>k</sup> &lambda;x : Z<sub>i</sub>.n<sub>i</sub> &cup; &Delta;</td></tr><tr><td>&phi;</td><td>&top;</td><td>z<sub>1</sub> = 1</td><td>z<sub>1</sub> = 1</td><td>&Sigma;<sub>i=1</sub><sup>k</sup> z<sub>k</sub> = l &and;<br/>(x &in; Z<sub>k</sub> &rarr; l = 0)</td></tr></tbody></table>

As an example, in Figure 6 in Appendix A we show the result of computing $[[ls(u, x_1)]]_{Z_1, \dots, Z_k}$, $1 \le k \le 3$, for $Z_i \subseteq \{u, x_1, x_2\}$, in the following cases: (a) $Z_1 = \{u, x_1\}$, (b) $Z_1 = \{u, x_1, x_2\}$, (c) $Z_1 = \{u\}$, $Z_2 = \{x_1\}$, (d) $Z_1 = \{u, x_2\}$, $Z_2 = \{x_1\}$, (e) $Z_1 = \{u\}$, $Z_2 = \{x_1, x_2\}$, and (f) $Z_1 = \{u\}$, $Z_2 = \{x_2\}$, $Z_3 = \{x_1\}$. The dangling nodes are labeled with D. For simplicity here we avoided showing all combinations resulting from the different partitionings of dangling variables.

The pure formulae $x = \text{nil}$ ($x = y$) correspond to sets of SGRs are the ones in which $x$ points to nil ($y$), and the counters occur unconstrained. Their SGR semantics is defined as
follows:

$$ 
\begin{aligned}
[[x = \text{nil}]_x(k) &= \{ \langle G, \top \rangle \mid G = \langle N, D, R, Z, S, V \rangle \in S_k(\mathbf{x}), V(x) = \text{Nil} \} \\
[[x = y]_x(k) &= \{ \langle G, \top \rangle \mid G = \langle N, D, R, Z, S, V \rangle \in S_k(\mathbf{x}), V(x) = V(y) \}
\end{aligned}
$$

The SGR semantics for the QSL connectives is defined as follows:

$$ 
\begin{aligned}
[[T]]_x(k) &= \{ \langle G, \top \rangle \mid G \in S_k(\mathbf{x}) \} \\
[[\psi_1 \wedge \psi_2]]_x(k) &= [[\psi_1]]_x(k) \sqcap [[\psi_2]]_x(k) \\
[[\neg \psi]]_x(k) &= \{ \langle G, \top \rangle \mid G \in S_k(\mathbf{x}) \} \ominus [[\psi]]_x(k) \\
[[\psi_1 * \psi_2]]_x(k) &= [[\psi_1]]_x(k) \oplus [[\psi_2]]_x(k)
\end{aligned}
$$

If $\pi$ is a purely arithmetic formula, then we have:

$$ [[\psi \wedge \pi]]_x(k) = \{ \langle G, \theta \wedge \pi \rangle \mid \langle G, \theta \rangle \in [[\psi]]_x(k) \} $$

The semantics for the existential quantifiers is as follows:

$$ 
\begin{aligned}
[[\exists x . \psi]]_x(k) &= \{ R \downarrow_x | R \in [[\psi]]_{x \cup \{x\}}(k-1) \}, k \ge 1 \\
[[\exists N l . \psi]]_x(k) &= \{ \langle G, \exists l . \theta \rangle \mid \langle G, \theta \rangle \in [[\psi]]_x(k) \}
\end{aligned}
$$

Let $FV_L(\varphi) = FV(\varphi) \cap LVar$ and $FV_I(\varphi) = FV(\varphi) \cap IVar$ denote the sets of location and integer free variables of $\varphi$, respectively. The following lemma formalizes the correctness of our construction.

**Lemma 7** Given $\varphi$ a QSL formula containing only numeric quantifiers ($\exists_N, \forall_N$), and $\mathbf{x} = \{x_1, \dots, x_n\} \subseteq FV_L(\varphi)$, we have:

$$ \Gamma( [[\exists \mathbf{x} . \varphi]]_{FV_L(\varphi)} \setminus \mathbf{x})(n) = \{ H \mid \exists \mathbf{v} : FV_L(\varphi) \setminus \mathbf{x} \to Loc, \exists \mathbf{t} : FV_I(\varphi) \to \mathbb{N}^+ . \langle H, \mathbf{v}, \mathbf{t} \rangle \models \exists \mathbf{x} . \varphi \} $$

*Proof* Let $L = FV_L(\varphi)$, $I = FV_I(\varphi)$ and $\Gamma_{v,l}(S) = \{ \langle G, \psi \rangle \mid \langle G, \psi \rangle \in S, \mathbf{t} \models \psi \} / \text{in the following. It is enough to prove that, for all } \mathbf{v} : L \to Loc \text{ and } \mathbf{t} : I \to \mathbb{N}^+, \text{ we have:}$

$$ \Gamma_{v,l}([\varphi]_L(0)) = \{ H \mid \langle H, \mathbf{v}, \mathbf{t} \rangle \models \varphi \} \quad (1) $$

For, assuming that (1) is true, we have:

$$ 
\begin{aligned}
\Gamma( [[\exists \mathbf{x} . \varphi]]_{L \setminus \mathbf{x}}(n)) &= \{ R \downarrow_{\mathbf{x}} | R \in [[\varphi]]_L(0) \} \text{ by Lemma 6} \\
&= \bigcup_{R \in [[\varphi]]_L(0)} \{ \langle s[\mathbf{x} \leftarrow \perp], h \rangle \mid \langle s, h \rangle \in \Gamma(R) \} \\
&= \bigcup_{R \in [[\varphi]]_L(0)} \bigcup_{\mathbf{v} : L \to Loc} \{ \langle s[\mathbf{x} \leftarrow \perp], h \rangle \mid \langle s, h \rangle \in \Gamma_{v,l}(R) \} \\
&= \bigcup_{\mathbf{v} : L \to Loc} \{ \langle s[\mathbf{x} \leftarrow \perp], h \rangle \mid \langle s, h \rangle \in \Gamma_{v,l}([\varphi]_L(0)) \} \\
&= \{ \langle s[\mathbf{x} \leftarrow \perp], h \rangle \mid \exists \mathbf{v} : L \to Loc, \exists \mathbf{t} : I \to \mathbb{N}^+ . \langle \langle s[\mathbf{x} \leftarrow \perp], h \rangle, \mathbf{v}, \mathbf{t} \rangle \models \varphi \} \text{ by (1)} \\
&= \{ H \mid \exists \mathbf{v} : L \setminus \mathbf{x} \to Loc, \exists \mathbf{t} : I \to \mathbb{N}^+ . \langle H, \mathbf{v}, \mathbf{t} \rangle \models \exists \mathbf{x} . \varphi \}
\end{aligned}
$$

For the rest of this proof, let us fix $\mathbf{v} : L \to Loc$ and $\mathbf{t} : I \to \mathbb{N}^+$. We prove (1) by induction on the structure of $\varphi$. Before we proceed, for a given valuation $\mathbf{v}$ of location variables, let
$Y_1^v, \dots, Y_p^v$ be the partition of $L$ induced by the following equivalence relation : $x_i \simeq_v x_j$ iff $v(x_i) = v(x_j)$.

For the basic cases we will prove the following statement, equivalent to (1) : for all $H \in \mathcal{H}$, $v : L \to Loc$ and $t : I \to \mathbb{N}^+$ :

$$ \langle H, v, t \rangle \models \varphi \iff \begin{array}{l} \text{exists } \langle G, \psi \rangle \in [[\varphi]]_L(0), \text{ where } G = \langle N, D, R, Z, S, V \rangle \text{ and} \\ \kappa : \mathrm{img}(Z) \to \mathbb{N}^+ \text{ such that } t \cup \kappa \models \psi \text{ and } H \in \Gamma_{v,t \cup \kappa}(G) \end{array} \qquad (2) $$

- $\mathbb{T}$: “⇒” Let $H = \langle s, h \rangle$ be a heap over $PVar$ and $H' = \langle s \cup v, h \rangle$. By definition, $[[\mathbb{T}]]_L(0) = \{\langle G, \top \rangle \mid G \in S_0(L)\}$. Choose $G$ to be the SSG isomorphic to the quotient heap $H'_\sim$ w.r.t $\sim H'$. “<=” Trivial, since always $\langle H, v, t \rangle \models \mathbb{T}$.

- emp : “⇒” Let $H = \langle s, h \rangle$ be a heap such that $dom(h) = \emptyset$ ($H \models \mathrm{emp}$). Let $\{\langle G, \top \rangle\} = [[\mathrm{emp}]_{Y_1^v, \dots, Y_p^v}^{Y_1^v, \dots, Y_p^v}$ (note that $[[\mathrm{emp}]_{Y_1^v, \dots, Y_p^v}$ is a singleton set). Clearly $t \models \top$ and $H \in \Gamma_{v,t}(G)$. “<=” Let $H = \langle s, h \rangle \in \Gamma_{v,t}(G)$, for some SSG $G$ such that $\langle G, \top \rangle \in [[\mathrm{emp}]]_L(0)$. By definition of $[[\mathrm{emp}]]_L(0)$, $dom(h) = \emptyset$, since $G$ has only dangling nodes and the Nil node. Hence $\langle H, v, t \rangle \models \mathrm{emp}$.

- $x \mapsto \mathrm{nil}$ : “⇒” Let $H = \langle s, h \rangle$ be a heap over $PVar$ such that $s(x) = l$ and $h = \{\langle l, \mathrm{nil} \rangle\}$. Let $\{\langle G, z_1 = 1 \rangle\} = [[x \mapsto \mathrm{nil}]_{Y_1^v, \dots, Y_p^v}^{Y_1^v, \dots, Y_p^v}$ and $\kappa = \{\langle z_1, 1 \rangle\}$. Clearly $\kappa \models z_1 = 1$, and $H \in \Gamma_{v,t}(G)$. “<=” Let $\kappa$ be a valuation such that $\kappa(z_1) = 1$, and $H = \langle s, h \rangle \in \Gamma_{v,t \cup \kappa}(G)$, for some SSG $G$ such that $\langle G, z_1 = 1 \rangle \in [[x \mapsto \mathrm{nil}]]_L(0)$. The fact that $s(x) = l$ and $h = \{\langle l, \mathrm{nil} \rangle\}$ for some $l \in Loc$ is now a trivial check.

- $x \mapsto y$ : Similar to the case $x \mapsto \mathrm{nil}$.

- $ls^m(x, \mathrm{nil})$ : “⇒” Let $H = \langle s, h \rangle$ be a heap over $PVar$ such that $s(x) = l_1$ and $h = \{\langle l_i, l_{i+1} \rangle \mid 1 \le i < M\} \cup \{\langle l_M, \mathrm{nil} \rangle\}$, and $t$ be a valuation such that $t(m) = M$. We consider the case $M > 0$, the other case $M = 0$ being left to the reader. Let $H' = \langle s \cup v, h \rangle$, and $H'_\sim$ be the quotient heap w.r.t. $\sim H'$. Let $[l_{i_1}]_\sim, \dots, [l_{i_k}]_\sim, l_{i_k} = \mathrm{nil}$, be the equivalence classes of $\sim H'$, ordered such that $i_1 < \dots < i_k$, and let $Z_1, \dots, Z_k$ be subsets of $\{x_1, \dots, x_n\} \cup \{x\}$ such that $\forall y \in Z_j$ we have $s'_\sim(y) = [l_{i_j}]_\sim$, for all $1 \le j \le k$. Let $\{\langle G, \psi \rangle\} = [[ls^m(x, \mathrm{nil})]_{Z_1, \dots, Z_k}^{Y_1^v, \dots, Y_p^v}$, where $\psi : \sum_{i=1}^k z_i = m$. Notice that $x \notin Z_k$, since $M > 0$. Let $\kappa$ be a valuation of $z_1, \dots, z_k$ such that $\kappa(z_j) = [[l_{i_j}]]$, $1 \le j \le k$. We have $t \cup \kappa \models \psi$ and $H \in \Gamma_{v,t \cup \kappa}(G)$. “<=” Assume that $t(m) > 0$, the case $t(m) = 0$ being left to the reader. Let $\kappa$ be a positive valuation of $z_1, \dots, z_k$ such that $\sum_{i=1}^k \kappa(z_i) = t(m)$ and $H \in \Gamma_{v,t \cup \kappa}(G)$, for some $\langle G, \psi \rangle \in [[ls^m(x, \mathrm{nil})]]_L(0)$. The fact that $\langle H, v, t \rangle \models ls^m(x, \mathrm{nil})$ is a simple check.

- $ls^m(x, y)$ : Similar to the case $ls^m(x, \mathrm{nil})$.

- $x = \mathrm{nil}$ : Let $H = \langle s, h \rangle$ be a heap such that $s(x) = \mathrm{nil}$, and $H' = \langle s \cup v, h \rangle$. By definition, $[[x = \mathrm{nil}]]_L(0) = \{\langle G, \top \rangle \mid G = \langle N, D, R, Z, S, V \rangle \in S_0(L), V(x) = \mathrm{Nil} \}$. Choose $G$ to be the SSG isomorphic to the quotient heap $H'_\sim$ w.r.t $\sim H'$. “<=” Let $G = \langle N, D, R, Z, S, V \rangle$ where $V(x) = \mathrm{Nil}$. For any $v$ and $t$, if $H = \langle s, h \rangle \in \Gamma_{v,t}(G)$, we have $s(x) = \mathrm{nil}$, hence $\langle H, v, t \rangle \models x = \mathrm{nil}$.

- $x = y$ : Similar to the case $x = \mathrm{nil}$.

For the induction steps, we consider the following cases for $\varphi$ :

- $\varphi_1 \wedge \varphi_2$ :

$$ \begin{align*} \Gamma_{v,t}([ [ \varphi_1 \wedge \varphi_2 ] ]_L(0)) &= \Gamma_{v,t}([ [ \varphi_1 ] ]_L(0) \sqcap [ [ \varphi_2 ] ]_L(0)) \\ &= \Gamma_{v,t}([ [ \varphi_1 ] ]_L(0)) \cap \Gamma_{v,t}([ [ \varphi_2 ] ]_L(0)) \text{ by Lemma 4} \\ &= \{ H \mid \langle H, v, t \rangle \models \varphi_1 \} \cap \{ H \mid \langle H, v, t \rangle \models \varphi_2 \} \text{ by induction hypothesis} \\ &= \{ H \mid \langle H, v, t \rangle \models \varphi_1 \wedge \varphi_2 \} \end{align*} $$
¬φ:

$$
\begin{align*}
\Gamma_{v,l}([[\neg\phi]]_L) &= \Gamma_{v,l}(\{\langle G, \top \rangle \mid G \in S_0(L)\} \ominus [[\phi]]_L(0)) \\
&= \Gamma_{v,l}(\{\langle G, \top \rangle \mid G \in S_0(L)\}) \setminus \Gamma_{v,l}([[\phi]]_L(0)) \text{ by Lemma 4} \\
&= \mathcal{H} \setminus \{H \mid \langle H, v, l \rangle \models \phi\} \text{ by induction hypothesis} \\
&= \{H \mid \langle H, v, l \rangle \models \neg\phi\}
\end{align*}
$$

φ₁ * φ₂:

$$
\begin{align*}
\Gamma_{v,l}([[\varphi_1 * \varphi_2]]_L(0)) &= \Gamma_{v,l}([\varphi_1]_L(0) \oplus [\varphi_2]_L(0)) \\
&= \{H_1 \bullet H_2 \mid H_1 \in \Gamma_{v,l}([\varphi_1]_L(0)), H_2 \in \Gamma_{v,l}([\varphi_2]_L(0))\} \text{ by Lemma 5} \\
&= \{H_1 \bullet H_2 \mid \langle H_1, v, l \rangle \models \varphi_1, \langle H_2, v, l \rangle \models \varphi_2\} \text{ by induction hypothesis} \\
&= \{H \mid \langle H, v, l \rangle \models \varphi_1 * \varphi_2\}
\end{align*}
$$

φ ∧ π, where π is a purely arithmetic formula :

Let $S_{v,l} = \{H \mid \langle H, v, l \rangle \models \phi \wedge \pi\}$. We distinguish two cases:

1. If $l \not\models \pi$ then $S_{v,l} = \emptyset$. In this case

$$
\begin{align*}
\Gamma_{v,l}([\phi \wedge \pi]_L) &= \Gamma_{v,l}(\{\langle G, \phi \wedge \pi \rangle \mid \langle G, \psi \rangle \in [\phi]_L(0)\}) \\
&= \bigcup_{\langle G, \psi \rangle \in [\phi]_L(0)} \Gamma_{v,l}(\langle G, \psi \wedge \pi \rangle) = \emptyset
\end{align*}
$$

2. If $l \models \pi$ then

$$
\begin{align*}
S_{v,l} &= \{H \mid \langle H, v, l \rangle \models \phi\} \\
&= \Gamma_{v,l}([\phi]_L(0)) \text{ by induction hypothesis} \\
&= \Gamma_{v,l}([\phi \wedge \pi]_L(0))
\end{align*}
$$

∃Nl. φ:

$$
\begin{align*}
\Gamma_{v,l}([\exists_N l . \phi]_L(0)) &= \Gamma_{v,l}(\{\langle G, \exists l . \psi \rangle \mid \langle G, \psi \rangle \in [[\phi]]_L(0)\}) \\
&= \bigcup_{\langle G, \psi \rangle \in [[\phi]]_L(0)} \Gamma_{v,l}(\langle G, \exists l . \psi \rangle) \\
&= \bigcup_{\langle G, \psi \rangle \in [[\phi]]_L(0)} \Gamma_{v,l}[l \leftarrow n](\langle G, \psi \rangle), \text{ for some } n \in \mathbb{N}^+ \\
&= \Gamma_{v,l}[l \leftarrow n]([\phi]_L(0)) \\
&= \{H \mid \langle H, v, l \mid l \leftarrow n \rangle \models \phi\} \\
&= \{H \mid \langle H, v, l \rangle \models \exists l . \phi\}
\end{align*}
$$

□

As a result, we obtain the decidability of the entailment problem in the $∃^*\{∃_N, ∀_N\}^*$ fragment of QSL.

**Theorem 2** The validity of entailments between formulae in the $∃^*\{∃_N, ∀_N\}^*$ fragment of QSL is a decidable problem.
Proof This proof is a direct consequence of Lemma 7.

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

As an example, in Figure 6 and 7 in Appendix A we detail the SGR construction used to show the validity of the following entailment:

$$[\exists x_{1,2} \exists_N l_{1,2,3} . ls^{l_1}(u, x_1) * ls^{l_2}(x_1, x_2) * ls^{l_3}(x_2, \text{nil}) \wedge ls^{l_1}(u, x_2) * ls^{l_2}(x_2, x_1) * ls^{l_3}(x_1, \text{nil})] \\ \rightarrow [\exists_N l . ls^d(u, \text{nil})]$$

The validity of the entailment is equivalent to the validity of the following Presburger formula:

$$\forall k_3 [\exists l_{1,2,3} . (l_1 = k_3 \wedge l_2 = 0 \wedge l_3 = 0) \lor (l_1 = 0 \wedge l_2 = 0 \wedge l_3 = k_3) \lor \\ (\exists k_{1,2} . k_1 + k_2 = k_3 \wedge l_1 = k_1 \wedge l_2 = 0 \wedge l_3 = k_2)] \rightarrow [\exists l . l = k_3]$$

The various combinations resulting from the different partitionings of dangling variables have been skipped for obvious simplicity reasons.

# 6 Application of the Model Theoretic Method for QSL

The translation between QSL formulae with quantifier prefix of the form $∃^*\{∃_N, ∀_N\}^*$ and sets of SGRs gives a method for deciding the validity of entailments in this logic. Moreover, there is another, more practical advantage to this approach, that gives us a effective method for the verification of both shape and numeric properties of programs with lists.

The L2CA tool [3] is a tool for verifying safety and termination properties of programs with singly-linked lists, based on the translation of programs into counter automata [9]. A counter automaton generated by L2CA has control states of the form $\langle l, G \rangle$, where $l$ is a control label of the original program, and $G$ is a SSG over the set $PVar$ of pointer variables of the input program. By Lemma 2, the set of control states of a counter automaton generated by L2CA is finite, which guarantees that each program with lists will be translated into a finite-control counter automaton. The semantics (set of runs) of the counter automaton generated by L2CA is in a bisimulation relation with the semantics of the original program, therefore all results of the analysis of the counter automaton (e.g. safety properties, termination) carry over to the original program.

The fact that any $∃^*\{∃_N, ∀_N\}^*$ QSL formula $\varphi$ corresponds to a set $[[\varphi]]$ of pairs $\langle G, \psi \rangle$, where $G$ is an SSG and $\psi$ is a Presburger constraint, allows us to extend the L2CA tool to check total correctness of Hoare triples in which the pre- and post-conditions are expressed as $∃^*\{∃_N, ∀_N\}^*$ QSL formulae. Suppose that $\{\varphi\} \mathbf{P} \{\psi\}$ is such a triple. Then for each SGR $\langle G_k, \phi_k \rangle \in [[\varphi]]$ the L2CA tool will generate a counter automaton $A_k$ with initial state $\langle l_0, G_k \rangle$, where $l_0$ is the initial control label of the program $\mathbf{P}$. This automaton corresponds to the semantics of $\mathbf{P}$ when started in an initial control state $\langle l_0, H_0 \rangle$, where $H_0 \in \Gamma(\langle G_k, \phi_k \rangle)$. Let $A$ be the union of all such $A_k$.

By using a combination of existing tools for the analysis of counter automata, e.g. [6, 2, 1] we can verify whether $A$, started in each control state $\langle l_0, G_k \rangle$ with values of counters satisfying the Presburger constraint $\phi_k$, reaches a final control state $\langle l_f, G_f \rangle$ with the counters satisfying some Presburger constraint $\phi^1$ such that $|\varphi \rightarrow \phi'|$, for some $\langle G_f, \phi' \rangle \in [[\psi]]$. This suffices for checking partial correctness. On what concerns total correctness, we use a termination analysis tool for counter automata, e.g. [1], to check whether $\mathbf{P}$, started with any heap $H_0$ such that $H_0 = \varphi$, terminates.

<footnote n="1">¹ In general this is an over-approximation of the set of reachable configurations, obtained using a combination of precise (acceleration) and abstract (widening) methods.</footnote>
## 6.1 Experimental Results

Table 2 presents some experimental results of verifying Hoare triples of the form {$\varphi$} **P** {$\psi$}, where $\varphi$ and $\psi$ are **QSL** formulae, and **P** is a program handling lists. The ListReversal example receives in input a non-circular list pointed to by $u$ of length $l$ and returns a non-circular list pointed to by $v$ containing the cells of the first list in reversed order. The BubbleSort and InsertSort programs are classical sorting algorithms for which we verified that the length of the input list stays the same. The ListCounter example is a simple loop traversing a list pointed to by $u$, while incrementing an integer counter $c$. InsertDelete is the example from Figure 2.

<table><caption>**Table 2** Experimental Results using the L2CA and ASPIC tools</caption><thead><tr><th>{φ}</th><th>P</th><th>{ψ}</th><th>Size</th><th>Gen (s)</th><th>Verif (s)</th><th>Tool</th><th>Result</th></tr></thead><tbody><tr><td>{ls'(u, nil)}</td><td>ListReversal</td><td>{ls'(v, nil)}</td><td>25</td><td>0.4</td><td>0.1</td><td>Aspic</td><td>ok</td></tr><tr><td>{ls'(u, nil)}</td><td>BubbleSort</td><td>{ls'(u, nil)}</td><td>500</td><td>0.4</td><td>0.9</td><td>Aspic</td><td>ok</td></tr><tr><td>{ls'(u, nil)}</td><td>InsertSort</td><td>{ls'(u, nil)}</td><td>880</td><td>0.6</td><td>2</td><td>Aspic</td><td>?</td></tr><tr><td>{ls'(u, nil) ∧ c = 0}</td><td>ListCounter</td><td>{ls'(u, nil) ∧ c = l}</td><td>16</td><td>0.2</td><td>0.1</td><td>Aspic</td><td>ok</td></tr><tr><td>{c = 0 ∧ emp ∧ u = nil}</td><td>InsertDelete</td><td>{c = 0 ∧ emp}</td><td>6</td><td>1.5</td><td>0.5</td><td>Fast</td><td>ok</td></tr></tbody></table>

For all examples, the size (number of control locations) of the automata generated by L2CA is given in the second (Size) column, the time needed for generation in the third (Gen) column, and the time needed to verify partial correctness of the model is given in the fourth (Verif) column. Finally the tool used (either Aspic [2] or Fast [6]) is given in the fifth column.

## 7 Conclusions

We have developed an extension of Separation Logic interpreted over singly-linked heaps, that allows to specify properties related to the sizes of the lists. This logic is especially useful for reasoning about programs that combine dynamically allocated data with variables ranging over integer domains.

The decidability of the extended logic is studied, the full quantifier fragment being shown to be undecidable, by a reduction from the halting problem for 2 counter machines. However the validity of entailments in the $∃^*\{∃_N, ∀_N\}^*$ fragment of the logic is decidable, which allows the use this fragment to specify Hoare triples for programs with lists. The verification of total correctness properties specified in this way was made possible by an extension of the L2CA tool.

## References

1. ARMC. http://www.mpi-sb.mpg.de/~rybal/armc/.

2. ASPIC. http://www-verimag.imag.fr/~gonnord/aspic/aspic.html.

3. L2CA. http://www-verimag.imag.fr/~async/L2CA/l2ca.html.

4. Smallfoot. http://www.dcs.qmul.ac.uk/research/logic/theory/projects/smallfoot/index.html.

5. A. Annichini, A. Bouajjani, and M. Sighireanu. Trex: A tool for reachability analysis of complex systems. In Proc.CAV, volume 2102 of LNCS, pages 368 – 372. Springer, 2001.
6. S. Bardin, A. Finkel, J. Leroux, and L. Petrucci. Fast: Fast accelereation of symbolic transition systems. In Proc. TACAS, volume 2725 of LNCS. Springer, 2004.

7. M. Benedikt, T. Reps, and M. Sagiv. A decidable logic for describing linked data structures. In Springer Verlag, editor, Proc. European Symposium On Programming. LNCS, 1999.

8. J. Berdine, C. Calcagno, and P. O'Hearn. A Decidable Fragment of Separation Logic. In FSTTCS, volume 3328 of LNCS, 2004.

9. A. Bouajjani, M. Bozga, P. Habermehl, R. Iosif, P. Moro, and T. Vojnar. Programs with lists are counter automata. In Springer Verlag, editor, Proc. Computer Aided Verification (CAV). LNCS, 2006.

10. R. M. Burstall. Some techniques for proving correctness of programs which alter data structures. Machine Intelligence, 7:23–50, 1972.

11. N. Immerman, A. Rabinovich, T. Reps, M. Sagiv, and G. Yorsh. Verification via Structure Simulation. In CAV, volume 3114 of LNCS, 2004.

12. S. Ishtiaq and P. O'Hearn. BI as an assertion language for mutable data structures. In POPL, 2001.

13. F. Klaedtke and H. Ruess. Monadic second-order logics with cardinalities. In Proc. 30th International Colloquium on Automata, Languages and Programming. LNCS, 2003.

14. S. Magill, J. Berdine, E. Clarke, and B. Cook. Arithmetic Strengthening for Shape Analysis. In SAS, volume 4634 of LNCS, 2007.

15. M. Minsky. Computation: Finite and Infinite Machines. Prentice-Hall, 1967.

16. P. O'Hearn, C. Calcagno, and H. Yang. Computability and Complexity Results for a Spatial Assertion Language for Data Structures. In FSTTCS, volume 2245 of LNCS, 2001.

17. M. Presburger. Über die Vollständigkeit eines gewissen Systems der Arithmetik. Comptes rendus du I Congrès des Pays Slaves, Warsaw 1929.

18. J. C. Reynolds. Separation logic: A logic for shared mutable data structures. In Springer Verlag, editor, Proc. 17th IEEE Symposium on Logic in Computer Science. LNCS, 2002.

19. P. Wolper and B. Boigelot. Verifying systems with infinite but regular state spaces. In Proc. CAV, volume 1427 of LNCS, pages 88–97. Springer, 1998.

20. G. Yorsh, A. Rabinovich, M. Sagiv, A. Meyer, and A. Bouajjani. A logic of reachable patterns in linked data-structures. In Proc. Foundations of Software Science and Computation Structures. LNCS, 2006.

## A Deciding Validity of an Entailment

$$ \begin{array}{l} [\exists x_{1,2} \exists \mathbb{N} l_{1,2,3} \cdot ls^l(u, x_1) * ls^l(x_1, x_2) * ls^l(x_2, \text{nil}) \land ls^l(u, x_2) * ls^l(x_2, x_1) * ls^l(x_1, \text{nil})] \\ \rightarrow [\exists \mathbb{N} l \cdot ls^l(u, \text{nil})] \end{array} $$

The validity of the entailment is equivalent to the validity of the following Presburger formula:

$$ \forall k_3 [\exists l_{1,2,3} \cdot (l_1 = k_3 \land l_2 = 0 \land l_3 = 0) \lor (l_1 = 0 \land l_2 = 0 \land l_3 = k_3) \lor \\ (\exists k_{1,2} \cdot k_1 + k_2 = k_3 \land l_1 = k_1 \land l_2 = 0 \land l_3 = k_2)] \rightarrow [\exists l \cdot l = k_3] $$
<figure><img src="image_7.png" /><figcaption>Fig. 6 Solving entailment validity with SGRs (1/2)</figcaption></figure>
$$[[Is^1(u, x_1) * Is^2(x_1, x_2) * Is^3(x_2, nil)] \{x_1, x_2\}$$

$$u, x_1, x_2$$
$$\boxed{\text{Nil}}$$

$$l_1 = 0 \wedge l_2 = 0 \wedge l_3 = 0$$

$$u, x_1$$
$$\boxed{k_1} \rightarrow \boxed{x_2}$$
$$\boxed{\text{Nil}}$$

$$l_1 = 0 \wedge l_2 = k_1 \wedge l_3 = 0$$

$$u, x_1, x_2$$
$$\boxed{k_1} \rightarrow \boxed{x_1, x_2}$$
$$\boxed{\text{Nil}}$$

$$l_1 = k_1 \wedge l_2 = 0 \wedge l_3 = 0$$

$$u, x_1, x_2$$
$$\boxed{k_1} \rightarrow \boxed{x_1, x_2}$$
$$\boxed{\text{Nil}}$$

$$l_1 = 0 \wedge l_2 = 0 \wedge l_3 = k_1$$

$$u, x_1$$
$$\boxed{k_1} \rightarrow \boxed{x_1}$$
$$\boxed{k_2} \rightarrow \boxed{x_2}$$
$$\boxed{\text{Nil}}$$

$$l_1 = k_1 \wedge l_2 = k_2 \wedge l_3 = 0$$

$$u, x_1$$
$$\boxed{k_1} \rightarrow \boxed{x_1, x_2}$$
$$\boxed{k_2} \rightarrow \boxed{x_2}$$
$$\boxed{\text{Nil}}$$

$$l_1 = k_1 \wedge l_2 = 0 \wedge l_3 = k_2$$

$$u, x_1$$
$$\boxed{k_1} \rightarrow \boxed{x_1}$$
$$\boxed{k_2} \rightarrow \boxed{x_2}$$
$$\boxed{\text{Nil}}$$

$$l_1 = 0 \wedge l_2 = k_1 \wedge l_3 = k_2$$

$$[[Is^1(u, x_1) * Is^2(x_1, x_2) * Is^3(x_2, nil) \wedge Is^1(u, x_2) * Is^2(x_2, x_1) * Is^3(x_1, nil)] \{x_1, x_2\}$$

$$u, x_1, x_2$$
$$\boxed{\text{Nil}}$$

$$l_1 = 0 \wedge l_2 = 0 \wedge l_3 = 0$$

$$u, x_1$$
$$\boxed{k_1} \rightarrow \boxed{x_1, x_2}$$
$$\boxed{\text{Nil}}$$

$$l_1 = k_1 \wedge l_2 = 0 \wedge l_3 = 0$$

$$u, x_1, x_2$$
$$\boxed{k_1} \rightarrow \boxed{x_1}$$
$$\boxed{\text{Nil}}$$

$$l_1 = 0 \wedge l_2 = 0 \wedge l_3 = k_1$$

$$u, x_1$$
$$\boxed{k_1} \rightarrow \boxed{x_1, x_2}$$
$$\boxed{\text{Nil}}$$

$$l_1 = k_1 \wedge l_2 = 0 \wedge l_3 = k_2$$

$$[[\exists x_1, x_2 . Is^1(u, x_1) * Is^2(x_1, x_2) * Is^3(x_2, nil) \wedge Is^1(u, x_2) * Is^2(x_2, x_1) * Is^3(x_1, nil)] \{x_1, x_2\}$$

$$u, x_1$$
$$\boxed{\text{Nil}}$$

$$l_1 = 0 \wedge l_2 = 0 \wedge l_3 = 0$$

$$u, x_1$$
$$\boxed{k_1} \rightarrow \boxed{x_1}$$
$$\boxed{\text{Nil}}$$

$$l_1 = k_1 \wedge l_2 = 0 \wedge l_3 = 0 \lor$$

$$l_1 = 0 \wedge l_2 = 0 \wedge l_3 = k_1 \lor$$

$$\exists k_1, k_2 . k_1 + k_2 = k_3 \wedge l_1 = k_1 \wedge l_2 = 0 \wedge l_3 = k_2$$

$$[[Is^1(u, nil)]$$

$$u, x_1$$
$$\boxed{\text{Nil}}$$

$$l = 0$$

$$u, x_1$$
$$\boxed{k_1} \rightarrow \boxed{x_1}$$
$$\boxed{\text{Nil}}$$

$$l = k_3$$

<caption>Fig. 7 Solving entailment validity with SGRs (2/2)</caption>