Andrew Reynolds

Radu Iosif

Cristina Serban

Reasoning in the Bernays-Schönfinkel-Ramsey Fragment of Separation Logic

. However, SL becomes undecidable when the quantifier prefix belongs to ∃ * ∀ * ∃ * instead, or when the memory locations are interpreted as integers with linear arithmetic constraints, thus setting a sharp boundary for decidability within SL. We have implemented a decision procedure for the decidable fragment of ∃ * ∀ * SL as a specialized solver inside a DPLL(T ) architecture, within the CVC4 SMT solver. The evaluation of our implementation was carried out using two sets of verification conditions, produced by (i) unfolding inductive predicates, and (ii) a weakest precondition-based verification condition generator. Experimental data shows that automated quantifier instantiation has little overhead, compared to manual model-based instantiation.

Introduction

Separation Logic (SL) is a popular logical framework for program verification, used by a large number of methods, ranging from static analysis [START_REF] Dudka | Predator: A practical tool for checking manipulation of dynamic data structures using separation logic[END_REF][START_REF] Toubhans | An Abstract Domain Combinator for Separately Conjoining Memory Abstractions[END_REF][START_REF] Calcagno | Infer: An automatic program verifier for memory safety of c programs[END_REF] to Hoare-style proofs [START_REF] Nguyen | Enhancing program verification with lemmas[END_REF] and property-guided abstraction refinement [START_REF] Albargouthi | Spatial Interpolants[END_REF]. The salient features that make SL particularly attractive for program verification are the ability of defining (i) recursive data structures using small and natural inductive definitions, (ii) weakest pre-and postcondition calculi that capture the semantics of programs with pointers, and (iii) compositional verification methods, based on the principle of local reasoning (analyzing separately pieces of program working on disjoint heaps).

Consider, for instance, the following inductive definitions, describing an acyclic and a possibly cyclic list segment, respectively: ls(x, y) ≡ emp ∧ x = y ∨ x y ∧ ∃z . x → z * ls(z, y) acyclic list segment from x to y ls(x, y) ≡ emp ∧ x = y ∨ ∃u . x → u * ls(u, y) list segment from x to y

Intuitively, an acyclic list segment is either empty, in which case the head and the tail coincide (emp ∧ x = y), or it contains at least one element which is disjoint from the rest of the list segment. We denote by x → z the fact that x is an allocated memory location, which points to z, and by x → z * ls(z, y) the fact that x → z and ls(z, y) hold over disjoint parts of the heap. The constraint x y, in the inductive definition of ls, captures the fact that the tail of the list segment is distinct from every allocated cell in the list segment, which ensures the acyclicity condition. Since this constraint is omitted from the definition of the second (possibly cyclic) list segment ls(x, y), its tail y is allowed to point inside the set of allocated cells. Automated reasoning is the key enabler of push-button program verification. Any procedure that checks the validity of a logical entailment between inductive predicates requires checking the satisfiability of formulae from the base (non-inductive) assertion language, as shown by the example below. Consider a fragment of the inductive proof showing that any acyclic list segment is also a list segment, given below: ls(z, y) ls(z, y)

x y ∧ x → z * ls(z, y) ∃u . x → u * ls(u, y)

x y ∧ x → z | = ∃u . x → u by instantiation u ← z ls(x, y) ls(x, y)

The first (bottom) inference in the proof corresponds to one of the two cases produced by unfolding both the antecedent and consequent of the entailment (the second case emp ∧ x = y emp ∧ x = y is trivial and omitted for clarity). The second inference is a simplification of the sequent obtained by unfolding, to a sequent matching the initial one (by renaming z to x), and allows to conclude this branch of the proof by an inductive argument, based on the principle of infinite descent [START_REF] Brotherston | Sequent calculi for induction and infinite descent[END_REF].

The simplification applied by the second inference above relies on the validity of the entailment x y ∧ x → z | = ∃u . x → u, which reduces to the (un)satisfiability of the formula x y ∧ x → z ∧ ∀u . ¬x → u. The latter falls into the Bernays-Schönfinkel-Ramsey fragment, defined by the ∃ * ∀ * quantifier prefix, and can be proved unsatisfiable using the instantiation of the universally quantified variable u with the existentially quantified variable z (or a corresponding Skolem constant). In other words, this formula is unsatisfiable because the universal quantified subformula asks that no memory location is pointed to by x, which is contradicted by x → z. The instantiation of u that violates the universal condition is u ← z, which is carried over in the rest of the proof.

The goal of this paper is mechanizing satisfiability of the Bernays-Schönfinkel-Ramsey fragment of SL, without inductively defined predicates 3 . This fragment is defined by the quantifier prefix of the formulae in prenex normal form. We consider formulae ∃x 1 . . . ∃x m ∀y 1 . . . ∀y n . φ(x 1 , . . . , x m , y 1 , . . . , y n ), where φ is any quantifier-free formula of SL, consisting of pure formulae from given base theory T , and points-to atomic propositions relating terms of T , combined with unrestricted Boolean and separation connectives, and the quantified variables range essentially over the set of memory locations. In a nutshell, the contributions of the paper are two-fold:

1. We draw a sharp boundary between decidability and undecidability, proving essentially that the satisfiability problem for the Bernays-Schönfinkel-Ramsey fragment of SL is PSPACE-complete, if the domain of memory locations is an uninterpreted set, whereas interpreting memory locations as integers with linear arithmetic constraints, leads to undecidability. Moreover, undecidability occurs even for uninterpreted memory locations, if we extend the quantifier prefix to ∃ * ∀ * ∃ * . 2. We have implemented an effective decision procedure for quantifier instantiation, based on counterexample-driven learning of conflict lemmas, integrated within the DPLL(T ) architecture [START_REF] Ganzinger | Dpll (t): Fast decision procedures[END_REF] of the CVC4 SMT solver [START_REF] Barrett | CVC4. In: Computer Aided Verification (CAV)[END_REF]. Experimental evaluation of our implementation shows that the overhead of the push-button quantifier instantiation is negligible, compared to the time required to solve a quantifier-free instance of the problem, obtained manually, by model inspection.

Related Work

The first theoretical results on the decidability and computational complexity of SL (without inductive definitions) were found by Calcagno, Yang and O'Hearn [START_REF] Calcagno | Computability and complexity results for a spatial assertion language for data structures[END_REF]. They showed that the satisfiability problem for SL is undecidable, in the presence of quantifiers, assuming that each memory location can point to two other locations, i.e. using atomic propositions of the form x → (y, z). Decidability can be recovered by considering the quantifier-free fragment, proved to be PSPACE-complete, by a small model argument [START_REF] Calcagno | Computability and complexity results for a spatial assertion language for data structures[END_REF]. Refinements of these results consider decidable fragments of SL with one record field (atomic points-to propositions x → y), and one or two quantified variables. In a nutshell, SL with one record field and separating conjunction only is decidable with non-elementary time complexity, whereas adding the magic wand adjoint leads to undecidability [START_REF] Brochenin | On the almighty wand[END_REF]. Decidability, in the presence of the magic wand operator, is recovered by restricting the number of quantifiers to one, in which case the logic becomes PSPACE-complete [START_REF] Demri | Separation logic with one quantified variable[END_REF]. This bound is sharp, because allowing two quantified variables leads to undecidability, and decidability with non-elementary time complexity if the magic wand is removed [START_REF] Demri | Two-variable separation logic and its inner circle[END_REF].

SMT techniques were applied to deciding the satisfiability of SL in the work of Piskac, Wies and Zufferey [START_REF] Piskac | Automating separation logic using smt[END_REF][START_REF] Piskac | Automating separation logic with trees and data[END_REF]. They considered quantifier-free fragments of SL with separating conjunction in positive form (not occurring under negation) and without magic wand, and allowed for hardcoded inductive predicates (list and tree segments). In a similar spirit, we previously defined a translation to multi-sorted second-order logic combined with counterexample-driven instantiation for set quantifiers to define a decision procedure for the quantifier-free fragment of SL [START_REF] Reynolds | A decision procedure for separation logic in SMT[END_REF]. In a different vein, a tableaubased semi-decision procedure is given by Méry and Galmiche [START_REF] Galmiche | Tableaux and resource graphs for separation logic[END_REF]. Termination of this procedure is guaranteed for the (decidable) quantifier-free fragment of SL, yet no implementation is available for comparison.

A number of automated theorem provers have efficient and complete approaches for the Bernays-Schönfinkel-Ramsey fragment of first-order-logic, also known as effectively propositional logic (EPR) [START_REF] Baumgartner | Implementing the model evolution calculus[END_REF][START_REF] Korovin | iprover -an instantiation-based theorem prover for first-order logic (system description)[END_REF]. A dedicated approach for EPR in the SMT solver Z3 was developed in [START_REF] Piskac | Deciding effectively propositional logic using DPLL and substitution sets[END_REF]. An approach based on finite model finding is implemented in CVC4 [START_REF] Reynolds | Finite model finding in SMT[END_REF], which is model-complete for EPR. Our approach is based on counterexample-guided quantifier instantiation, which has been used in the context of SMT solving in previous works [START_REF] Ge | Complete instantiation for quantified formulas in satisfiability modulo theories[END_REF][START_REF] Reynolds | Counterexample-guided quantifier instantiation for synthesis in SMT[END_REF].

Preliminaries

We consider formulae in multi-sorted first-order logic. A signature Σ consists of a set Σ s of sort symbols and a set Σ f of (sorted) function symbols f σ 1 •••σ n σ , where n ≥ 0 and σ 1 , . . . , σ n , σ ∈ Σ s . If n = 0, we call f σ a constant symbol. In this paper, we consider signatures Σ containing the Boolean sort, and write and ⊥ for the Boolean constants true and false. For this reason, we do not consider predicate symbols as part of a signature, as predicates are viewed as Boolean functions. Additionally, we assume for any finite sequence of sorts σ 1 , . . . , σ n ∈ Σ s , the tuple sort σ 1 × . . . × σ n also belongs to Σ s , and that Σ f includes the i th tuple projection function for each i = 1, . . . , n. For each k > 0, let σ k denote the k-tuple sort σ × . . . × σ.

Let Vars be a countable set of first-order variables, each x σ ∈ Vars having an associated sort σ. First-order terms and formulae over the signature Σ (called Σ-terms and Σ-formulae) are defined as usual. For a Σ-formula ϕ, we denote by Fvc(ϕ) the set of free variables and constant symbols in ϕ, and by writing ϕ(x) we mean that x ∈ Fvc(φ). Whenever Fvc(φ) ∩ Vars = ∅, we say that φ is a sentence, i.e. φ has no free variables. A Σ-interpretation I maps: (1) each sort symbol σ ∈ Σ to a non-empty set σ I , (2) each function symbol f σ 1 ,...,σ n ,σ ∈ Σ to a total function f I : σ I 1 × . . . × σ I n → σ I where n > 0, and to an element of σ I when n = 0, and (3) each variable x σ ∈ Vars to an element of σ I . For an interpretation I a sort symbol σ and a variable x, we denote by I[σ ← S ] and, respectively I[x ← v], the interpretation associating the set S to σ, respectively the value v to x, and which behaves like I in all other cases 4 . For a Σ-term t, we write t I to denote the interpretation of t in I, defined inductively, as usual. A satisfiability relation between Σ-interpretations and Σ-formulas, written I | = ϕ, is also defined inductively, as usual. We say that I is a model of ϕ if I satisfies ϕ.

A (multi-sorted first-order) theory is a pair T = (Σ, I) where Σ is a signature and I is a non-empty set of Σ-interpretations, the models of T . We assume that Σ always contains the equality predicate, which we denote by ≈, as well as projection functions for each tuple sort. A Σ-formula ϕ is T -satisfiable if it is satisfied by some interpretation in I. We write E to denote the empty theory (with equality), whose signature consists of a sort U with no additional function symbols, and LIA to denote the theory of linear integer arithmetic, whose signature consists of the sort Int, the binary predicate symbol ≥, function + denoting addition, and the constants 0, 1 of sort Int, interpreted as usual. In particular, there are no uninterpreted function symbols in LIA. By ELIA we denote the theory obtained by extending the signature of LIA with the sort U of E and the equality over U.

Let T = (Σ, I) be a theory and let Loc and Data be two sorts from Σ, with no restriction other than the fact that Loc is always interpreted as a countable set. Also, we consider that Σ has a designated constant symbol nil Loc . The Separation Logic fragment SL(T ) Loc,Data is the set of formulae generated by the following syntax:

ϕ := φ | emp | t → u | ϕ 1 * ϕ 2 | ϕ 1 - - * ϕ 2 | ¬ϕ 1 | ϕ 1 ∧ ϕ 2 | ∃x σ . ϕ 1 (x)
where φ is a Σ-formula, and t, u are Σ-terms of sorts Loc and Data, respectively. As usual, we write ∀x σ . ϕ(x) for ¬∃x σ . ¬ϕ(x). We omit specifying the sorts of variables and constants when they are clear from the context. 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 1 and h 2 , we write h 1 #h 2 for dom(h 1 ) ∩ dom(h 2 ) = ∅ and h = h 1 h 2 for h 1 #h 2 and h = h 1 ∪ h 2 . We define the satisfaction relation I, h | = SL φ inductively, as follows:

I, h | = SL φ ⇐⇒ I | = φ if φ is a Σ-formula I, h | = SL emp ⇐⇒ h = ∅ I, h | = SL t → u ⇐⇒ h = {(t I , u I )} and t I ≈ nil I I, h | = SL φ 1 * φ 2 ⇐⇒ there exist heaps h 1 , h 2 s.t. h = h 1 h 2 and I, h i | = SL φ i , i = 1, 2 I, h | = SL φ 1 - - * φ 2 ⇐⇒ for all heaps h if h #h and I, h | = SL φ 1 then I, h h | = SL φ 2 I, h | = SL ∃x S .ϕ(x) ⇐⇒ I[x ← s], h | = SL ϕ(x), for some s ∈ S I
The satisfaction relation for Σ-formulae, Boolean connectives ∧, ¬, and linear arithmetic atoms, are the classical ones from first-order logic. Notice that the range of a quantified variable x S is the interpretation of its associated sort S I .

A formula ϕ is said to be satisfiable if there exists an interpretation I and a heap h such that I, h | = SL ϕ. The (SL, T )-satisfiability problem asks, given an SL formula ϕ, whether there exists an interpretation I of T and a heap h such that I, h | = SL ϕ. We write ϕ | = SL ψ if for every interpretation I and heap h, if I, h | = SL ϕ then I, h | = SL ψ, and we say that ϕ entails ψ in this case.

The Bernays-Schönfinkel-Ramsey Fragment of SL In this paper we address the satisfiability problem for the class of sentences φ ≡ ∃x 1 . . . ∃x m ∀y 1 . . . ∀y n . ϕ(x 1 , . . . , x m , y 1 , . . . , y n ), where ϕ is a quantifier-free formula of SL(T ) Loc,Data . We shall denote this fragment by ∃ * ∀ * SL(T ) Loc,Data . It is easy to see that any sentence φ, as above, is satisfiable if and only if the sentence ∀y 1 . . . ∀y n . ϕ[c 1 /x 1 , . . . , c m /x m ] is satisfiable, where c 1 , . . . , c m are fresh (Skolem) constant symbols. The latter is called the functional form of φ.

As previously mentioned, SL is used mainly specify properties of a program's heap. If the program under consideration uses pointer arithmetic, as in C or C++, it is useful to consider LIA for the theory of memory addresses. Otherwise, if the program only compares the values of the pointers for equality, as in Java, one can use E for this purpose. This distinction led us to considering the satisfiability problem for ∃ * ∀ * SL(T ) Loc,Data in the following cases:

1. Loc is interpreted as the sort U of E and Data as U k , for some k ≥ 1. The satisfiability problem for the fragment ∃ * ∀ * SL(E) U,U k is PSPACE-complete, and the proof follows a small model property argument. 2. as above, with the further constraint that U is interpreted as an infinite countable set, i.e. of cardinality ℵ 0 . In this case, we prove a cut-off property stating that all locations not in the domain of the heap and not used in the interpretation of constants, are equivalent from the point of view of an SL formula. This satisfiability problem is reduced to the unconstrained one above, and also found to be PSPACE-complete. 3. both Loc and Data are interpreted as Int, equipped with addition and total order, in which case ∃ * ∀ * SL(LIA) Int,Int is undecidable.

4.

Loc is interpreted as the sort U of E, and Data as U ×Int. Then ∃ * ∀ * SL(ELIA) U,U×Int is undecidable. Additionally, we prove that the fragment ∃ * ∀ * ∃ * SL(E) U,U k , with two quantifier alternations, is undecidable, if k ≥ 2. The question whether the fragment ∃ * ∀ * SL(ELIA) U,Int is decidable is currently open, and considered for future work.

For space reasons, all missing proofs are given in [START_REF] Reynolds | Reasoning in the bernays-schoenfinkel-ramsey fragment of separation logic[END_REF].

Decidability and Complexity Results

This section defines the decidable cases of the Bernays-Schönfinkel-Ramsey fragment of SL, with matching undecidable extensions. The decidable fragment ∃ * ∀ * SL(E) U,U k relies on a small model property given in Section 3.1. Undecidability of ∃ * ∀ * SL(LIA) Int,Int is obtained by a refinement of the undecidability proof for Presburger arithmetic with one monadic predicate [START_REF] Halpern | Presburger arithmetic with unary predicates is π 1 1 complete[END_REF], in Section 3.4.

Small Model Property

The decidability proof for the quantifier-free fragment of SL [START_REF] Calcagno | Computability and complexity results for a spatial assertion language for data structures[END_REF][START_REF] Yang | Local Reasoning for Stateful Programs[END_REF] relies on a small model property. Intuitively, no quantifier-free SL formula can distinguish between heaps in which the number of invisible locations, not in the range of the set of free variables, exceeds a certain threshold, linear in the size of the formula. Then a formula is satisfiable iff it has a heap model of size linear in the size of the input formula.

For reasons of self-containment, we recall a number of definitions and results from [START_REF] Yang | Local Reasoning for Stateful Programs[END_REF]. Some of them are slightly modified for our purposes, but these changes have no effect on the validity of the original proofs for the Lemmas 1 and 2 below. In the rest of this section, we consider formulae of SL(E) U,U k , meaning that (i) Loc = U, and (ii) there exists an integer k > 0 such that Data = U k , where U is the (uninterpreted) sort of E. We fix k for the rest of this section. Definition 1. [30, Definition 90] Given a set of locations S , the equivalence relation = S between k-tuples of locations is defined as v 1 , . . . , v k = S v 1 , . . . , v k if and only if if v i ∈ S then v i = v i , and if v i S then v i S , for all i = 1, . . . , k.

Intuitively, = S restricts the equality to the elements in S . Observe that = S is an equivalence relation and that S ⊆ T implies = T ⊆ = S . For a set S , we write | |S | | for its cardinality, in the following. Definition 2. [30, Definition 91] Given an interpretation I, an integer n > 0, a set of variables X ⊆ Vars and a set of locations S ⊆ U I , for any two heaps h, h :

U I fin (U I ) k , we define h ∼ I n,X,S h if and only if 1. I(X) ∩ dom(h) = I(X) ∩ dom(h ), 2. for all ∈ I(X) ∩ dom(h), we have h( ) = I(X)∪S h ( ), 3. if | |dom(h) \ I(X)| | < n then | |dom(h) \ I(X)| | = | |dom(h ) \ I(X)| |, 4. if | |dom(h) \ I(X)| | ≥ n then | |dom(h ) \ I(X)| | ≥ n.
Observe that, for any n ≤ m and S ⊆ T we have ∼ I m,X,T ⊆ ∼ I n,X,S . In addition, for any integer k > 0, subset S ⊆ U I and location ∈ U I , we consider the function prun k,S ( 1 , . . . , k ), which replaces each value i S in its argument list by .

. h ∼ I n,X,L h , 2. dom(h ) \ I(X) ⊆ L, 3. for all ∈ dom(h ), we have h ( ) = prun v k,I(X)∪L (h( ))
. Next, we define the following measure on quantifier-free SL formulae:

|φ * ψ| = |φ| + |ψ| |φ - - * ψ| = |ψ| |φ ∧ ψ| = max(|φ|, |ψ|) |¬φ| = |φ| |t → u| = 1 |emp| = 1 |φ| = 0 if φ is a Σ-formula
Intuitively, |ϕ| is the maximum number of invisible locations, that are not in I(Fvc(ϕ)), and which can be distinguished by the quantifier-free SL(E) U,U k formula ϕ. The crux of the PSPACE-completeness proof for quantifier-free SL(E) U,U k is that two heaps equivalent up to |ϕ| invisible locations are also equivalent from the point of view of satisfiability of ϕ, which provides a small model property for this fragment [START_REF] Yang | Local Reasoning for Stateful Programs[END_REF][START_REF] Calcagno | Computability and complexity results for a spatial assertion language for data structures[END_REF].

Lemma 2. [30, Prop. 95] Given a quantifier-free SL(E) U,U k formula ϕ, an interpretation I, and two heaps h and h , if h ∼ I |ϕ|,Fvc(ϕ),∅ h and

I, h | = SL ϕ then I, h | = SL ϕ.
Our aim is to extend this result to ∃ * ∀ * SL(E) U,U k , in the first place. This new small model property is given by the next lemma.

Lemma 3. Let ϕ(x U 1 , . . . , x U n ) be a quantifier-free SL(E) U,U k -formula, and ϕ ∀ ≡ ∀x U 1 . . . ∀x U n . ϕ(x U 1 , . . . , x U n ) be its universal closure. Then ϕ ∀ has a model if and only if there exists an interpretation I and a heap h :

U I fin (U I ) k such that I, h | = SL ϕ ∀ and: 1. | |U I | | ≤ |ϕ| + | |Fvc(ϕ ∀ )| | + n, 2. dom(h) ⊆ L ∪ I(Fvc(ϕ ∀ )), 3. for all ∈ dom(h), we have h( ) ∈ (I(Fvc(ϕ ∀ )) ∪ {nil I } ∪ L ∪ {v}) k , where L ⊆ U I \ I(Fvc(ϕ ∀ )) is a set of locations such that | |L| | = |ϕ| + n and v ∈ U I \ (I(Fvc(ϕ ∀ )) ∪ {nil I } ∪ L) is an arbitrary location.
We are ready to prove two decidability results, based on the above small model property, concerning the cases where (i) Loc is interpreted as a countable set with equality, and (ii) Loc is interpreted as an infinite countable set with no other operators than equality.

Uninterpreted Locations without Cardinality Constraints

In this section, we consider the satisfiability problem for the fragment ∃ * ∀ * SL(E) U,U k , where the location sort U can be interpreted by any (possibly finite) countable set, with no other operations than the equality, and the data sort consists of k-tuples of locations.

Theorem 1. The satisfiability problem for ∃ * ∀ * SL(E) U,U k is PSPACE-complete.

Proof. PSPACE-hardness follows from the fact that satisfiability is PSPACE-complete for quantifier-free SL(E) U,U k [START_REF] Calcagno | Computability and complexity results for a spatial assertion language for data structures[END_REF]. To prove membership in PSPACE, consider the formula φ ≡ ∃x 1 . . . ∃x m ∀y 1 . . . ∀y n . ϕ(x, y), where ϕ is a quantifier-free SL(E) U,U k formula. Let c = c 1 , . . . , c m be a tuple of constant symbols, and φ ≡ ∀y 1 . . . ∀y n . ϕ(c, y) be the functional form of φ, obtained by replacing x i with c i , for all i = 1, . . . , m. By Lemma 3, φ has a model if and only if it has a model I, h such that:

-

| |U I | | ≤ |ϕ| + n + m, -dom(h) ⊆ L ∪ c I , -∀ ∈ dom(h) . h( ) ∈ (I(c) ∪ {nil I } ∪ L ∪ {v}) k , where L ⊆ U I \ I(c), | |L| | = |ϕ| + m and v ∈ U I \ (I(c) ∪ {nil I } ∪ L).
We describe below a nondeterministic polynomial space algorithm that decides satisfiability of φ. First, nondeterministically chose a model I, h that meets the above requirements. Then we check, for each tuple u 1 , . . . ,

u n ∈ (U I ) n that I[y 1 ← u 1 ] . . . [y n ← u n ], h | = SL ϕ.
In order to enumerate all tuples from (U I ) n we need n • log 2 (|ϕ| + n + m) extra bits, and the check for each such tuple can be done in PSPACE, according to [7, §5].

This result is somewhat surprising, because the classical Bernays-Schönfinkel fragment of first-order formulae with predicate symbols (but no function symbols) and quantifier prefix ∃ * ∀ * is known to be NEXPTIME-complete [17, §7]. The explanation lies in the fact that the interpretation of an arbitrary predicate symbol P(x 1 , . . . , x n ) cannot be captured using only points-to atomic propositions, e.g. x 1 → (x 2 , . . . , x n ), between locations and tuples of locations, due to the interpretation of points-to's as heaps 5(finite partial functions).

The following lemma sets a first decidability boundary for SL(E) U,U k , by showing how extending the quantifier prefix to ∃ * ∀ * ∃ * leads to undecidability.

Lemma 4. The satisfiability problem for

∃ * ∀ * ∃ * SL(E) U,U k is undecidable, if k ≥ 2.
Observe that the result of Lemma 4 sets a fairly tight boundary between the decidable and undecidable fragments of SL. On the one hand, simplifying the quantifier prefix to ∃ * ∀ * yields a decidable fragment (Theorem 1), whereas SL(E) U,U (k = 1) without the magic wand (-- * ) is decidable with non-elementary time complexity, even when considering an unrestricted quantifier prefix [START_REF] Brochenin | On the almighty wand[END_REF].

Uninterpreted Locations with Cardinality ℵ 0

We consider the stronger version of the satisfiability problem for ∃ * ∀ * SL(E) U,U k , where U is interpreted as an infinite countable set (of cardinality ℵ 0 ) with no function symbols, other than equality. Instances of this problem occur when, for instance, the location sort is taken to be Int, but no operations are used on integers, except for testing equality.

Observe that this restriction changes the satisfiability status of certain formulae. For instance, ∃x∀y . y ≈ nil ⇒ (y → x * ) is satisfiable if U is interpreted as a finite set, but becomes unsatisfiable when U is infinite. The reason is that this formula requires every location from U I apart from nil to be part of the domain of the heap, which is impossible due the fact that only finite heaps are considered by the semantics of SL.

In the following proof, we use the formula alloc(x) ≡ x → (x, . . . , x) -- * ⊥, expressing the fact that a location variable x is allocated, i.e. its interpretation is part of the heap's domain [START_REF] Brochenin | On the almighty wand[END_REF]. Intuitively, we reduce any instance of the ∃ * ∀ * SL(E) U,U k satisfiability problem, with U of cardinality ℵ 0 , to an instance of the same problem without this restriction, by the following cut-off argument: if a free variable is interpreted as a location which is neither part of the heap's domain, nor equal to the interpretation of some constant, then it is not important which particular location is chosen for that interpretation.

Theorem 2. The satisfiability problem for

∃ * ∀ * SL(E) U,U k is PSPACE-complete if U is required to have cardinality ℵ 0 .
Proof. PSPACE-hardness follows from the PSPACE-completeness of the satisfiability problem for quantifier-free SL, with uninterpreted locations [7, §5.2]. Since the reduction from [7, §5.2] involves no universally quantified variables, the ℵ 0 cardinality constraint has no impact on this result.

Let ∃x 1 . . . ∃x m ∀y 1 . . . ∀y n . ϕ(x, y) be a formula, and ∀y 1 . . . ∀y n . ϕ(c, y) be its functional form, obtained by replacing each x i with c i , for i = 1, . . . , m. We consider the following formulae, parameterized by y i , for i = 1, . . . , n:

ψ 0 (y i ) ≡ alloc(y i ) ψ 1 (y i ) ≡ m j=1 y i = c j ψ 2 (y i ) ≡ y i = d i external ≡ n i=1 (¬alloc(d i ) ∧ m j=1 d i c j )
where {d i | i = 1, . . . , n} is a set of fresh constant symbols. We show the following fact:

I , h | = SL external ∧ ∀y 1 . . . ∀y n t 1 ,...,t n ∈{0,1,2} n n i=1 ψ t i (y i ) ⇒ ϕ(c, y) Ψ t 1 ,.

..,tn

To show membership in PSPACE, consider a nondeterministic algorithm that choses I and h and uses 2n extra bits to check that I , h | = SL extern ∧ ∀y 1 . . . ∀y n . Ψ t 1 ,...,t n separately, for each t 1 , . . . , t n ∈ {0, 1, 2} n . By Lemma 3, the sizes of I and h are bounded by a polynomial in the size of Ψ t 1 ,...,t n , which is polynomial in the size of ϕ, and by Theorem 1, each of these checks can be done in polynomial space.

Integer Locations with Linear Arithmetic

In the rest of this section we show that the Bernays-Schönfinkel-Ramsey fragment of SL becomes undecidable as soon as we use integers to represent the set of locations and combine SL with linear integer arithmetic (LIA). The proof relies on an undecidability argument for a fragment of Presburger arithmetic with one monadic predicate symbol, interpreted over finite sets. Formally, we denote by (∃ * ∀ * ∩ ∀ * ∃ * ) -LIA the set of formulae consisting of a conjunction between two linear arithmetic formulae, one with quantifier prefix in the language ∃ * ∀ * , and another with quantifier prefix ∀ * ∃ * . Theorem 3. The satisfiability problem is undecidable for the fragment (∃ * ∀ * ∩ ∀ * ∃ * ) -LIA, with one monadic predicate symbol, interpreted over finite sets of integers.

Proof. We reduce from the following variant of Hilbert's 10th Problem: given a multivariate Diophantine polynomial R(x 1 , . . . , x n ), the problem "does R(x 1 , . . . , x n ) = 0 have a solution in N n ?" is undecidable [START_REF] Matiyasevich | Enumerable sets are diophantine[END_REF].

By introducing sufficiently many free variables, we encode R(x 1 , . . . , x n ) = 0 as an equisatisfiable Diophantine system of degree at most two, containing only equations of the form x = yz (resp. x = y 2 ) and linear equations k i=1 a i x i = b, where a 1 , . . . , a k , b ∈ Z. Next, we replace each equation of the form x = yz, with y and z distinct variables, with the quadratic system 2x + t y + t z = t y+z ∧ t y = y 2 ∧ t z = z 2 ∧ t y+z = (y + z) 2 , where t y , t z and t y+z are fresh (free) variables. In this way, we replace all multiplications between distinct variables by occurrences of the squaring function. Let Ψ R(x 1 ,...,x n )=0 be the conjunction of the above equations. It is manifest that R(x 1 , . . . , x n ) = 0 has a solution in N n iff Ψ R(x 1 ,...,x n )=0 is satisfiable, with all free variables ranging over N. Now we introduce a monadic predicate symbol P, which is intended to denote a (possibly finite) set of consecutive perfect squares, starting with 0. To capture this definition, we require the following:

P(0) ∧ P(1) ∧ ∀x∀y∀z . P(x) ∧ P(y) ∧ P(z) ∧ x < y < z ∧ (∀u . x < u < y ∨ y < u < z ⇒ ¬P(u)) ⇒ z -y = y -x + 2 (sqr)
Observe that this formula is a weakening of the definition of the infinite set of perfect squares given by Halpern [START_REF] Halpern | Presburger arithmetic with unary predicates is π 1 1 complete[END_REF], from which the conjunct ∀x∃y . y > x ∧ P(y), requiring that P is an infinite set of natural numbers, has been dropped. Moreover, notice that sqr has quantifier prefix ∀ 3 ∃, due to the fact that ∀u occurs implicitly under negation, on the left-hand side of an implication. If P is interpreted as a finite set P I = {p 0 , p 1 , . . . , p N } such that (w.l.o.g.) p 0 < p 1 < . . . < p N , it is easy to show, by induction on N > 0, that p i = i 2 , for all i = 0, 1, . . . , N. The next step is encoding the squaring function using the monadic predicate P. This is done by replacing each atomic proposition x = y 2 in Ψ R(x 1 ,...,x n )=0 by the formula Let Φ R(x 1 ,...,x n )=0 be the conjunction of sqr with the formula obtained by replacing each atomic proposition x = y 2 with θ x=y 2 in Ψ R(x 1 ,...,x n )=0 . Observe that each universally quantified variable in Φ R(x 1 ,...,x n )=0 occurs either in sqr or in some θ x=y 2 , and moreover, each θ x=y 2 belongs to the ∃ * ∀ * fragment of LIA. Φ R(x 1 ,...,x n )=0 belongs thus to the ∃ * ∀ * ∩ ∀ * ∃ * fragment of LIA, with P being the only monadic predicate symbol. Finally, we prove that R(x 1 , . . . , x n ) = 0 has a solution in N n iff Φ R(x 1 ,...,x n )=0 is satisfiable.

θ x=y 2 ≡ P(x) ∧ P(x + 2y + 1) ∧ ∀z . x < z < x + 2y + 1 ⇒ ¬P(z).
"⇒" Let I be a valuation mapping x 1 , . . . , x n into N, such that I | = R(x 1 , . . . , x n ) = 0. Obviously, I can be extended to a model of Ψ R(x 1 ,...,x n )=0 by assigning t I x = (x I ) 2 for all auxiliary variables t x occurring in Ψ R(x 1 ,...,x n )=0 . We extend I to a model of Φ R(x 1 ,...,x n )=0 by assigning

P I = {n 2 | 0 ≤ n ≤ √ m}, where m = max{(x I + 1) 2 | x ∈ Fvc(Ψ R(x 1 ,...,x n )=0
)}. Clearly P I meets the requirements of sqr. By Fact 2, we obtain that

I | = θ x=y 2 for each subformula θ x=y 2 of Φ R(x 1 ,...,x n )=0 , thus I | = Φ R(x 1 ,...,x n )=0 . "⇐" If I | = Ψ R(x 1 ,...,x n )=0
then, by sqr, P I is a set of consecutive perfect squares, and, by Fact 2,

I | = x = y 2 for each subformula θ x=y 2 of Φ R(x 1 ,...,x n )=0 . Then I | = Ψ R(x 1 ,...,x n )=0 and consequently I | = R(x 1 , . . . , x n ) = 0.
We consider now the satisfiability problem for the fragment ∃ * ∀ * SL(LIA) Int,Int where both Loc and Data are taken to be the Int sort, equipped with addition and total order. Observe that, in this case, the heap consists of a set of lists, possibly with aliases and circularities. Without losing generality, we consider that Int is interpreted as the set of positive integers 6 .

The above theorem cannot be directly used for the undecidability of ∃ * ∀ * SL(LIA) Int,Int , by interpreting the (unique) monadic predicate as the (finite) domain of the heap. The problem is with the sqr formula, that defines the interpretation of the monadic predicate as a set of consecutive perfect squares 0, 1, . . . , n 2 , and whose quantifier prefix lies in the ∀ * ∃ * fragment. We overcome this problem by replacing the sqr formula above with a definition of such sets in ∃ * ∀ * SL(LIA) Int,Int . Let us first consider the following properties expressed in SL [START_REF] Brochenin | On the almighty wand[END_REF]:

x ≥ 1 ≡ ∃u . u → x * x ≤ 1 ≡ ∀u∀t . ¬(u → x * t → x * )
Intuitively, x ≥ 1 states that x has at least one predecessor in the heap, whereas x ≤ 1 states that x has at most one predecessor. We use x = 0 and x = 1 as shorthands for ¬( x ≥ 1) and x ≥ 1 ∧ x ≤ 1, respectively. The formula below states that the heap can be decomposed into a list segment starting with x and ending in y, and several disjoint cyclic lists:

x --→ + y ≡ x = 0 ∧ alloc(x) ∧ y = 1 ∧ ¬alloc(y) ∧ ∀z . z ≈ y ⇒ ( z = 1 ⇒ alloc(z)) ∧ ∀z . z ≤ 1
We forbid the existence of circular lists by adding the following arithmetic constraint:

∀u∀t . u → t * ⇒ u < t (nocyc)
We ask, moreover, that the elements of the list segment starting in x are consecutive perfect squares:

consqr(x) ≡ x = 0 ∧ x → 1 * ∧ ∀z∀u∀t . z → u * u → t * ⇒ t -u = u -z + 2 (consqr)
Observe that the formula ∃x∃y . x --→ + y∧nocyc∧consqr(x) belongs to ∃ * ∀ * SL(LIA) Int,Int .

Theorem 4. The satisfiability problem for ∃ * ∀ * SL(LIA) Int,Int is undecidable.

Proof. We use the same reduction as in the proof of Theorem 3, with two differences:

we replace sqr by ∃x∃y . x --→ + y ∧ nocyc ∧ consqr(x), and define θ x=y 2 ≡ alloc(x) ∧ alloc(x + 2y + 1) ∧ ∀z . x < z < x + 2y + 1 ⇒ ¬alloc(z).

It is tempting, at this point to ask whether interpreting locations as integers and considering subsets of LIA instead may help recover the decidability. For instance, it has been found that the Bernays-Schönfinkel-Ramsey class is decidable in presence of integers with difference bounds arithmetic [START_REF] Voigt | Bernays-schönfinkel-ramsey with simple bounds is nexptimecomplete[END_REF], and the same type of question can be asked about the fragment of ∃ * ∀ * SL(LIA) Int,Int , with difference bounds constraints only.

Finally, we consider a variant of the previous undecidability result, in which locations are the (uninterpreted) sort U of E and the data consists of tuples of sort U × Int. This fragment of SL can be used to reason about lists with integer data. The undecidability of this fragment can be proved along the same lines as Theorem 4.

Theorem 5. The satisfiability problem for ∃ * ∀ * SL(ELIA) U,U×Int is undecidable.

4 A Procedure for ∃ * ∀ * Separation Logic in an SMT Solver This section presents a procedure for the satisfiability of ∃ * ∀ * SL(E) U,U k inputs 7 . Our procedure builds upon our previous work [START_REF] Reynolds | A decision procedure for separation logic in SMT[END_REF], which gave a decision procedure for quantifier-free SL(T ) Loc,Data inputs for theories T where the satisfiability problem for quantifier-free T -constraints is decidable. Like existing approaches for quantified formulas in SMT [START_REF] Ge | Complete instantiation for quantified formulas in satisfiability modulo theories[END_REF][START_REF] Reynolds | Counterexample-guided quantifier instantiation for synthesis in SMT[END_REF], our approach is based on incremental quantifier instantiation based on a stream of candidate models returned by a solver for quantifier-free inputs. Our approach for this fragment exploits the small model property given in Lemma 3 to restrict the set of quantifier instantiations it considers to a finite set.

Figure 1 gives a counterexample-guided approach for establishing the satisfiability of input ∃x ∀y ϕ(x, y). We first introduce tuples of fresh constants k and e of the same type as x and y respectively. Our procedure will be based on finding a set of instantiations of ∀y ϕ(k, y) that are either collectively unsatisfiable or are satisfiable and entail our input. Then, we construct a set L which is the union of constants k and a set L of fresh constants whose cardinality is equal to |ϕ(x, y)| (see Section 3.1) plus the number of universal variables n in our input. Conceptually, L is a finite set of terms from which the instantiations of y in ∀y ϕ(k, y) can be built.

After constructing L, we call the recursive subprocedure solve rec on Γ (initially empty) and L. This procedure incrementally adds instances of ∀y ϕ(k, y) to Γ. In step 1, we first check if Γ is (SL, T )-unsatisfiable using the procedure from [START_REF] Reynolds | A decision procedure for separation logic in SMT[END_REF]. If so, our input is (SL, T )-unsatisfiable. Otherwise, in step 2 we consider the miniscoped form of our input ∃x ∀y ϕ 1 (x, y) ∧ . . . ∧ ∀y ϕ p (x, y), that is, where quantification over x is distributed over conjunctions. In the following, we may omit quantification on conjunctions ϕ j that do not contain variables from y. Given this formula, for each j = 1, . . . , p, we check the (SL, T )-satisfiability of set Γ j containing Γ, the negation of ∀y ϕ j (k, y) where y is solve(∃x ∀y ϕ(x, y)) where x = (x 1 , . . . , x m ) and y = (y 1 , . . . , y n ):

Let k = (k 1 , . . . , k m ) and e = (e 1 , . . . , e n ) be fresh constants of the same type as x and y.

Let L = L ∪ {k 1 , . . . , k m } where L is a set of fresh constants s.t. | |L | | = |ϕ(x, y)| + n.
Return solve rec(∃x ∀y ϕ(x, y), ∅, L). solve rec(∃x ∀y ϕ(x, y), Γ, L):

1. If Γ is (SL, E)-unsat, return "unsat". 2. Assume ∃x ∀y ϕ(x, y) is equivalent to ∃x ∀y ϕ 1 (x, y) ∧ . . . ∧ ∀y ϕ p (x, y).

If Γ j = Γ ∪ {¬ϕ j (k, e) ∧ n i=1 t∈L
e i ≈ t} is (SL, E)-unsat for all j = 1, . . . , p, return "sat".

3. Otherwise, let I, h | = SL Γ j for some j ∈ {1, . . . , p}.

Let t = (t 1 , . . . , t n ) be such that e I i = t I i and t i ∈ L for each i = 1, . . . , n. Return solve rec(∃x ∀y ϕ(x, y), Γ ∪ {ϕ j (k, t)}, L). Fig. 1. A counterexample-guided procedure for ∃ * ∀ * SL(E) U,U k formulas ∃x ∀y ϕ(x, y), where U is an uninterpreted sort in the signature of E.

replaced by fresh contants e, and a conjunction of constraints that says each e i must be equal to at least one term in L for i = 1, . . . , n. If Γ j is (SL, T )-unsatisfiable for each j = 1, . . . , p, our input is (SL, T )-satisfiable. Otherwise in step 3, given an interpretation I and heap h satisfying Γ j , we construct a tuple of terms t = (t 1 , . . . , t n ) used for instantiating ∀y ϕ j (k, y). For each i = 1, . . . , n, we choose t i to be a term from L whose interpretation is the same as e i . The existence of such a t i is guaranteed by the fact that I satisfies the constraint from Γ j that tells us e i is equal to at least one such term. This selection ensures that instantiations on each iteration are chosen from a finite set of possibilities and are unique. In practice, the procedure terminates, both for unsatisfiable and satisfiable inputs, before considering all t from L n for each ∀y ϕ j (x, y). Theorem 6. Let U be an uninterpreted sort belonging to the signature of E. For all ∃ * ∀ * SL(E) U,U k formulae ψ of the form ∃x ∀y ϕ(x, y), solve(ψ):

1. Answers "unsat" only if ψ is (SL, E)-unsatisfiable. 2. Answers "sat" only if ψ is (SL, E)-satisfiable.

Terminates.

We discuss a few important details regarding our implementation of the procedure. Matching Heuristics When constructing the terms t for instantiation, it may be the case that e I i = u I for multiple u ∈ L for some i ∈ {1, . . . , n}. In such cases, the procedure will choose one such u for instantiation. To increase the likelihood of the instantiation being relevant to the satisfiability of our input, we use heuristics for selecting the best possible u among those whose interpretation is equal to e i in I. In particular, if e I i = u I 1 = u I 2 , and Γ contains predicates of the form e i → v and u 1 → v 1 for some v, v 1 where v I = v I 1 but no predicate of the form u 2 → v 2 for some v 2 where v I = v I 2 , then we strictly prefer term u 1 over term u 2 when choosing term t i for e i .

Finding Minimal Models Previous work [START_REF] Reynolds | Finite model finding in SMT[END_REF] developed efficient techniques for finding small models for uninterpreted sorts in CVC4. We have found these techniques to be beneficial to the performance of the procedure in Figure 1. In particular, we use these techniques to find Σ-interpretations I in solve rec that interpret U as a finite set of minimal size. When combined with the aforementioned matching heuristics, these techniques lead to finding useful instantiations more quickly, since more terms are constrained to be equal to e i for i = 1, . . . , n in interpretations I. Symmetry Breaking The procedure in Figure 1 introduces a set of fresh constants L, which in turn introduce the possibility of discovering Σ-interpretations I that are isomorphic, that is, identical up to renaming of constants in L . Our procedure adds additional constraints to Γ that do not affect its satisfiability, but reduce the number of isomorphic models. In particular, we consider an ordering ≺ on the constants from L , and add constraints that ensure that all models (I, h) of Γ are such that if I 1 dom(h), then I 2 dom(h) for all 2 such that 1 ≺ 2 .

Example 1. Say we wish to show the validity of the entailment x y ∧ x → z | = SL ∃u . x → u, from the introductory example (Section 1), where x, y, z, u are of sort U of E. This entailment is valid iff the ∃ * ∀ * SL(E) U,U k formula ∃x∃y∃z∀u . x ≈ y ∧ x → z ∧ ¬x → u is (SL, E)-unsatisfiable. A run of the procedure in Figure 1 on this input constructs tuples k = (k x , k y , k z ) and e = (e u ), and set L = {k x , k y , k z , 1 , 2 }, noting that |x ≈ y ∧ x → z ∧ ¬x → u| = 1. We then call solve rec where Γ is initially empty. By miniscoping, our input is equivalent to ∃x∃y∃z . x ≈ y ∧ x → z ∧ ∀u . ¬x → u. On the first two recursive calls to solve rec, we may add k x ≈ k y and k x → k z to Γ by trivial instantiation of the first two conjuncts. On the third recursive call, Γ is (SL, E)-satisfiable, and we check the satisfiability of:

Γ = {k x k y , k x → k z , k x → e u ∧ (e u ≈ k x ∨ e u ≈ k y ∨ e u ≈ k z ∨ e u ≈ 1 ∨ e u ≈ 2 )}
Since k x → k z and k x → e u are in Γ , all Σ-interpretations I and heaps h such that I, h | = SL Γ are such that e I u = k I z . Since k z ∈ L, we may choose to add the instantiation ¬k x → k z to Γ, after which Γ is (SL, E)-unsatisfiable on the next recursive call to solve rec. Thus, our input is (SL, E)-unsatisfiable and the entailment is valid.

A modified version of the procedure in Figure 1 can be used for ∃ * ∀ * SL(T ) Loc,Datasatisfiability for theories T beyond equality, and where Loc and Data are not restricted to uninterpreted sorts. Notice that in such cases, we cannot restrict Σ-interpretations I in solve rec to interpret each e i as a member of finite set L, and hence we modify solve rec to omit the constraint restricting variables in e to be equal to a term from L in the check in Step 2. This modification results in a procedure that is sound both for "unsat" and "sat", but is no longer terminating in general. Nevertheless, it may be used as a heuristic for determining ∃ * ∀ * SL(T ) Loc,Data -(un)satisfiability.

Experimental Evaluation

We implemented the solve procedure from Figure 1 within the CVC4 SMT solver8 (version 1.5 prerelease). This implementation was tested on two kinds of benchmarks:

(i) finite unfoldings of inductive predicates, mostly inspired by benchmarks used in the SL-COMP'14 solver competition [START_REF] Sighireanu | Report on sl-comp 2014[END_REF], and (ii) verification conditions automatically generated by applying the weakest precondition calculus of [START_REF] Ishtiaq | Bi as an assertion language for mutable data structures[END_REF] to the program loops in Figure 2. All experiments were run on a 2.80GHz Intel(R) Core(TM) i7 CPU machine with 8MB of cache9 . We compared our implementation with the results of applying the CVC4 decision procedure for the quantifier-free fragment of SL [START_REF] Reynolds | A decision procedure for separation logic in SMT[END_REF] to a variant of the benchmarks, obtained by manual quantifier instantiation, as follows. Consider checking the validity of the entailment ∃x . φ(x) | = SL ∃y . ψ(y), which is equivalent to the unsatisfiability of the formula ∃x∀y . φ(x) ∧ ¬ψ(y). We first check the satisfiability of φ. If φ is not satisfiable, the entailment holds trivially, so let us assume that φ has a model. Second, we check the satisfiability of φ ∧ ψ. Again, if this is unsatisfiable, 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 check is inconclusive. The times in Table 1 correspond to checking satisfiability of ∃x∀y . φ(x) ∧ ¬ψ(y) using the solve procedure (Figure 1), compared to checking satisfiability of φ ∧ ¬ψ ∧ E, where E is manually generated.

In the first set of experiments (Table 1) we have considered inductive predicates commonly used as verification benchmarks [START_REF] Sighireanu | Report on sl-comp 2014[END_REF]. Here we check the validity of the entailment between lhs and rhs, where both predicates are unfolded n = 1, 2, 3, 4, 8 times. The entailment between pos 1 2 and neg 1 4 is skipped because it is not valid (since the negated formula is satisfiable, we cannot generate the manual instantiation).

The second set of experiments considers the verification conditions of the forms ϕ ⇒ wp(l, φ) and ϕ ⇒ wp n (l, φ), where wp(l, φ) denotes the weakest precondition of the SL formula φ with respect to the sequence of statements l, and wp n (l, φ) = wp(l, . . . wp(l, wp(l, φ)) . . .) denotes the iterative application of the weakest precondition n times in a row. We consider the loops depicted in Figure 2, where, for each loop l, we consider the variant zl as well, which tests that the data values contained within the memory cells are equal to a constant c 0 of sort Loc, by the assertions on line 2. The postconditions are specified by finite unfoldings of the inductive predicates list and zlist.

We observed that, compared to checking the manual instantiation, the fully automated solver was less than 0.5 seconds slower on 72% of the test cases, and less than 1 second slower on 79% of the test cases. The automated solver experienced 3 timeouts, where the manual instantiation succeeds (for tree vs tree with n = 8, ts vs ts with n = 3, and list n (u) * list 0 (v) vs wp n (rev, u = nil ∧ list n (v)) with n = 8). These timeouts are caused by the first call to the quantifier-free SL decision procedure, which fails to produce a model in less than 300 seconds (time not accounted for in the manually produced instance of the problem). ∃z . x →z * ls(z,y) manual < 0.01s < 0.01s < 0.01s < 0.01s < 0.01s tree(x) emp∧x=nil∨ tree(x) emp∧x=nil∨ solve < 0.01s 0.04s 1.43s 23.42s > 300s ∃l∃r . l r∧x →(l,r) * tree(l) * tree(r) ∃l∃r . x →(l,r) * tree(l) * tree(r) manual < 0.01s < 0.01s < 0.01s < 0.01s 0.09s ts(x,a) emp∧x=nil∨ ts(x,a) emp∧x=nil∨ solve < 0.01s 0.81s > 300s > 300s > 300s ∃l∃r . x y∧x →(l,r) * ts(l,y) * tree(r)∨ ∃l∃r . ∧x →(l,r) * ts(l,y) * tree(r)∨ manual < 0.01s 0.03s 103.89s > 300s > 300s ∃l∃r . x y∧x →(l,r) * tree(l) * ts(r,y) ∃l∃r . ∧x →(l,r) * tree(l) * ts(r,y) x →a * neg 3 (a,y) manual 0.01s 0.03s 0.05s 0.09s 0.45s pos 2 (x,a) x →a∨∃y . neg 4 (x,a) x →a∨∃y . solve -0.08s 0.15s 0.26s 1.33s

x →a * pos 2 (a,y) ¬x →a * neg 4 (a,y) manual -0.03s 0.06s 0.09s 0.46s Verification conditions list n (w) wp(disp,list n-1 (w)) solve 0.01s 0.03s 0.08s 0.19s 1.47s manual < 0.01s 0.01s 0.02s 0.05s 0.26s list n (w) wp n (disp,emp∧w=nil) solve 0.01s 0.06s 0.17s 0.53s 7.08s manual < 0.01s 0.02s 0.08s 0.14s 2.26s

zlist n (w) wp(zdisp,zlist n-1 (w)) solve 0.04s 0.05s 0.09s 0.19s 1.25s manual < 0.01s 0.01s 0.02s 0.04s 0.29s zlist n (w) wp n (zdisp,emp∧w=nil) solve 0.01s 0.10s 0.32s 0.87s 11.88s manual 0.01s 0.02s 0.07s 0.15s 2.20s

list n (u) * list 0 (v) wp(rev,list n-1 (u) * list 1 (v)) solve 0.38s 0.06s 0.11s 0.16s 0.56s manual 0.07s 0.03s 0.07s 0.11s 0.43s list n (u) * list 0 (v) wp n (rev,u=nil∧list n (v)) solve 0.38s 0.07s 0.30s 68.68s > 300s manual 0.08s 0.06s 0.11s 0.23s 1.79s

zlist n (u) * zlist 0 (v) wp(zrev,zlist n-1 (u) * zlist 1 (v)) solve 0.22s 0.07s 0.15s 0.21s 0.75s manual 0.04s 0.02s 0.04s 0.06s 0.31s zlist n (u) * zlist 0 (v) wp n (zrev,u=nil∧zlist n (v)) solve 0.23s 0.09s 0.17s 0.30s 2.06s manual 0.04s 0.02s 0.05s 0.09s 0.48s Table 1. Experimental results

Conclusions and Future Work

We present theoretical and practical results for the existence of effective decision procedures for the fragment of Separation Logic obtained by restriction of formulae to quantifier prefixes in the set ∃ * ∀ * . The theoretical results range from undecidability, when the set of memory locations is taken to be the set of integers and linear arithmetic constraints are allowed, to PSPACE-completeness, when locations and data in the cells belong to an uninterpreted sort, equipped with equality only. We have implemented a decision procedure for the latter case in the CVC4 SMT solver, using an effective counterexample-driven instantiation of the universal quantifiers. The procedure is shown to be sound, complete and termination is guaranteed when the input belongs to a decidable fragment of SL.

As future work, we aim at refining the decidability chart for ∃ * ∀ * SL(T ) Loc,Data , by considering the case where the locations are interpreted as integers, with weaker arithmetics, such as sets of difference bounds, or octagonal constraints. These results are likely to extend the application range of our tool, to e.g. solvers working on SL with inductive definitions and data constraints. The current implementation should also benefit from improvements of the underlying quantifier-free SL and set theory solvers.

Lemma 1 .

 1 [START_REF] Yang | Local Reasoning for Stateful Programs[END_REF] Lemma 94] Given an interpretation I and a heap h : U I fin (U I ) k , for each integer n > 0, each set of variables X ⊆ Vars, each set of locations L ⊆ U I such that L ∩ I(X) = ∅ and | |L| | = n, and each location v ∈ U I \ (I(X) ∪ {nil I } ∪ L), there exists a heap h : U I fin (U I ) k , with the following properties: 1

Fact 1

 1 There exists an interpretation I and a heap h such that | |U I | | = ℵ 0 and I, h | = SL ∀y 1 . . . ∀y n . ϕ(c, y) iff there exists an interpretation I , not constraining the cardinality of U I , and a heap h such that:

Fact 2

 2 For each interpretation I mapping x and y into N, I | = x = y 2 iff I can be extended to an interpretation of P as a finite set of consecutive perfect squares such that I | = θ x=y 2 .

1: while w nil do 2 :Fig. 2 .

 22 Fig. 2. Program Loops

lhs rhs n = 1 n

 1 = 2 n = 3 n = 4 n = 8Unfoldings of inductive predicates ls(x,y) emp∧x=y∨ ls(x,y) emp∧x=y∨ solve < 0.01s 0.02s 0.03s 0.05s 0.21s ∃z . x y∧x →z * ls(z,y)

pos 1

 1 (x,a) x →a∨∃y∃b . neg 1 (x,a) ¬x →a∨∃y∃b . solve 0.34s 0.01s 0.31s 0.76s 21.19s x →a * pos 1 (y,b) x →a * neg 1 (y,b) manual 0.04s 0.05s 0.08s 0.12s 0.53s pos 1 (x,a) x →a∨∃y∃b . neg 2 (x,a) x →a∨∃y∃b . solve 0.03s 0.12s 0.23s 0.46s 3.60s x →a * pos 1 (y,b) ¬x →a * neg 2 (y,b) manual 0.05s 0.08s 0.08s 0.12s 0.54s pos 2 (x,a) x →a∨∃y . neg 3 (x,a) ¬x →a∨∃y . solve 0.04s 0.13s 0.28s 0.48s 4.20s x →a * pos 2 (a,y)

Strictly speaking, the Bernays-Schönfinkel-Ramsey class refers to the ∃ * ∀ * fragment of firstorder logic with equality and predicate symbols, but no function symbols[START_REF] Lewis | Complexity results for classes of quantificational formulas[END_REF].

By writing I[σ ← S ] we ensure that all variables of sort σ are mapped by I to elements of S .

If x 1 → (x 2 , . . . , x n ) and x 1 → (x 2 , . . . , x n ) hold, this forces x i = x i , for all i = 2, . . . , n.

Extending the interpretation of Loc to include negative integers does not make any difference for the undecidability result.

The procedure is incorporated into the master branch of the SMT solver CVC4 (https:// github.com/CVC4), and can be enabled by command line parameter --quant-epr.

Available at http://cvc4.cs.nyu.edu/web/.

The CVC4 binary and examples used in these experiments are available at http://cs.uiowa.edu/ ˜ajreynol/VMCAI2017-seplog-epr.


James Mc Gilligan

Kaitlin Moore

Rodolphe Boudot

Joseph Griffin

A Arnold

Moshe Shuker

E Riis

E Donley

John Kitching

Two-photon imaging of a magneto-optical trap in a microfabricated cell for cold atom sensors

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.

I. INTRODUCTION

Laser cooling has driven technological advances in metrological experiments due to the long interrogation times and unperturbed atomic structure provided by cold-atoms [START_REF] Lamporesi | Determination of the Newtonian gravitational constant using atom interferometry[END_REF], [2], [START_REF] Kovachy | Quantum superposition at the half-meter scale[END_REF]. However, the bulky apparatus of cold atom clocks and interferometers have largely confined these instruments to laboratory environments, such that the growing market for compact atomic devices is currently dominated by pre-existing, miniaturized hot-vapor-cell technologies [START_REF] Schwindt | Chip-scale atomic magnetometer[END_REF], [START_REF] Lutwak | The Chip-Scale atomic clock -recent developments[END_REF], [START_REF] Vicarini | Demonstration of the mass-producible feature of a Cs vapor microcell technology for miniature atomic clocks[END_REF].

Recent studies into compact cold-atom devices have focused on optical miniaturization and total power consumption [START_REF] Pollock | Integrated magnetooptical traps on a chip using silicon pyramid structures[END_REF], [START_REF] Mcgilligan | Grating Chips for Quantum Technologies[END_REF], [START_REF] Saint | 3D-printed components for quantum devices[END_REF]. However, the UHV system has thus far eluded miniaturization on a micro-fabricated scale.

In previous literature, aluminosilicate glass (ASG) has been demonstrated to exhibit helium permeation rates significantly lower than borosilicates. This property makes ASG an attractive candidate for the development of MEMS cells that could potentially maintain UHV below 10 -7 Torr for timescales exceeding a few months [START_REF] Dellis | Low helium permeation cells for atomic microsystems technology[END_REF], [START_REF] Rushton | Contributed Review: The feasibility of a fully miniaturized magneto-optical trap for portable ultracold quantum technology[END_REF].

In this paper we report the fabrication of ASG based MEMS UHV cells with an optimized anodic bonding process for a high yield of successful cells. This study discusses laser cooling in such geometries and background-free imaging to overcome the dominant scatter in such planar stacked devices. This technology is proposed with an outlook to a passivelypumped UHV cell.

II. CELL FABRICATION

The vacuum cell configuration, presented in Fig. 1 (a), consists solely of a silicon frame sandwiched between two ASG wafers using anodic bonding [START_REF] Kitching | Chip-scale atomic devices[END_REF], [START_REF] Lee | Detailed characterization of anodic bonding process between glass and thin film coated silicon substrates[END_REF]. The silicon frames used in these tests are fabricated using a potassium hydroxide (KOH) wet etch through a 4 mm frame thickness. To achieve such an etch depth, 2 mm deep concentric rectangles are etched on each side of the silicon wafer surface. The KOH etching of the rectangle follows the Miller indices of the silicon crystal orientation to produce 54.7 • inner walls [START_REF] Chutani | Laser light routing in an elongated micromachined vapor cell with diffraction gratings for atomic clock applications[END_REF]. Overetching is then used to produce a smooth inner wall surface orthogonal to the upper and lower bonding surfaces.

The outer cell walls are diced to achieve frame dimensions of 40 mm× 20 mm× 4 mm. Such dimensions were chosen to provide a large surface bond area for increased probability of a hermetic seal, whilst providing a 12 mm inner diameter to facilitate laser cooling with 1 cm diameter beams. The upper ASG is drilled and bonded to a silicon washer and borosilicate tube that is sealed to a vacuum flange. This attachment permits these bonded cells to be connected to a standard ion pump to characterize the cell vacuum and perform initial laser cooling tests. A thorough study of anodically bonding ASG MEMS cells will be presented at the conference.

III. ACTIVELY PUMPED MEMS MOT

The MEMS cell was pumped down to 10 -9 Torr and aligned with a grating-magneto-optical-trap (GMOT) [START_REF] Nshii | A surface-patterned chip as a strong source of ultracold atoms for quantum technologies[END_REF] for a compact and robust laser cooling platform. With the silicon walls of the MEMS cell restricting optical access to nonorthogonal angles for imaging, the CCD must look down upon a scatter dominated diffractive optic. Imaging with 780 nm light restricts the ability to well resolve cold atom fluorescence from environmental scatter, as shown in Fig. 1 (b). To overcome the scatter in this planar stacked geometry, a second laser is used to couple atoms to the 5D 5/2 electronic state, where atoms can cascade via the 6P 3/2 state with 420 nm light emission [START_REF] Ohadi | Magnetooptical trapping and background-free imaging for atoms near nanostructured surfaces[END_REF], [START_REF] Sheludko | State-selective imaging of cold atoms[END_REF]. Imaging with a CCD and 420 nm bandpass filter refines the observed light to the atomic fluorescence, shown in Fig. 1 (c).

IV. CONCLUSION AND OUTLOOK

Our characterization of anodically bonding aluminosilicate glass vacuum cells for UHV applications has been optimized for a high yield of successful cells. Such MEMS cells have been connected to an external ion pump and associated to a laser cooling optics system to demonstrate the detection of a magneto-optical trap using background-free imaging. The latest results and outlooks will be presented at the conference.

Fig. 1 .

 1 Fig. 1. (a): Micro-fabricated alkali vapor cell coupled to a grating MOT system. The science cell consists of silicon frame, anodically bonded to equally sized ASG. The upper ASG glass is drilled and bonded to a silicon washer to permit anodic bonding to a borosilicate tube that connects the cell to a standard ion pump and alkali dispenser. (b): Imaging the 780 nm fluorescence. (c): Imaging the 420 nm fluorescence with a bandpass filter.

ACKNOWLEDGMENT J. P. M. gratefully acknowledges support from the English Speaking Unions Lindemann Fellowship. R. Boudot is supported by Délegation Générale de l'Armement and the NIST guest-researcher program. The authors would like to thank D. Bopp and Dr. Moshe for helpful discussions. The views, opinions, and/or findings contained in this letter are those of the authors and should not be interpreted as representing the official views or policies of the Department of Commerce or the U.S. Government.