Radu Iosif
email: radu.iosif@univ-grenoble-alpes.fr

Program Verification with Separation Logic

Separation Logic is a framework for the development of modular program analyses for sequential, inter-procedural and concurrent programs. The first part of the paper introduces Separation Logic first from a historical, then from a program verification perspective. Because program verification eventually boils down to deciding logical queries such as the validity of verification conditions, the second part is dedicated to a survey of decision procedures for Separation Logic, that stem from either SMT, proof theory or automata theory. Incidentally we address issues related to decidability and computational complexity of such problems, in order to expose certain sources of intractability.

How it all Started

Separation Logic [Rey02] is nowadays a major paradigm in designing scalable modular verification methods for programs with dynamic memory and destructive pointer updates, which is something that most programs written using imperative languages tend to use. The basic idea that enabled the success, both in academia and in industry, is the embedding of a notion of resource within the syntax and proof system of the logic, before it's now widely accepted semantics was even defined.

Resources are understood as items, having finite volume, that can be split (separated) among individuals. Since volumes are finite, splitting reduces the resources in a measurable way and cannot be done ad infinitum. The story of how resources and separation ended up in logic can be traced back to Girard's Linear Logic [Gir87], the first one to restrict the proof rules of weakening and contraction in natural deduction:

With them, the sequents Γ, ϕ ψ and Γ, ϕ, ϕ ψ can be deduced one from another, but without them, they become unrelated. Removing the (W) and (C) rules leads to two distinct conjunction connectives, illustrated below by their introduction rules:

While ∧ is the classical conjunction, for which (W) and (C) apply, * is a new separating conjunction, for which they don't [OP99].

In natural deduction, conjunction and implication are intertwined, the following introduction rule being regarded as the definition of the implication:

Γ, ϕ ψ Γ ϕ → ψ (→ I)
The connection is given by the fact that the comma on a sequent's antecedent is interpreted as conjunction. However, if now we have two conjunctions, we must distinguish them in the antecedents, and moreover, we obtain two implications:

Γ; ϕ ψ Γ ϕ → ψ (→ I) Γ, ϕ ψ Γ ϕ -- * ψ (-- * I)
We use semicolumn and comma for the classical and separating conjunctions, while → and -- * denote the classical and separating implications, respectively. Antecedents are no more viewed as sets but as trees (bunches) with leaves labeled by propositions and internal nodes labeled with semicolumns or commas. Furthermore, (-- * I) leads to consumption of antecedent nodes and cannot be applied indefinitely. This is where resources became part of the logic, before any semantics was attributed to it.

Heaps as Resources

Since the most expensive resource of a computer is the memory, it is only natural to define the semantics of the logic (initially called BI, for Bunched Implications) with memory as the resource. There are several memory models and the one on the lowest level views memory as an array of bounded values indexed by addresses. However, the model which became widespread is the one allowing to reason about the shape (topology) of recursive data structures. In this model, the memory (heap) is viewed as a graph, where nodes represent cells and edges represent pointers between cells, and there is no comparison between cells, other than equality.

This new logic, called Separation Logic (SL), is equipped with equality and two atomic propositions, emp for the empty heap and x → (y 1 , . . . , y k ) meaning that x is the only allocated memory address and there are exactly k pointers from x to y 1 , . . . , y k , respectively. From now on, k is a strictly positive parameter of the logic and SL k denotes the set of formulae generated by the grammar below:

ϕ := ⊥ | | emp | x ≈ y | x → (y 1 , . . . , y k ) | ϕ ∧ ϕ | ¬ϕ | ϕ * ϕ | ϕ -- * ϕ | ∃x . ϕ
SL k formulae are interpreted over SL-structures I = (U, s, h), where U is a countable set, called the universe, the elements of which are called locations, s : Var U is a mapping of variables to locations, called a store and h : U fin U k is a finite partial mapping of locations to k-tuples of locations, called a heap. We denote by dom(h) the domain of the heap h. A cell ∈ U is allocated in I if ∈ dom(h) and dangling otherwise.

The notion of separable resources is now embedded in the semantics of SL. Two heaps h 1 and h 2 are disjoint if and only if dom(h 1 ) ∩ dom(h 2 ) = / 0, in which case h 1 h 2 denotes their union ( is undefined for non-disjoint heaps). A heap h is a subheap of h if and only if h = h h , for some heap h . The relation (U, s, h) |= ϕ is defined inductively below:

(U, s, h) |= emp ⇔ h = / 0 (U, s, h) |= x → (y 1 , . . . , y k ) ⇔ h = { s(x), (s(y 1 ), . . . , s(y k )) } (U, s, h) |= ϕ 1 * ϕ 2 ⇔ there exist disjoint heapsh 1 , h 2 such that h = h 1 h 2 and (U, s, h i ) |= ϕ i , for i = 1, 2 (U, s, h) |= ϕ 1 -- * ϕ 2 ⇔ for all heaps h disjoint from h such that (U, s, h ) |= ϕ 1 , we have (U, s, h h) |= ϕ 2
The semantics of equality, boolean and first-order connectives is the usual one and thus omitted. The question is now what can be expressed in SL and what kind of reasoning1 could be carried out? First, one defines a single (finite) heap structure up to equality on dangling cells. This is done considering the following fragment of symbolic heaps:

Π := x ≈ y | x = y | Π 1 ∧ Π 2 Σ := emp | x → (y 1 , . . . , y k ) | Σ 1 * Σ 2
The Π formulae are called pure as they do not depend on the heap. The Σ formulae are called spatial. A symbolic heap is a conjunction Σ ∧ Π, defining a finite set of heaps.

For instance, x → (y 1 , y 2 ) * y 1 → (x, y 2 ) ∧ y 1 = y 2 defines cyclic heaps of length two, in which x and y 1 are distinct, x points to y 1 , y 1 points to x and both point to y 2 . Further, y 2 is distinct from y 1 , but could be aliased with x. Observe that x → (y 1 , y 2 ) * y 1 → (x, y 2 ) ∧ x ≈ y 1 is unsatisfiable, because x → (y 1 , y 2 ) and y 1 → (x, y 2 ) define separated singleton heaps, in which x ≈ y 1 is not possible.

However, being able to define just bounded heaps is not satisfactory, because one needs to represent potentially infinite sets of structures of unbounded size, such as the ones generated during the execution of a program. Since most imperative programmers are used to working with recursive data structures, a natural requirement is using SL to define the usual recursive datatypes, such as singly-and doubly-linked lists, trees, etc. It turns out that this requires inductive definitions. For instance, the following inductive definitions describe 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 contains at least one element which is disjoint from the rest of the list segment. Observe that x → z and ls(z, y) hold over disjoint parts of the heap, which ensures that the definition unfolds producing distinct cells. 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.

As usual, the semantics of inductive definitions is given by the least fixed point of a monotone function between sets of finite SL-structures. To avoid clutter, we omit this definition, but point out that the reasons why symbolic heaps define monotone functions are that (i) * 's do not occur negated, and (ii) -- * 's are not used.

In fact, one may wonder, at this point, why only * 's are used for specification of data structures and what is the rôle of -- * in reasoning about programs? The answer is given in the next section.

Program Verification

Program verification means providing a proof for the following problem: given a program P and a set of states Ψ, is there an execution of P ending in a state from Ψ? More concretely, Ψ can be a set of "bad" states in which the program ends after attempting to dereference an unallocated pointer variable, or after leaking memory. A program proof consist in annotating the program with assertions that (i) must hold each time the control reaches an assertion site, such that (ii) the set Ψ is excluded from the reachable states of P.

Ensuring the point (i) requires proving the validity of a certain number of Hoare triples of the form {φ} C {ψ}, each of which amounts to proving the validity of an entailment φ ⇒ pre(C, ψ), or equivalently, post(C, φ) ⇒ ψ, where pre and post are the weakest precondition and the strongest postcondition predicate transformers. Such entailments are called verification conditions.

In the seminal papers of Ishtiaq and O'Hearn [START_REF] Samin | Bi as an assertion language for mutable data structures[END_REF] and Reynolds [START_REF] Reynolds | Separation logic: A logic for shared mutable data structures[END_REF], SL was assigned the purpose of an assertion logic in a Hoare-like logic used for writing correctness proofs of pointer-manipulating programs. This turn from proof theory [START_REF] O'hearn | The logic of bunched implications[END_REF] to program proofs removes a long-standing thorn from the side of Hoare logicians, namely that the substitution-based assignment rule {φ[E/x]} x = E {φ} [START_REF] Hoare | An axiomatic basis for computer programming[END_REF] is no longer valid in the presence of pointers and aliasing.

The other problems, originally identified in the seminal works of Floyd [START_REF] Floyd | Assigning meanings to programs[END_REF] and Hoare [START_REF] Hoare | An axiomatic basis for computer programming[END_REF] are how to accomodate program proofs with procedure calls and concurrency. Surprisingly, the * connective provides very elegant solutions to these problems as well, enabling the effective transfer of this theory from academia to industry.

In general, writing Hoare-style proofs requires lots of human insight, essentially for (i) infering appropriate loop invariants, and (ii) solving the verification conditions obtained from the pre-or postcondition calculus that captures the semantics of a straightline program. With SL as an assertion language, automation is possible but currently at (what we believe are) the early stages.

For instance, the problem (i) can be tackled using abstract interpretation [START_REF] Cousot | Systematic design of program analysis frameworks[END_REF], but the (logical) abstract domains currently used are based on the hardcoded ls(x, y) predicate, making use of specific properties of heaps with a single pointer field, that are composed of lists, and which can be captured by finitary abstractions [BBH + 06]. An extension to nested lists (doubly-linked lists of . . . of doubly-linked lists) has been since developped in the SPACEINVADER tool [BCC + 07] and later shipped to industry in the INFER tool [START_REF] Calcagno | Infer: An automatic program verifier for memory safety of c programs[END_REF].

Alternatives to invariant inference using fixed point computations are also possible. These methods use the expressive power of the higher-order inductive definitions of SL and attempt to define inductive predicates that precisely define loop invariants, using only a single symbolic execution pass through the loop [START_REF] Loc | Shape analysis via second-order bi-abduction[END_REF]. The difficulty of the verification problem is then shipped to the decision procedure that solves the verification condition thus obtained (ii). This is probably the real problem standing in front of the researchers that aim at developping a fully push-button program verification method for real-life programs, based on SL. We shall survey this issue at large in §4

While Programs

Perhaps the longest lasting impression after reading Ishtiaq and O'Hearn's paper [START_REF] Samin | Bi as an assertion language for mutable data structures[END_REF] is that a sound and complete weakest precondition calculus for programs with pointers and destructive updates has finally been found. But let us first recall the problem with Hoare's substitution-based assignment rule. Consider the triple

{(y.data = 2 ∧ x = y)[1/x.data]} x.data := 1 {y.data = 2 ∧ x = y}
which is the same as {y.data = 2 ∧ x = y} x.data := 1 {y.data = 2 ∧ x = y} because the substitution has no effect on the precondition. The triple is clearly invalid, because the assignment x.data := 1 makes the assertion x.data = 2 false.

The solution provided by SL is of great simplicity and elegance. Since pointer updates alter a small part of the heap, we can "remove" this part using * and "replace" it with an updated heap, using -- * , while requiring that the postcondition hold afterwards:

{∃x∃y . u → (x, y) * ((u → (v, y)) -- * φ)} u.1 := v {φ}
where u.1 := v denotes the assignment of the first selector of the cell referred to by u to v. We have a similar weakest precondition for memory allocation, where we adopt the more structured object-oriented constructor cons(v, w) instead of C's malloc(n):

{∀x. (x → (v, w)) -- * φ[x/u]} u := cons(v, w) {φ}
Observe that this calculus produces preconditions that mix * and -- * with quantifiers. Very early, this hindered the automation of program proofs, because at the time, there was no "automatic theorem prover which can deal with the form of these assertions (which use quantification and the separating implication)" [START_REF] Berdine | Symbolic execution with separation logic[END_REF]. This issue, together with a rather coarse undecidability result for quantified SL formulae [START_REF] Calcagno | Computability and complexity results for a spatial assertion language for data structures[END_REF] made researchers almost entirely forget about the existence of -- * and of the weakest precondition calculus, for more than a decade. During this time, program verifiers used (and still do) incomplete, overapproximating, postcondition calculi on (inductive definitions on top of) * -based symbolic heaps. In the light of recent results concerning decision procedures for the base assertion SL language, we believe this difficulties can be overcome. A detailed presentation of these results is given in §4.1.

Before going further, an interesting observation can be made. The weakest precondition of a straight-line program, in which more than one such statement occurs in a sequence, would be a formula in which first-order quantifiers occur within the scope of a separating connective. This could potentially be problematic for automated reasoning because, unlike first order logic, SL formulae do not have a prenex form: φ * ∀x . ψ(x) ≡ ∀x . φ * ψ(x) and φ -- * ∃x . ψ(x) ≡ ∃x . φ -- * ψ(x). However, the following notion of precise formulae comes to rescue in this case [OYR04]: Definition 1. A SL formula φ is precise if and only if, for all SL-structures I = (U, s, h) there exists at most one subheap h of h such that (U, s, h ) |= φ.

If φ is precise, we recover the equivalences φ * ∀x . ψ(x) ≡ ∀x . φ * ψ(x) and φ -- * ∃x . ψ(x) ≡ ∃x . φ -- * ψ(x). Moreover, since formulae such as x → (y, z) are precise, one can hoist the first-order quantifiers and write any precondition in prenex form. As we shall see ( §4.1) prenexisation of formulae is an important step towards the decidability of the base assertion language.

Local Reasoning and Modularity

Being able to provide easy-to-write specifications of recursive data structures (lists, trees, etc.) as well as concise weakest preconditions of pointer updates, were the first salient features of SL. With separating conjunction * as the main connective, a principle of local reasoning has emerged:

To understand how a program works, it should be possible for reasoning and specification to be confined to the cells that the program actually accesses. The value of any other cell will automatically remain unchanged [START_REF] O'hearn | Local reasoning about programs that alter data structures[END_REF].

The rôle of the separating conjunction in local reasoning requires little explanation. If a set of program states is specified as ϕ * ψ, and the update occurs only in the ϕ part, then we are sure that ψ is not affected by the update and can be copied from pre-to postcondition as it is. This is formalized by the following frame rule: {ϕ} P {φ} {ϕ * ψ} P {φ * ψ} modifies(P) ∩ var(ψ) = / 0

where modifies(P) is the set of variables whose value is changed by the program P, defined recursively on the syntactic structure of P.

The frame rule allows to break a program proof into small pieces that can be specified locally. However, locality should not be confounded with modularity, which is the key to scalability of program verification technique. Indeed, most large, industrial-size programs are built from a large number of small components, such as functions (procedures) or threads, in a concurrent setting.

By a modular program verification we understand a method capable of inferring specifications of any given program component in isolation, independently on the context in which the other components interact with the component's environment. Then the local specifications are combined into a global one, using the frame rule or a variant thereof. Observe that this is not to be mixed up with program verification algorithms that store and reuse analysis results.

An example of modular program verification with SL is the compositional shape analysis based on the inference of footprints [START_REF] Calcagno | Footprint analysis: A shape analysis that discovers preconditions[END_REF]. These are summaries specified as pairs of pre-/postconditions, that guarantee absence of implicit memory faults, such as null pointer dereferences or memory leaks. The important point is that footprints can be inferred directly from the program, without user-supplied pre-or postconditions.

Combining component footprints into a global verification condition is the other ingredient of a modular verification technique. Since footprints are generated without knowledge of their context, sometimes their combination requires some "adjustment". To understand this point, consider an interprocedural analysis in which a function foo(x, y) is invoked at a call site. The summary of the function, inferred by footprint analysis, is say ls(x, z) * ls(y, nil), using the previously defined inductive predicates ( §2). Informally, this sais that there is a list segment from x to z and disjointly a nil-ending list starting with y. Assume further that x → z is the assertion at the call site. Clearly x → z does not entail ls(x, z) * ls(y, nil), in which case a classical interprocedural analysis would give up.

However, an SL-based interprocedural analysis uses the frame rule for function calls and may reason in the following way: find a frame φ such that x → z * φ ⇒ ls(x, z) * ls(y, nil). In this case, a possible answer (frame) is φ = ls(y, nil). If the current precondition of the caller of foo(x, y) is ϕ, we percolate the frame all the way up to the caller and modify its precondition to ϕ * φ, as local reasoning allows us to do. This method is implemented by the INFER analyzer and is used, on an industrial scale, at Facebook [START_REF] Calcagno | Infer: An automatic program verifier for memory safety of c programs[END_REF].

This style of modular verification introduces abductive reasoning as a way to perform frame inference. In classical logic, the abduction problem is: given an assumption φ and a goal ψ, find a missing assumption X such that φ ∧ X ⇒ ψ. Typically, we aim at finding the weakest such assumption, which belongs, moreover, to a given language (a disjunction of conjunctive assertions pertaining to a restricted set). If we drop the latter requirement, about the allowed form of X, we obtain the weakest solution X = φ → ψ.

Abductive reasoning in SL follows a very similar pattern. An abduction problem is: given assertions φ and ψ, find an assertion X such that φ * X ⇒ ψ. Similar to the classical case, the weakest solution, in this case is . . . X = φ -- * ψ! So the long-forgotten magic wand comes back to program analysis, this time by way of abduction. However, since decision procedures for SL still have a hard time in dealing with -- * , they use underapproximations of the weakest solutions, that are mostly good enough for the purposes of the proof [START_REF] Calcagno | Compositional shape analysis by means of bi-abduction[END_REF].

Decision Procedures

As mentioned in the introduction of §3, the job of a verifier is turning a program verification problem into a (finite) number of logical entailments of the form φ ⇒ ψ, called verification conditions. In this section, we survey how one can establish the validity of such entailments, provided that φ and ψ are SL formulae.

If the fragment of SL to which φ and ψ belong is closed under negation, the entailment φ ⇒ ψ is valid if and only if the formula φ ∧ ¬ψ is unsatisfiable. Usually negation is part of basic SL assertions, that do not use inductive definitions. These are mostly discussed in §4.1. In this case, we reduce the entailment to a satisfiability problem, that ultimately, can be solved using SMT technology.

If the logic in which φ and ψ are written does not have negation, which is typically the case of inductive definitions built on top of symbolic heaps, we deal with entailments directly, either by proof-theoretic (we search for a sequent calculus proof of the entailment) or automata-theoretic (we reduce to the inclusion between the languages of two automata) arguments. The pros and cons of each approach are discussed in §4.2.

Basic Logic

Let us consider the language SL k given in §2. For k ≥ 2, undecidability of this logic occurs even if separating connectives are almost not used at all. If one encodes an uninterpreted binary relation R(x, y) as ∃z . z → (x, y) * , undecidability occurs as a simple consequence of Trakhtenbrot's result for finite satisfiability of first-order logic [START_REF] Börger | The Classical Decision Problem[END_REF]. If k = 1, the logic is still undecidable, but the fragment of SL 1 without -- * becomes decidable, with a nonelementary recursive complexity lower bound [START_REF] Brochenin | On the almighty wand[END_REF].

On the other hand, the quantifier-free fragment of SL k is PSPACE-complete, for any k ≥ 1 [START_REF] Calcagno | Computability and complexity results for a spatial assertion language for data structures[END_REF]. The crux of this proof is a small model property of quantifierfree SL k . If a formula φ in this language has a model (U, s, h) then it has a model where ||h|| = O(size(φ)). This also provides effective algorithms for the satisfiability problem.

It is possible, for instance, to encode the quantifier-free SL k formula in first-order logic with bitvectors and use existing SMT technology for the latter [START_REF] Calcagno | From separation logic to first-order logic[END_REF], or directly using a DPLL(T )-style algorithm that attempts to build a model of bounded size and learns from backtracking [START_REF] Reynolds | A decision procedure for separation logic in smt[END_REF].

The quantifier-free fragment of SL k is also important in understanding the expressiveness of SL, relative to that of classical first-and second-order logics. This point addresses a more fundamental question, relative to the presence of the separating connectives * and -- * : is it possible to reason about resources and separation in first-order logic, or does one need quantified relations, as the heap semantics of SL k suggests?

It turns out that, surprisingly, the entire prenex fragment of SL k can be embedded into uninterpreted first-order logic. This is the set of formulae Q 1 x 1 . . . Q n x n . φ, where φ is quantifier-free. First, we consider a small set of patterns, called test formulae, that use * and -- * in very restricted ways: Definition 2. The following patterns are called test formulae: In contrast with the majority of the literature on Separation Logic, here the universe of available memory locations (besides the ones occurring in the heap, which is finite) is not automatically assumed to be infinite. In particular, the finite universe hypothesis is useful when dealing with bounded memory issues, for instance checking that the execution of the program satisfies its postcondition, provided that there are sufficiently many available memory cells. Having different interpretations of the universe is also motivated by a recent integration of SL k within the DPLL(T )-based SMT solver CVC4 [START_REF] Reynolds | A decision procedure for separation logic in smt[END_REF][START_REF] Reynolds | Reasoning in the bernaysschönfinkel-ramsey fragment of separation logic[END_REF], in which the SL theory is parameterized by the theory of locations, just like the theories of arrays and sets are parameterized by theories of values.

x → (y 1 , . . . , y k ) def = x → (y 1 , . . . , y k ) * |U| ≥ n def = ¬( -- * ¬(|h| ≥ n)), n ∈ N alloc(x) def = x → (x, . . . , x) k times -- * ⊥ |h| ≥ |U| -n def = |h| ≥ n + 1 -- * ⊥, n ∈ N |h| ≥ n def =    |h| ≥ n -1 * ¬emp, if n > 0 , if n = 0 ⊥, if n = ∞
A first nice result is that any quantifier-free SL k formula is equivalent to a boolean combination of test formulae [START_REF] Echenim | On the expressive completeness of bernays-schönfinkel-ramsey separation logic[END_REF]. Then we can define an equivalence-preserving translation of the quantifier-free fragment of SL k into FO. Let d be a unary predicate symbol and let f i (for i = 1, . . . , k) be unary function symbols. We define the following transformation from quantified boolean combinations of test formulae into first order formulae:

Θ(x ≈ y) def = x ≈ y Θ(x → (y 1 , . . . , y k )) def = d(x) ∧ k i=1 y i ≈ f i (x) Θ(alloc(x)) def = d(x) Θ(¬φ) def = ¬Θ(φ) Θ(φ 1 • φ 2 ) def = Θ(φ 1 ) • Θ(φ 2 ) if • ∈ {∧, ∨, →, ↔} Θ(Qx . φ) def = Qx . Θ(φ) if Q ∈ {∃, ∀} Θ(|U| ≥ n) def = ∃x 1 , . . . , x n . distinct(x 1 , . . . , x n ) Θ(|h| ≥ n) def = ∃x 1 , . . . , x n . distinct(x 1 , . . . , x n ) ∧ n i=1 d(x i ) Θ(|h| ≥ |U| -n) def = ∃x 1 , . . . , x n ∀y . n i=1 y ≈ x i → d(y)
As a result of this translation, any formula of the prenex fragment of SL k is equivalent to a first-order formula that uses one monadic predicate and k monadic function symbols. Thus, we obtain the decidability of the prenex fragment of SL 1 as a consequence of the decidability of first-order logic with one monadic function symbol and any number of monadic predicate symbols [START_REF] Börger | The Classical Decision Problem[END_REF]. Moreover, for k ≥ 2, undecidability occurs even for the quantifier prefix of the form ∃ * ∀ * , if universally quantified variables occur under the scope of -- * . However, if this is not the case, ∃ * ∀ * fragment of SL k becomes PSPACE-complete [START_REF] Echenim | On the expressive completeness of bernays-schönfinkel-ramsey separation logic[END_REF].

Interestingly, if k = 1 again, the ∃ * ∀ * fragment is PSPACE-complete independently of how -- * is used [START_REF] Echenim | The complexity of prenex separation logic with one selector[END_REF]. This result points out the difference between the prenex fragment of SL 1 and SL 1 with unrestricted use of quantifiers, which is undecidable: in fact, the full second-order logic can be embedded within it [START_REF] Brochenin | On the almighty wand[END_REF]. For program verification, the good news is that, as discussed in §3, the prenex fragment is closed under weakest preconditions, making it possible to verify straight-line programs obtained by loop unfolding, à la Bounded Model Checking.

Inductive Definitions

Let us now turn to the definition of recursive data structures using inductive definitions in SL k . As a first remark, the base assertion language is usually that of symbolic heaps Σ ∧ Π, where Σ is either emp or a finite * -conjunction and Π is either or a nonempty conjunction of equalities and disequalities between variables. A system of inductive definitions is a set of rules of the form p(x 0 ) ← Σ∧Π * p 1 (x 1 ) * . . . p n (x n ), where w.l.o.g. x 0 , . . . , x n are pairwise disjoint sets of variables and var(Σ ∧ Π) ⊆ n i=0 x i . The examples below show the inductive definitions of a doubly-linked list dll(hd, p, tl, n) and of a tree with linked leaves tll(root, ll, lr), respectively: dll(hd, p, tl, n) ← hd → (n, p) ∧ hd = tl dll(hd, p, tl, n) ← ∃x . hd → (x, p) * dll(x, hd, tl, n) ... A solution of an inductive predicate system is a mapping of predicates to sets of SL-structures and the semantics of a predicate p, denoted [[p]] corresponds to the set of structures assigned to it by the least solution of the system. The entailment problem is given a system and two predicates p and q, does [[p]] ⊆ [[q]] hold? In general, this problem is undecidable [AGH + 14,IRV14].

Automata-based Techniques

As usual, we bypass undecidability by defining a number of easy-to-check restrictions on the system of predicates:

-Progress: each rule allocates exactly one node, called the root of the rule. This condition makes our technical life easier, and can be lifted in many cases -rules with more than one allocation can be split by introducing new predicates. -Connectivity: for each inductive rule of the form Σ * p 1 (x 1 ) * . . . * p n (x n ) ∧ Π, there exists at least one edge between the root of the rule and the root of each rule of p i , for all i ∈ [1, n]. This restriction prevents the encoding of context-free languages in SL, which requires disconnected rules, leading to undecidability. -Establishment: all existentially quantified variables in a recursive rule are eventually allocated. This restriction is not required for the satisfiability problem, but it is essential for entailment.

The fragment of SL obtained by applying the above, rather natural, restrictions, is denoted SL btw in the following. The proof of decidability for entailments in SL btw relies on three main ingredients: 1. for each predicate p in the system, all heaps from the least solution [[p]] are represented by graphs, whose treewidth is bounded by a linear function in the size of the system. 2. we define, for each predicate p, a formula Φ p in monadic second-order logic (MSO) of graphs whose models are exactly the graphs encoding the heaps from the least solution

[[p]]. 3. the entailment problem [[p]] ⊆ [[q]
] is reduced to the satisfiability of an MSO formula Φ p ∧ ¬Φ q . Since all models of p (thus of Φ p ) have bounded treewidth, this problem is decidable, by Courcelle's Theorem [START_REF] Courcelle | The monadic second-order logic of graphs. i. recognizable sets of finite graphs[END_REF]. This approach suggests that a direct encoding of the least solution of a system of inductive definitions is possible, using tree automata. That is, for each predicate p, we define a tree automaton A p that recognizes the set of structures from [[p]], and the entailment problem

[[p]] ⊆ [[q]]
reduces to a language inclusion problem between tree automata L(A p ) ⊆ L(A q ). However, there are instances of the entailment problem that cannot be directly solved by language inclusion between tree automata, due to the following polymorphic representation problem: the same set of states can be defined by two different inductive predicates, and the tree automata mirroring their definitions will report that the entailment does not hold. For example, doubly-linked lists can also be defined in reverse:

dll rev (hd, n, tl, p) ≡ hd → (p, n) ∧ hd = tl ∨ ∃x . tl → (x, n) * dll rev (hd, tl, x, p) A partial solution is to build tree automata only for a restriction of SL btw , called the local fragment (SL loc ). The structures that are models of predicates defined in this fragment have the following nice property: whenever the same structure is encoded by two different spanning trees, the two trees are related by a rotation relation, which changes the root to an arbitrary internal node, and the orientation of the edges from the path to the root to that node. We can thus check [[p]] ⊆ [[q]] in this fragment by checking the inclusion between A p and A rot q , where A rot q is automaton recognizing the closure of the languge of A q under rotation. Moreover, since the rotation closure of a tree automaton is possible in polynomial (quadratic) time, the entailment problem for SL loc can be shown to be EXPTIME-complete [START_REF] Iosif | Deciding entailments in inductive separation logic with tree automata[END_REF]. It is still an open question, whether this tight complexity bound applies to the entire SL btw logic.

Proof-based Techniques An experimental evaluation of SL inductive entailment solvers, carried out during the SL-COMP 2014 solver competition [START_REF] Sighireanu | Report on sl-comp 2014[END_REF], shows the strengths and weaknesses of automata-based versus proof-based solvers. On one hand, automatabased solvers can cope with polymorphic representations in a much better way than proof-based solvers, which require complex cut rules, whose completness is far from being understood [START_REF] Chu | Automatic induction proofs of data-structures in imperative programs[END_REF].

On the other hand, proof-based solvers are more flexible in deadling with extensions of the base theory (symbolic heaps), such as arbitrary equalities and disequalities or even (limited forms of) data constraints. Moreover, they can easily interact with SMT solvers and discharge proof obligations belonging to the base logic. However, as the example below shows, this requires quantifiers.

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) The bottom inference rule introduces one of the two cases produced by unfolding the inductive definitions on both sides of the sequent2 . The second inference rule is a reduction of the sequent obtained by unfolding, to a sequent matching the initial one (by renaming z to x), and allows to close this branch of the proof by an inductive argument, based on the principle of infinite descent [START_REF] Brotherston | Automated cyclic entailment proofs in separation logic[END_REF].

¬(x ≈ y) ∧ x → z * ls(z, y) ∃u . x → u * ls(u, y) ∨ emp ∧ x ≈ y ¬(x ≈ y) ∧ x → z |= ∃u
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 prenex 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 cell 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.

This example shows the need for a tight interaction between the decision procedures for the (quantified) base logic SL k and the entailment provers for systems of inductive definitions built on top of it. An implementation of an inductive prover that uses SMT technology to simplify sequents is INDUCTOR [START_REF] Serban | Inductor: an entailment checker for inductive systems[END_REF], which uses CVC4 [BCD + 11] for the reduction step. Just like the CYCLIST prover [START_REF] Brotherston | A generic cyclic theorem prover[END_REF] before, INDUCTOR is based on the principle of infinite descent [START_REF] Brotherston | Automated cyclic entailment proofs in separation logic[END_REF].

Future plans for INDUCTOR involve adding cut rules that would allow dealing with polymorphic representations of recursive data structures in a proof-theoretic fashion, as well as dealing with theories of the data within memory cells.

Conclusions

This paper surveys Separation Logic, a logical framework used to design modular and local analyses for programs that manipulate pointers and dynamically allocated memory cells. The essence of the logic is a notion of separable resource, which is embedded in the syntax and the proof system of the logic, before its nowadays widely accepted semantics was adopted. Program verifiers based on Separation Logic use local reasoning to model the updates in a compact way, by distinguishing the parts of the heap modified from the ones that are unchanged. The price to be paid for this expressivity is the difficulty of providing push-button decision procedures for it. However, recent advances show precisely what are the theoretical limits of decidability and how one can accomodate interesting program verification problems within them.

  and x ≈ y, where x, y ∈ Var, y ∈ Var k and n ∈ N ∞ is a positive integer or ∞.Observe first that -- * is instrumental in defining allocation without the use of existential quantifiers, as in alloc(x) def = ∃y 1 . . . ∃y n . x → (y 1 , . . . , y k ) * . Second, it can express cardinality constraints relative to the size of the universe |U| ≥ n and |h| ≥ |U|n, assuming that it is finite.

  , ll, lr) ← root → (nil, nil, lr) ∧ root = ll tll(root, ll, lr) ← ∃l∃r∃z . root → (l, r, nil) * tll(l, ll, z) * tll(r, z, lr)

  . x → u by instantiation u ← z ls(x, y) ls(x, y)

We use the term "reasoning" in general, not necessarily push-button automated decision.

The second case emp ∧ x ≈ y ∃u . x → u * ls(u, y) ∨ emp ∧ x ≈ y is trivial and omitted for clarity.


Radu Iosif
email: radu.iosif@univ-grenoble-alpes.fr

Xiao Xu
email: xiao.xu@univ-grenoble-alpes.fr

Abstraction Refinement for Emptiness Checking of Alternating Data Automata

. We have implemented both methods and report the results of an experimental comparison.

Introduction

The language inclusion problem is recognized as being central to verification of hardware, communication protocols and software systems. A property is a specification of the correct executions of a system, given as a set P of executions, and the verification problem asks if the set S of executions of the system under consideration is contained within P. This problem is at the core of widespread verification techniques, such as automata-theoretic model checking [START_REF] Vardi | Reasoning about infinite computations[END_REF], where systems are specified as finite-state automata and properties defined using Linear Temporal Logic [START_REF] Pnueli | The temporal logic of programs[END_REF]. However the bottleneck of this and other related verification techniques is the intractability of language inclusion (PSPACE-complete for finite-state automata over finite alphabets).

Alternation [START_REF] Chandra | [END_REF] was introduced as a generalization of nondeterminism, introducing universal, in addition to existential transitions. For automata over finite alphabets, the language inclusion problem can be encoded as the emptiness problem of an alternating automaton of linear size. Moreover, efficient exploration techniques based on antichains are shown to perform well for alternating automata over finite alphabets [START_REF] De Wulf | Antichains: Alternative algorithms for ltl satisfiability and model-checking[END_REF].

Using finite alphabets for the specification of properties and models is however very restrictive, when dealing with real-life computer systems, mostly because of the following reasons. On one hand, programs handle data from very large domains, that can be assumed to be infinite (64-bit integers, floating point numbers, strings of characters, etc.) and their correctness must be specified in terms of the data values. On the other hand, systems must respond to strict deadlines, which requires temporal specifications as timed languages [START_REF] Alur | A theory of timed automata[END_REF].

Although being convenient specification tools, automata over infinite alphabets lack the decidability properties ensured by finite alphabets. In general, when considering infinite data as part of the input alphabet, language inclusion is undecidable and, even complementation becomes impossible, for instance, for timed automata [START_REF] Alur | A theory of timed automata[END_REF] or finitememory register automata [START_REF] Kaminski | Finite-memory automata[END_REF]. One can recover theoretical decidability, by restricting the number of variables (clocks) in timed automata to one [START_REF] Ouaknine | On the language inclusion problem for timed automata: closing a decidability gap[END_REF], or forbidding relations between current and past/future values, as with symbolic automata [START_REF] Veanes | Symbolic finite state transducers: Algorithms and applications[END_REF]. In such cases, also the emptiness problem for the alternating versions becomes decidable [START_REF] Lasota | Alternating timed automata[END_REF][START_REF] D'antoni | A symbolic decision procedure for symbolic alternating finite automata[END_REF].

In this paper, we present a new model of alternating automata over infinite alphabets consisting of pairs (a, ν) where a is an input event from a finite set and ν is a valuation of a finite set x of variables that range over an infinite domain. We assume that, at all times, the successive values taken by the variables in x are an observable part of the language, in other words, there are no hidden variables in our model. The transition rules are specified by a set of formulae, in a combined first-order theory of Boolean control states and data, that relate past with present values of the variables. We do not fix the data theory a priori, but rather consider it to be a parameter of the class.

A run over an input word (a 1 , ν 1 ) . . . (a n , ν n ) is a sequence φ 0 (x 0 ) ⇒ φ 1 (x 0 , x 1 ) ⇒ . . . ⇒ φ n (x 0 , . . . , x n ) of rewritings of the initial formula by substituting Boolean states with time-stamped transition rules. The word is accepted if the final formula φ n (x 0 , . . . , x n ) holds, when all time-stamped variables x 1 , . . . , x n are substituted by their values in ν 1 , . . . , ν n , all non-final states replaced by false and all final states by true.

The Boolean operations of union, intersection and complement can be implemented in linear time in this model, thus matching the complexity of performing these operations in the finite-alphabet case. The price to be paid is that emptiness becomes undecidable, for which reason we provide two efficient semi-algorithms for emptiness, based on lazy predicate abstraction [START_REF] Henzinger | Lazy abstraction[END_REF] and the Impact method [START_REF] Mcmillan | Lazy abstraction with interpolants[END_REF]. These algorithms are proven to terminate and return a word from the language of the automaton, if one exists, but termination is not guaranteed when the language is empty.

We have implemented the Boolean operations and emptiness checking semi-algorithms and carried out experiments with examples taken from array logics [START_REF] Bozga | Automatic verification of integer array programs[END_REF], timed automata [START_REF] Henzinger | Symbolic model checking for realtime systems[END_REF], communication protocols [START_REF] Zbrzezny | Sat-based reachability checking for timed automata with discrete data[END_REF] and hardware verification [START_REF] Smrcka | Verifying parametrised hardware designs via counter automata[END_REF].

Related Work Data languages and automata have been defined previously, in a classical nondeterministic setting. For instance, Kaminski and Francez [START_REF] Kaminski | Finite-memory automata[END_REF] consider languages, over an infinite alphabet of data, recognized by automata with a finite number of registers, that store the input data and compare it using equality. Just as the timed languages recognized by timed automata [START_REF] Alur | A theory of timed automata[END_REF], these languages, called quasi-regular, are not closed under complement, but their emptiness is decidable. The impossibility of complementation here is caused by the use of hidden variables, which we do not allow. Emptiness is however undecidable in our case, mainly because counting (incrementing and comparing to a constant) data values is allowed, in many data theories.

Another related model is that of predicate automata [START_REF] Farzan | Proof spaces for unbounded parallelism[END_REF], which recognize languages over integer data by labeling the words with conjunctions of uninterpreted predicates.

We intend to explore further the connection with our model of alternating data automata, in order to apply our method to the verification of parallel programs.

The model presented in this paper stems from the language inclusion problem considered in [START_REF] Iosif | Abstraction refinement and antichains for trace inclusion of infinite state systems[END_REF]. There we provide a semi-algorithm for inclusion of data languages, based on an exponential determinization procedure and an abstraction refinement loop using lazy predicate abstraction [START_REF] Henzinger | Lazy abstraction[END_REF]. In this work we consider the full model of alternation and rely entirely on the ability of SMT solvers to produce interpolants in the combined theory of Booleans and data. Since determinisation is not needed and complementation is possible in linear time, the bulk of the work is carried out by the solver.

The emptiness check for alternating data automata adapts similar semi-algorithms for nondeterministic infinite-state programs to the alternating model of computation. In particular, we considered the state-of-the-art Impact procedure [START_REF] Mcmillan | Lazy abstraction with interpolants[END_REF] that is shown to outperform lazy predicate abstraction [START_REF] Henzinger | Lazy abstraction[END_REF] in the nondeterministic case, and generalized it to cope with alternation. More recent approaches for interpolant-based abstraction refinement target Horn systems [START_REF] Mcmillan | Lazy annotation revisited[END_REF][START_REF] Hoder | Generalized property directed reachability[END_REF], used to encode recursive and concurrent programs [START_REF] Grebenshchikov | Synthesizing software verifiers from proof rules[END_REF]. However, the emptiness of alternating word automata cannot be directly encoded using Horn clauses, because all the branches of the computation synchronize on the same input, which cannot be encoded by a finite number of local (equality) constraints. We believe that the lazy annotation techniques for Horn clauses are suited for branching computations, which we intend to consider in a future tree automata setting.

Preliminaries

A signature S = (S s , S f ) consists of a set S s of sort symbols and a set S f of sorted function symbols. To simplify the presentation, we assume w.l.o.g. that S s = {Data, Bool}1 and each function symbol f ∈ S f has #( f ) ≥ 0 arguments of sort Data and return value σ( f ) ∈ S s . If #( f ) = 0 then f is a constant. We consider constants and ⊥ of sort Bool.

Let Var be an infinite countable set of variables, where each x ∈ Var has an associated sort σ(x). A term t of sort σ(t) = S is a variable x ∈ Var where σ(x) = S , or f (t 1 , . . . , t #( f ) ) where t 1 , . . . , t #( f ) are terms of sort Data and σ( f ) = S . An atom is a term of sort Bool or an equality t ≈ s between two terms of sort Data. A formula is an existentially quantified combination of atoms using disjunction ∨, conjunction ∧ and negation ¬ and we write φ → ψ for ¬φ ∨ ψ.

We denote by FV σ (φ) the set of free variables of sort σ in φ and write FV(φ) for σ∈S s FV σ (φ). For a variable x ∈ FV(φ) and a term t such that σ(t) = σ(x), let φ[t/x] be the result of replacing each occurrence of x by t. For indexed sets t = {t 1 , . . . , t n } and x = {x 1 , . . . , x n }, we write φ[t/x] for the formula obtained by simultaneously replacing x i with t i in φ, for all i ∈ [1, n]. The size |φ| is the number of symbols occuring in φ.

An interpretation I maps (1) the sort Data into a non-empty set Data I , (2) the sort Bool into the set B = {true, false}, where I = true, ⊥ I = false, and (3) each function symbol f into a total function f I : (Data I ) #( f ) → σ( f ) I , or an element of σ( f ) I when #( f ) = 0. Given an interpretation I, a valuation ν maps each variable x ∈ Var into an element ν(x) ∈ σ(x) I . For a term t, we denote by t I ν the value obtained by replacing each function symbol f by its interpretation f I and each variable x by its valuation ν(x). For a formula φ, we write I, ν | = φ if the formula obtained by replacing each term t in φ by the value t I ν is logically equivalent to true. A formula φ is satisfiable in the interpretation I if there exists a valuation ν such that I, ν | = φ, and valid if I, ν | = φ for all valuations ν. The theory T(S, I) is the set of valid formulae written in the signature S, with the interpretation I. A decision procedure for T(S, I) is an algorithm that takes a formula φ in the signature S and returns yes iff φ ∈ T(S, I).

Given formulae ϕ and ψ, we say that φ entails ψ, denoted φ | = I ψ iff I, ν | = ϕ implies I, ν | = ψ, for each valuation ν, and φ ⇔ I ψ iff φ | = I ψ and ψ | = I φ. We omit mentioning the interpretation I when it is clear from the context.

Alternating Data Automata

In the rest of this section we fix an interpretation I and a finite alphabet Σ of input events. Given a finite set x ⊂ Var of variables of sort Data, let x → Data I be the set of valuations of the variables x and Σ[x] = Σ × (x → Data I ) be the set of data symbols. A data word (word in the sequel) is a finite sequence (a 1 , ν 1 )(a 2 , ν 2 ) . . . (a n , ν n ) of data symbols, where a 1 , . . . , a n ∈ Σ and ν 1 , . . . , ν n : x → Data I are valuations. We denote by ε the empty sequence, by Σ * the set of finite sequences of input events and by Σ[x] * the set of data words over x.

This definition generalizes the classical notion of words from a finite alphabet to the possibly infinite alphabet Σ[x]. Clearly, when Data I is sufficiently large or infinite, we can map the elements of Σ into designated elements of Data I and use a special variable to encode the input events. However, keeping Σ explicit in the following simplifies several technical points below, without cluttering the presentation.

Given sets of variables b, x ⊂ Var of sort Bool and Data, respectively, we denote by Form(b, x) the set of formulae φ such that FV Bool (φ) ⊆ b and FV Data (φ) ⊆ x. By Form + (b, x) we denote the set of formulae from Form(b, x) in which each Boolean variable occurs under an even number of negations.

An alternating data automaton (ADA or automaton in the sequel) is a tuple A = x, Q, ι, F, ∆ , where: -x ⊂ Var is a finite set of variables of sort Data, -Q ⊂ Var is a finite set of variables of sort Bool (states),

-ι ∈ Form + (Q, ∅) is the initial configuration, -F ⊆ Q is a set of final states, and -∆ : Q × Σ → Form + (Q, x ∪ x) is a transition function, where x denotes {x | x ∈ x}.
In each formula ∆(q, a) describing a transition rule, the variables x track the previous and x the current values of the variables of A. Observe that the initial values of the variables are left unconstrained, as the initial configuration does not contain free data variables. The size of A is defined as |A| = |ι| + (q,a)∈Q×Σ |∆(q, a)|.

Example Figure 1 (a) depicts an ADA with input alphabet Σ = {a, b}, variables x = {x, y}, states Q = {q 0 , q 1 , q 2 , q 3 , q 4 }, initial configuration q 0 , final states F = {q 3 , q 4 } and transitions given in Figure 1 (b), where missing rules, such as ∆(q 0 , b), are assumed to be ⊥. Rules ∆(q 0 , a) and ∆(q 1 , a) are universal and there are no existential nondeterministic

q 0 q 1 q 2 a x=0 ꓥ y=0 a x=& y+1 ꓥ y=& x+1 q 3 b & x≥& y q 4 a x>& x ꓥ y>& y b & x>& y (a) ∆(q 0 , a) ≡ q 1 ∧ q 2 ∧ x ≈ 0 ∧ y ≈ 0 ∆(q 1 , a) ≡ q 1 ∧ q 2 ∧ x ≈ y + 1 ∧ y ≈ x + 1 ∆(q 1 , b) ≡ q 3 ∧ x ≥ y ∆(q 2 , a) ≡ q 2 ∧ x > x ∧ y > y ∆(q 2 , b) ≡ q 4 ∧ x > y (b)
Fig. 1. Alternating Data Automaton Example rules. Rules ∆(q 1 , a) and ∆(q 2 , a) compare past (x, y) with present (x, y) values, ∆(q 0 , a) constrains the present and ∆(q 1 , b), ∆(q 2 , b) the past values, respectively.

Formally, let x k = {x k | x ∈ x}, for any k ≥ 0, be a set of time-stamped variables. For an input event a ∈ Σ and a formula φ, we write ∆(φ, a) (respectively ∆ k (φ, a)) for the formula obtained from φ by simultaneously replacing each state q ∈ FV Bool (φ) by the formula ∆(q, a) (respectively ∆(q, a)[x k /x, x k+1 /x], for k ≥ 0). Given a word w = (a 1 , ν 1 )(a 2 , ν 2 ) . . . (a n , ν n ), the run of A over w is the sequence of formulae:

φ 0 (Q) ⇒ φ 1 (Q, x 0 ∪ x 1 ) ⇒ . . . ⇒ φ n (Q, x 0 ∪ . . . ∪ x n ) where φ 0 ≡ ι and, for all k ∈ [1, n], we have φ k ≡ ∆ k (φ k-1 , a k ).
Next, we slightly abuse notation and write ∆(ι, a 1 , . . . , a n ) for the formula φ n (x 0 , . . . , x n ) above. We say that A accepts w iff I, ν | = ∆(ι, a 1 , . . . , a n ), for some valuation ν that maps: [START_REF] Alur | A theory of timed automata[END_REF]

each x ∈ x k to ν k (x), for all k ∈ [1, n], (2) each q ∈ FV Bool (φ n ) ∩ F to and (3) each q ∈ FV Bool (φ n ) \ F to ⊥. The language of A is the set L(A) of words from Σ[x] * accepted by A.
Example The following sequence is a non-accepting run of the ADA from Figure 1 on the word (a, 0, 0 ), (a, 1, 1 ), (b, 2, 1 ), where Data I = Z and the function symbols have standard arithmetic interpretation:

q 0 (a, 0,0 ) =⇒ q 1 ∧ q 2 ∧ x 1 ≈ 0 ∧ y 1 ≈ 0 (a, 1,1 ) =⇒ q 1 ∧ q 2 ∧ x 2 ≈ y 1 + 1 ∧ y 2 ≈ x 1 + 1 q 1 ∧ q 2 ∧ x 2 > x 1 ∧ y 2 > y 1 q 2 ∧ x 1 ≈ 0 ∧ y 1 ≈ 0 (b, 2,1 ) =⇒ q 3 ∧ x 2 ≥ y 2 q 1 ∧ q 4 ∧ x 2 > y 2 q 2 ∧x 2 ≈ y 1 + 1 ∧ y 2 ≈ x 1 + 1 ∧ q 4 ∧ x 2 > y 2 q 2 ∧x 2 > x 1 ∧ y 2 > y 1 ∧ x 1 ≈ 0 ∧ y 1 ≈ 0
In this paper we tackle the following problems: 1. Boolean closure: given automata A 1 and A 2 , both with the same set of variables

x, do there exist automata A ∪ , A ∩ and

A 1 such that L(A ∪ ) = A 1 ∪ A 2 , L(A ∩ ) = A 1 ∩ A 2 and L(A 1 ) = Σ[x] * \ L(A 1 ) ? 2. emptiness: given an automaton A, is L(A) = ∅ ?
It is well known that other problems, such as universality (given automaton A with variables x, does L(A) = Σ[x] * ?) and inclusion (given automata A 1 and A 2 with the same set of variables, does L(A 1 ) ⊆ L(A 2 )?) can be reduced to the above problems. Observe furthermore that we do not consider cases in which the sets of variables in the two automata differ. An interesting problem in this case would be: given automata A 1 and A 2 , with variables x 1 and x 2 , respectively, such that x 1 ⊆ x 2 , does L(A 1 ) ⊆ L(A 2 )↓ x 1 , where L(A 2 )↓ x 1 is the projection of the set of words L(A 2 ) onto the variables x 1 ? This problem is considered as future work.

Boolean Closure

Given a set Q of Boolean variables and a set x of variables of sort Data, for a formula φ ∈ Form + (Q, x), with no negated occurrences of the Boolean variables, we define the formula φ ∈ Form + (Q, x) recursively on the structure of φ:

φ 1 ∨ φ 2 ≡ φ 1 ∧ φ 2 φ 1 ∧ φ 2 ≡ φ 1 ∨ φ 2 ¬φ ≡ ¬φ if φ not atom φ ≡ φ if φ ∈ Q φ ≡ ¬φ if φ Q atom We have |φ| = |φ|, for every formula φ ∈ Form + (Q, x).
In the following let

A i = x, Q i , ι i , F i , ∆ i , for i = 1, 2
, where w.l.o.g. we assume that Q 1 ∩ Q 2 = ∅. We define:

A ∪ = x, Q 1 ∪ Q 2 , ι 1 ∨ ι 2 , F 1 ∪ F 2 , ∆ 1 ∪ ∆ 2 A ∩ = x, Q 1 ∪ Q 2 , ι 1 ∧ ι 2 , F 1 ∪ F 2 , ∆ 1 ∪ ∆ 2 A 1 = x, Q 1 , ι 1 , Q 1 \ F 1 , ∆ 1
where ∆ 1 (q, a) ≡ ∆ 1 (q, a), for all q ∈ Q 1 and a ∈ Σ. The following lemma shows the correctness of the above definitions:

Lemma 1. Given automata A i = x, Q i , ι i , F i , ∆ i , for i = 1, 2, such that Q 1 ∩ Q 2 = ∅, we have L(A ∪ ) = L(A 1 ) ∪ L(A 2 ), L(A ∩ ) = L(A 1 ) ∩ L(A 2 ) and L(A 1 ) = Σ[x] * \ L(A 1 ). It is easy to see that |A ∪ | = |A ∩ | = |A 1 | + |A 2 | and |A| = |A|,
thus the automata for the Boolean operations, including complementation, can be built in linear time. This matches the linear-time bounds for intersection and complementation of alternating automata over finite alphabets [START_REF] Chandra | [END_REF].

Antichains and Interpolants for Emptiness

The emptiness problem for ADA is undecidable, even in very simple cases. For instance, if Data I is the set of positive integers, an ADA can simulate an Alternating Vector Addition System with States (AVASS) using only atoms x ≥ k and x = x + k, for k ∈ Z, with the classical interpretation of the function symbols on integers. Since reachability of a control state is undecidable for AVASS [START_REF] Lincoln | Decision problems for propositional linear logic[END_REF], ADA emptiness is undecidable.

Consequently, we give up on the guarantee for termination and build semi-algorithms that meet the requirements below:

(i) given an automaton A, if L(A) ∅, the procedure will terminate and return a word w ∈ L(A), and (ii) if the procedure terminates without returning such a word, then L(A) = ∅.

Let us fix an automaton A = x, Q, ι, F, ∆ whose (finite) input event alphabet is Σ, for the rest of this section. Given a formula φ ∈ Form + (Q, x) and an input event a ∈ Σ, we define the post-image function Post A (φ, a) ≡ ∃x . ∆(φ[x/x], a) ∈ Form + (Q, x), mapping each formula in Form + (Q, x) to a formula defining the effect of reading the event a. We generalize the post-image function to finite sequences of input events, as follows:

Post A (φ, ε) ≡ φ Post A (φ, ua) ≡ Post A (Post A (φ, u), a) Acc A (u) ≡ Post A (ι, u) ∧ q∈Q\F (q → ⊥), for any u ∈ Σ *
Then the emptiness problem for A becomes: does there exist u ∈ Σ * such that the formula Acc A (u) is satisfiable? Observe that, since we ask a satisfiability query, the final states of A need not be constrained 2 . A naïve semi-algorithm enumerates all finite sequences and checks the satisfiability of Acc A (u) for each u ∈ Σ * , using a decision procedure for the theory T(S, I).

Since no Boolean variable from Q occurs under negation in φ, it is easy to prove the following monotonicity property: given two formulae φ, ψ

∈ Form + (Q, x) if φ | = ψ then Post A (φ, u) | = Post A (ψ, u), for any u ∈ Σ * .
This suggest an improvement of the above semi-algorithm, that enumerates and stores only a set U ⊆ Σ * for which {Post A (φ, u) | u ∈ U} forms an antichain3 w.r.t. the entailment partial order. This is because, for any

u, v ∈ Σ * , if Post A (ι, u) | = Post A (ι, v) and Acc A (uw) is satisfiable for some w ∈ Σ * , then Post A (ι, uw) | = Post A (ι, vw), thus Acc A (vw) is satisfiable as well,
and there is no need for u, since the non-emptiness of A can be proved using v alone. However, even with this optimization, the enumeration of sequences from Σ * diverges in many real cases, because infinite antichains exist in many interpretations, e.g. q ∧ x ≈ 0, q ∧ x ≈ 1, . . . for Data I = N.

A safety invariant for A is a function I : (Q → B) → 2 x →Data I such that, for every Boolean valuation β : Q → B, every valuation ν : x → Data I of the data variables and every finite sequence u ∈ Σ * of input events, the following hold:

1.

I, β ∪ ν | = Post A (ι, u) ⇒ ν ∈ I(β), and 2. ν ∈ I(β) ⇒ I, β ∪ ν | = Acc A (u)
. If I satisfies only the first point above, we call it an invariant. Intuitively, a safety invariant maps every Boolean valuation into a set of data valuations, that contains the initial configuration ι ≡ Post A (ι, ε), whose data variables are unconstrained, overapproximates the set of reachable valuations (point 1) and excludes the valuations satisfying the acceptance condition (point 2). A formula φ(Q, x) is said to define I iff for all β : Q → B and ν : x → Data I , we have I,

β ∪ ν | = φ iff ν ∈ I(β).
Lemma 2. For any automaton A, we have L(A) = ∅ if and only if A has a safety invariant.

Turning back to the issue of divergence of language emptiness semi-algorithms in the case L(A) = ∅, we can observe that an enumeration of input sequences u 1 , u 2 , . . . ∈ Σ * can stop at step k as soon as k i=1 Post A (ι, u i ) defines a safety invariant for A. Although this condition can be effectively checked using a decision procedure for the theory T(S, I), there is no guarantee that this check will ever succeed.

The solution we adopt in the sequel is abstraction to ensure the termination of invariant computations. However, it is worth pointing out from the start that abstraction alone will only allow us to build invariants that are not necessarily safety invariants. To meet the latter condition, we resort to counterexample guided abstraction refinement (CEGAR).

Formally, we fix a set of formulae Π ⊆ Form(Q, x), such that ⊥ ∈ Π and refer to these formulae as predicates. Given a formula φ, we denote by φ ≡ {π ∈ Π | φ | = π} the abstraction of φ w.r.t. the predicates in Π. The abstract versions of the post-image and acceptance condition are defined as follows:

Post A (φ, ε) ≡ φ Post A (φ, ua) ≡ (Post A (Post A (φ, u), a)) Acc A (u) ≡ Post A (ι, u) ∧ q∈Q\F (q → ⊥), for any u ∈ Σ * Lemma 3.
For any bijection µ : N → Σ * , there exists k > 0 such that k i=0 Post A (ι, µ(i)) defines an invariant I for A.

We are left with fulfilling point (2) from the definition of a safety invariant. To this end, suppose that, for a given set Π of predicates, the invariant I , defined by the previous lemma, meets point (1) but not point [START_REF] Bozga | Automatic verification of integer array programs[END_REF], where Post A and Acc A replace Post A and Acc A , respectively. In other words, there exists a finite sequence u ∈ Σ * such that ν ∈ I (β) and I, β∪ν | = Acc A (u), for some Boolean β : Q → B and data ν : x → Data I valuations. Such a u ∈ Σ * is called a counterexample.

Once a counterexample u is discovered, there are two possibilities. Either (i) Acc A (u) is satisfiable, in which case u is feasible and L(A) ∅, or (ii) Acc A (u) is unsatisfiable, in which case u is spurious. In the first case, our semi-algorithm stops and returns a witness for non-emptiness, obtained from the satisfying valuation of Acc A (u) and in the second case, we must strenghten the invariant by excluding from I all pairs (β, ν) such that I, β ∪ ν | = Acc A (u). This strenghtening is carried out by adding to Π several predicates that are sufficient to exclude the spurious counterexample.

Given an unsatisfiable conjunction of formulae ψ 1 ∧ . . . ∧ ψ n , an interpolant is a tuple of formulae I 1 , . . . , I n-1 , I n such that I n ≡ ⊥, I i ∧ ψ i | = T I i+1 and I i contains only variables and function symbols that are common to ψ i and ψ i+1 , for all i ∈ [n -1]. Moreover, by Lyndon's Interpolation Theorem [START_REF] Lyndon | An interpolation theorem in the predicate calculus[END_REF], we can assume without loss of generality that every Boolean variable with at least one positive (negative) occurrence in I i has at least one positive (negative) occurrence in both ψ i and ψ i+1 . In the following, we shall assume the existence of an interpolating decision procedure for T(S, I) that meets the requirements of Lyndon's Interpolation Theorem.

A classical method for abstraction refinement is to add the elements of the interpolant obtained from a proof of spuriousness to the set of predicates. This guarantees progress, meaning that the particular spurious counterexample, from which the interpolant was generated, will never be revisited in the future. Though not always, in many practical test cases this progress property eventually yields a safety invariant.

Given a non-empty spurious counterexample u = a 1 . . . a n , where n > 0, we consider the following interpolation problem:

Θ(u) ≡ θ 0 (Q 0 ) ∧ θ 1 (Q 0 ∪ Q 1 , x 0 ∪ x 1 ) ∧ . . . (1) ∧ θ n (Q n-1 ∪ Q n , x n-1 ∪ x n ) ∧ θ n+1 (Q n ) where Q k = {q k | q ∈ Q}, k ∈ [0, n] are time-stamped sets of Boolean variables corre- sponding to the set Q of states of A. The first conjunct θ 0 (Q 0 ) ≡ ι[Q 0 /Q]
is the initial configuration of A, with every q ∈ FV Bool (ι) replaced by q 0 . The definition of θ k , for all k ∈ [1, n], uses replacement sets R ⊆ Q , ∈ [0, n], which are defined inductively below:

-

R 0 = FV Bool (θ 0 ), -θ ≡ q -1 ∈R -1 (q -1 → ∆(q, a )[Q /Q, x -1 /x, x /x]) and R = FV Bool (θ ) ∩ Q , for each ∈ [1, n]. -θ n+1 (Q n ) ≡ q∈Q\F (q n → ⊥).
The intuition is that R 0 , . . . , R n are the sets of states replaced, θ 0 , . . . , θ n are the sets of transition rules fired on the run of A over u and θ n+1 is the acceptance condition, which forces the last remaining non-final states to be false. We recall that a run of A over u is a sequence:

φ 0 (Q) ⇒ φ 1 (Q, x 0 ∪ x 1 ) ⇒ . . . ⇒ φ n (Q, x 0 ∪ . . . ∪ x n )
where φ 0 is the initial configuration ι and for each k > 0, φ k is obtained from φ k-1 by replacing each state q ∈ FV Bool (φ k-1 ) by the formula ∆(q, a k )[x k-1 /x, x k /x], given by the transition function of A. Observe that, because the states are replaced with transition formulae when moving one step in a run, these formulae lose track of the control history and are not suitable for producing interpolants that relate states and data.

The main idea behind the above definition of the interpolation problem is that we would like to obtain an interpolant , I 0 (Q), I 1 (Q, x), . . . , I n (Q, x), ⊥ whose formulae combine states with the data constraints that must hold locally, whenever the control reaches a certain Boolean configuration. This association of states with data valuations is tantamount to defining efficient semi-algorithms, based on lazy abstraction [START_REF] Henzinger | Lazy abstraction[END_REF]. Furthermore, the abstraction defined by the interpolants generated in this way can also over-approximate the control structure of an automaton, in addition to the sets of data values encountered throughout its runs.

The correctness of this interpolation-based abstraction refinement setup is captured by the progress property below, which guarantees that adding the formulae of an interpolant for Θ(u) to the set Π of predicates suffices to exclude the spurious counterexample u from future searches. Lemma 4. For any sequence u = a 1 . . . a n ∈ Σ * , if Acc A (u) is unsatisfiable, the following hold:

1. Θ(u) is unsatisfiable, and 2. if , I 0 , . . . , I n , ⊥ is an interpolant for Θ(u) such that

{I i | i ∈ [0, n]} ⊆ Π then Acc A (u) is unsatisfiable.

Lazy Predicate Abstraction for ADA Emptiness

We have now all the ingredients to describe the first emptiness checking semi-algorithm for alternating data automata. Algorithm 4 1 builds an abstract reachability tree (ART) whose nodes are labeled with formulae over-approximating the concrete sets of configurations, and a covering relation between nodes in order to ensure that the set of formulae labeling the nodes in the ART forms an antichain. Any spurious counterexample is eliminated by computing an interpolant and adding its formulae to the set of predicates (cf. Lemma 4). Formally, an ART is tuple T = N, E, r, Λ, R, T, , where:

-N is a set of nodes, -E ⊆ N × Σ × N is a set of edges, -r ∈ N is the root of the directed tree (N, E), -Λ : N → Form(Q, x
) is a labeling of the nodes with formulae, such that

Λ(r) = ι, -R : N → 2 Q is a labeling of nodes with replacement sets, such that R(r) = FV Bool (ι), -T : E → ∞ i=0 Form + (Q i , x i , Q i+1 , x i+1
) is a labeling of edges with time-stamped formulae, and -⊆ N × N is a set of covering edges.

Each node n ∈ N corresponds to a unique path from the root to n, labeled by a sequence λ(n) ∈ Σ * of input events. The least infeasible suffix of λ(n) is the smallest sequence v = a 1 . . . a k , such that λ(n) = wv, for some w ∈ Σ * and the following formula is unsatisfiable:

Ψ (v) ≡ Λ(p)[Q 0 /Q] ∧ θ 1 (Q 0 ∪ Q 1 , x 0 ∪ x 1 ) ∧ . . . ∧ θ k+1 (Q k ) (2)
where θ 1 , . . . , θ k+1 are defined as in [START_REF] Alur | A theory of timed automata[END_REF] and

θ 0 ≡ Λ(p)[Q 0 /Q].
The pivot of n is the node p corresponding to the start of the least infeasible suffix. We assume the existence of two functions FindPivot(u, T ) and LeastInfeasibleSuffix(u, T ) that return the pivot and least infeasbile suffix of a sequence u ∈ Σ * in an ART T , without detailing their implementation. With these considerations, Algorithm 1 uses a worklist iteration to build an ART. We keep newly expanded nodes of T in a queue WorkList, thus implementing a breadthfirst exploration strategy, which guarantees that the shortest counterexamples are explored first. When the search encounters a counterexample candidate u, it is checked for spuriousness. If the counterexample is feasible, the procedure returns a data word w ∈ L(A), which interleaves the input events of u with the data valuations from the model of Acc A (u) (since u is feasible, clearly Acc A (u) is satisfiable). Otherwise, u is spurious and we compute its pivot p (line 12), add the interpolants for the least unfeasible suffix of u to Π, remove and recompute the subtree of T rooted at p.

Termination of Algorithm 1 depends on the ability of a given interpolating decision procedure for the combined Boolean and data theory T(S, I) to provide interpolants that yield a safety invariant, whenever L(A) = ∅. In this case, we use the covering relation to ensure that, when a newly generated node is covered by a node already in N, it is not added to the worklist, thus cutting the current branch of the search.

if Post A (λ(n)) is satisfiable then counterexample candidate 8: if Acc A (u) is satisfiable then feasible counterexample 9: get model (β, ν 1 , . . . , ν k ) of Acc A (λ(n))
10:

return w = (a 1 , ν 1 ) . . . (a k , ν k ) w ∈ L(A)
p ← FindPivot(λ(n), T ) 13: v ← LeastInfeasibleSuffix(λ(n), T )
14:

Π ← Π ∪ {I 0 , . . . , I }, where , I 0 , . . . , I , ⊥ is an interpolant for Ψ (v)

15:

let S = N , E , p, Λ , be the subtree of T rooted at p

16:

for (m, q) ∈ such that q ∈ N do for a ∈ Σ do expand n

22:

φ ← Post A (Λ(n), a)
23:

if exist m ∈ N such that φ | = Λ(m) then 24: ← ∪ {(n, m)} m covers n

25:

else 26:

let s be a fresh node 27:

E ← E ∪ {(n, a, s)} 28: Λ ← Λ ∪ {(s, φ)} 29: R ← {m ∈ WorkList | Λ(m) | = φ}
worklist nodes covered by s 30:

for r ∈ R do 31:

for m ∈ N such that (m, b, r) ∈ E, b ∈ Σ do 32: ← ∪ {(m, s)} redirect covered children from R into s

33:

for (m, r) ∈ do

34:

← ∪ {(m, s)} redirect covered nodes from R into s

35:

remove R from T

36:

enqueue s into WorkList

37: return true

Example Consider the automaton given in Figure 1. First, Algorithm 1 fires the sequence a, and since there are no other formulae than ⊥ in Π, the successor of ι ≡ q 0 is , in Figure 2 (a). The spuriousness check for a yields the root of the ART as pivot and the interpolant q 0 , q 1 , which is added to the set Π. Then the node is removed and the next time a is fired, it creates a node labeled q 1 . The second sequence aa creates a successor node q 1 , which is covered by the first, depicted with a dashed arrow, in Figure 2 (b). The third sequence is ab, which results in a new uncovered node and triggers a spuriousness check. The new predicate obtained from this check is x ≤ 0 ∧ q 2 ∧ y ≥ 0 and the pivot is again the root. Then the entire ART is rebuilt with the new predicates and the fourth sequence aab yields an uncovered node , in Figure 2 (c). The new pivot is the endpoint of a and the newly added predicates are q 1 ∧ q 2 and y > x -1 ∧ q 2 . Finally, the ART is rebuilt from the pivot node and finally all nodes are covered, thus proving the emptiness of the automaton, in Figure 2 (d).

The correctness of Algorithm 1 is proved below: Theorem 1. Given an automaton A, such that L(A) ∅, Algorithm 1 terminates and returns a word w ∈ L(A). If Algorithm 1 terminates reporting true, then L(A) = ∅.

q 0 Π={⊥} ⊤ a add predicates {q 0 ,q 1 } pivot q 0 Π={⊥,q 0 ,q 1 } ⊤ a add predicates {x≤0ꓥq 2 ꓥy≥0} pivot q 1 q 1 a b (a) (b) q 0 Π={⊥,q 0 ,q 1 ,x≤0ꓥq 2 ꓥy≥0} a add predicates {q 1 ꓥq 2 ,y>x-1ꓥq 2 } pivot q 1 ꓥx≤0ꓥq 2 ꓥy≥0 q 1 a q 1 a ⊤ b ⊥ b q 0 Π={⊥,q 0 ,q 1 ,x≤0ꓥq 2 ꓥy≥0,q 1 ꓥq 2 ,y>x-1ꓥq 2 } a q 1 ꓥx≤0ꓥq 2 ꓥy≥0 a b q 1 ꓥq 2 ꓥy>x-1 a ⊥ q 1 ꓥq 2 ꓥy>x-1 ⊥ b (c) (d)

Checking ADA Emptiness with Impact

As pointed out by a number of authors, the bottleneck of predicate abstraction is the high cost of reconstructing parts of the ART, subsequent to the refinement of the set of predicates. The main idea of the Impact procedure [START_REF] Mcmillan | Lazy abstraction with interpolants[END_REF] is that this can be avoided and the refinement (strenghtening of the node labels of the ART) can be performed inplace. This refinement step requires an update of the covering relation, because a node that used to cover another node might not cover it after the strenghtening of its label. We consider a total alphabetical order ≺ on Σ and lift it to the total lexicographical order ≺ * on Σ * . A node n ∈ N is covered if (n, p) ∈ or it has an ancestor m such that (m, p) ∈ , for some p ∈ N.

A node n is closed if it is covered, or Λ(n) | = Λ(m) for all m ∈ N such that λ(m) ≺ * λ(n).
Observe that we use the coverage relation here with a different meaning than in Algorithm 1.

The execution of Algorithm 2 consists of three phases5 : close, refine and expand. Let n be a node removed from the worklist at line 4. If Acc A (λ(n)) is satisfiable, the counterexample λ(n) is feasible, in which case a model of Acc A (λ(n)) is obtained and a word w ∈ L(A) is returned. Otherwise, λ(n) is a spurious counterexample and the procedure enters the refinement phase (lines 11-18). The interpolant for Θ(λ(n)) (cf. formula 1) is used to strenghten the labels of all the ancestors of n, by conjoining the formulae of the interpolant to the existing labels.

In this process, the nodes on the path between r and n, including n, might become eligible for coverage, therefore we attempt to close each ancestor of n that is impacted by the refinement (line 18). Observe that, in this case the call to Close must uncover for i = 0, . . . , k do 14:

if Λ(n i ) | = I i then 15: ← \ {(m, n i ) ∈ | m ∈ N} 16: Λ(n i ) ← Λ(n i ) ∧ I i strenghten the label of n i 17: if ¬b then 18: b ← Close(n i )
19:

if n is not covered then 20:

for a ∈ Σ do expand n

21:

let s be a fresh node and e = (n, a, s) be a new edge

22:

E ← E ∪ {e}

23:

Λ ← Λ ∪ {(s, )}

24:

T ← T ∪ {(e, θ k )}

25:

R ← R ∪ {(s, q∈R(n) FV Bool (∆(q, a)))}

26:

enqueue s into WorkList 27: return true 1: function Close(x) returns Bool 2:

for y ∈ N such that λ(y) ≺ * λ(x) do

3:

if Λ(x) | = Λ(y) then

4:

← ( \ {(p, q) ∈ | q is x or a successor of x}) ∪ {(x, y)}

5:

return true

6:

return false each node which is covered by a successor of n (line 4 of the Close function). This is required because, due to the over-approximation of the sets of reachable configurations, the covering relation is not transitive, as explained in [START_REF] Mcmillan | Lazy abstraction with interpolants[END_REF]. If Close adds a covering edge (n i , m) to , it does not have to be called for the successors of n i on this path, which is handled via the Boolean flag b.

Finally, if n is still uncovered (it has not been previously covered during the refinement phase) we expand n (lines 20-26) by creating a new node for each successor s via the input event a ∈ Σ and inserting it into the worklist. Example We show the execution of Algorithm 2 on the automaton from Figure 1. Initially, the procedure fires the sequence a, whose endpoint is labeled with , in Figure 3 (a). Since this node is uncovered, we check the spuriousness of the counterexample a and refine the label of the node to q 1 . Since the node is still uncovered, two successors, labeled with are computed, corresponding to the sequences aa and ab, in Figure 3 (b). The spuriousness check for aa yields the interpolant q 0 , x ≤ 0 ∧ q 2 ∧ y ≥ 0 which strenghtens the label of the endpoint of a from q 1 to q 1 ∧ x ≤ 0∧q 2 ∧y ≥ 0. The sequence ab is also found to be spurious, which changes the label of its endpoint from to ⊥, and also covers it (depicted with a dashed edge). Since the endpoint of aa is not covered, it is expanded to aaa and aab, in Figure 3 (c). Both sequences aaa and aab are found to be q 0 R={q 0 } a ⊤ R={q 1 ,q 2 } q 0

[0] →q 1 [1] ꓥq 2 [1] ꓥx [1] =0ꓥy [1] =0 refined q 1

(a)

q 0 R={q 0 } a q 1 R={q 1 ,q 2 } q 0

[0] →q 1 [1] ꓥq 2 [1] ꓥx [1] =0ꓥy [1] =0 refined ⊥ ⊤ R={q 1 ,q 2 } a (q 1 [1] →q 3 [2] ꓥx [1] ≥y [1] ) ꓥ (q 2 [1] →q 4 [2] ꓥx [1] >y [1] ) ⊤ R={q 3 ,q 4 } b refined q 1 refined q 1 ꓥx≤0ꓥq 2 ꓥy≥0 (q 1 [1] →q 1 [2] ꓥq 2 [2] ꓥ x [2] =y [1] +1ꓥy [2] =x [1] +1) ꓥ (q 2 [1] →q 2 [2] ꓥ x [2] >x [1] ꓥy [2] >y [1] )

(b) q 0 R={q 0 } a q 1 ꓥx≤0ꓥq 2 ꓥy≥0
R={q 1 ,q 2 } q 0

[0] →q 1 [1] ꓥq 2 [1] ꓥx [1] =0ꓥy [1] =0 (q 1 [1] →q 1 [2] ꓥq 2 [2] ꓥ x [2] =y [1] +1ꓥy [2] =x [1] +1) ꓥ (q 2 [1] →q 2 [2] ꓥ x [2] >x [1] ꓥy [2] >y [1] ) q 1 R={q 1 ,q 2 } a (q 1 [1] →q 3 [2] ꓥx [1] ≥y [1] ) ꓥ (q 2 [1] →q 4 [2] ꓥx [1] >y [1] ) ⊥ R={q 3 ,q 4 } b ⊤ R={q 3 ,q 4 } ⊤ R={q 1 ,q 2 } b (q 1 [2] →q 3 [3] ꓥx [2] ≥y [2] ) ꓥ (q 2 [2] →q 4 [3] ꓥx [2] >y [2] ) a (q 1 [2] →q 1 [3] ꓥq 2 [3] ꓥx [3] =y [2] +1ꓥy [3] =x [2] +1) ꓥ (q 2 [2] →q 2 [3] ꓥx [3] >x [2] ꓥy [3] >y [2] ) refined q 1 ꓥy>x-1ꓥq 2 refined ⊥ refined q 1

(c) q 0 R={q 0 } a q 1 ꓥx≤0ꓥq 2 ꓥy≥0 R={q 1 ,q 2 } q 0

[0] →q 1 [1] ꓥq 2 [1] ꓥx [1] =0ꓥy [1] =0 (q 1 [1] →q 1 [2] ꓥq 2 [2] ꓥ x [2] =y [1] +1ꓥy [2] =x [1] +1) ꓥ (q 2 [1] →q 2 [2] ꓥ x [2] >x [1] ꓥy [2] >y [1] ) q 1 ꓥy>x-1ꓥq 2 R={q 1 ,q 2 } a (q 1 [1] →q 3 [2] ꓥx [1] ≥y [1] ) ꓥ (q 2 [1] →q 4 [2] ꓥx [1] >y [1] ) ⊥ R={q 3 ,q 4 } b ⊥ R={q 3 ,q 4 } q 1 R={q 1 ,q 2 } b (q 1 [2] →q 3 [3] ꓥx [2] ≥y [2] ) ꓥ (q 2 [2] →q 4 [3] ꓥx [2] >y [2] ) a (q 1 [2] →q 1 [3] ꓥq 2 [START_REF] Chandra | [END_REF] ꓥx [3] =y [2] +1ꓥy [3] =x [2] +1) ꓥ (q 2 [2] →q 2 [START_REF] Chandra | [END_REF] ꓥx [3] >x [2] ꓥy [3] >y [2] ) ⊤ R={q 3 ,q 4 } ⊤ R={q 1 ,q 2 } (q 1 [3] →q 1 [4] ꓥq 2 [4] ꓥx [4] =y [3] +1ꓥy [4] =x [3] +1) ꓥ (q 2 [3] →q 2 [4] ꓥx [4] >x [3] ꓥy [4] >y [3] ) b a (q 1 [3] →q 3 [4] ꓥx [3] ≥y [3] ) ꓥ (q 2 [3] →q 4 [4] ꓥx [3] >y [3] ) refined ⊥ refined q 1 refined q 1 ꓥy>x-1ꓥq 2 spurious, and the enpoint of aab, whose label has changed from to ⊥, is now covered. In the process, the label of aa has also changed from q 1 to q 1 ∧ y > x -1 ∧ q 2 , due to the strenghtening with the interpolant from aab. Finally, the only uncovered node aaa is expanded to aaaa and aaab, both found to be spurious, in Figure 3 (d). The refinement of aaab causes the label of aaa to change from q 1 to q 1 ∧ y > x -1 ∧ q 2 and this node is now covered by aa. Since its successors are also covered, there are no uncovered nodes and the procedure returns true.

The correctness of Algorithm 2 is coined by the theorem below: Theorem 2. Given an automaton A, such that L(A) ∅, Algorithm 2 terminates and returns a word w ∈ L(A). If Algorithm 2 terminates reporting true, then L(A) = ∅.

Experimental Evaluation

We have implemented both Algorithm 1 and 2 in a prototype tool 6 that uses the Math-SAT5 SMT solver7 via the Java SMT interface 8 for the satisfiability queries and interpolant generation, in the theory of linear integer arithmetic with uninterpreted Boolean functions (UFLIA). We compared both algorithms with a previous implementation of a trace inclusion procedure, called Includer9 , that uses on-the-fly determinisation and lazy predicate abstraction with interpolant-based refinement [START_REF] Iosif | Abstraction refinement and antichains for trace inclusion of infinite state systems[END_REF] in the LIA theory.

The results of the experiments are given in Table 1. We applied the tool first to several array logic entailments, which occur as verification conditions for imperative programs with arrays [START_REF] Bozga | Automatic verification of integer array programs[END_REF] (array shift, array simple, array rotation1+2) available online [START_REF]Numerical Transition Systems Repository[END_REF]. Next, we applied it on proving safety properties of hardware circuits (hw1+2) [START_REF] Smrcka | Verifying parametrised hardware designs via counter automata[END_REF]. Finally, we considered two timed communication protocols, consisting of systems that are asynchronous compositions of timed automata, whom correctness specifications are given by timed automata monitors: a timed version of the Alternating Bit Protocol (abp) [START_REF] Zbrzezny | Sat-based reachability checking for timed automata with discrete data[END_REF] and a controller of a railroad crossing (train) [START_REF] Henzinger | Symbolic model checking for realtime systems[END_REF]. All results were obtained on x86 64 Linux Ubuntu virtual machine with 8GB of RAM running on an Intel(R) Xeon(R) CPU E5-2683 v3 @ 2.00GHz. The automata sizes are given in bytes needed to store their ASCII description on file and the execution times are in seconds. As in the case of non-alternating nondeterministic integer programs [START_REF] Mcmillan | Lazy abstraction with interpolants[END_REF], the alternating version of Impact (Algorithm 2) outperforms lazy predicate abstraction for checking emptiness by at least one order of magnitude. Moreover, Impact is comparable, on average, to the previous implementation of Includer, which uses also MathSAT5 via the C API. We believe the reason for which Includer outperforms Impact on some examples is the hardness of the UFLIA entailment checks used in Algorithm 2 (line 14 and line 3 in the function Close) as opposed to the pure LIA entailment checks used in Includer. According to our statistics, Algorithm 2 spends more than 50% of the time waiting for the SMT solver to finish answering entailment queries.

Proof of Lemma 1

Proposition 1. Given a formula φ ∈ Form + (Q, x) and a valuation ν mapping each q ∈ Q to a value ν(q) ∈ B and each x ∈ x to a value ν(x) ∈ Data I , let ν be the valuation that assigns each q ∈ Q the value ¬ν(q) and each x ∈ x the value ν(x). Then we have I, ν | = φ if and only if I, ν | = φ.

Proof. Immediate, by induction on the structure of φ.

Proof. We prove L(A ∪ ) = L(A 1 ) ∪ L(A 2 ) first, the proof for A ∩ being analogous. Let w = (a 1 , ν 1 ) . . . (a n , ν n ) be a word, where n = 0 corresponds to the empty word. We prove by induction on n ≥ 0 that ∆(ι 1 ∨ ι 2 , a 1 . . . a n ) ⇔ ∆(ι 1 , a 1 . . . a n ) ∨ ∆(ι 2 , a 1 . . . a n ). The case n = 0 follows from the definition of the initial configuration of A ∪ . For the inductive step n > 0, ∆(ι 1 ∨ ι 2 , a 1 . . . a n ) is obtained from ∆(ι 1 ∨ ι 2 , a 1 . . . a n-1 ) by replacing each variable q ∈ FV Bool (∆(ι 1 ∨ ι 2 , a 1 . . . a n-1 )) with ∆(q, a n )[x n-1 /x, x n /x], denoted ∆ n (∆(ι 1 ∨ι 2 , a 1 . . . a n-1 ), a n ). Since by induction hypothesis, ∆(ι 1 ∨ι 2 , a 1 . . . a n-1 ) ⇔ ∆(ι 1 , a 1 . . . a n-1 ) ∨ ∆(ι 2 , a 1 . . . a n-1 ), we obtain:

∆ n (∆(ι 1 ∨ ι 2 , a 1 . . . a n-1 ), a n ) ⇔ ∆ n (∆(ι 1 , a 1 . . . a n-1 ), a n ) ∨ ∆ n (∆(ι 2 , a 1 . . . a n-1 ), a n ) ⇔ ∆(ι 1 , a 1 . . . a n ) ∨ ∆(ι 2 , a 1 . . . a n ) .

To prove L(A 1 ) = Σ[x] * \ L(A 1 ), let w = (a 1 , ν 1 ) . . . (a n , ν n ) be a word and show that ∆(ι 1 , a 1 . . . a n ) = ∆(ι 1 , a 1 . . . a n ) by induction on n ≥ 0. The case n = 0 is immediate, because FV(ι 1 ) ⊆ Q and thus ι 1 ≡ ι 1 . For the case n > 0, we compute: ∆(ι 1 , a 1 . . . a n ) = ∆(ι 1 , a 1 . . . a n ) by induction on n ≥ 0.

In the case n = 0, we have ∆(ι 1 , a 1 . . . a n ) ≡ ι 1 . Then ε is accepted by A 1 iff ν 0 | = ι 1 , where ν 0 (q) = if q ∈ F 1 and ν 0 (q) = ⊥, otherwise. But ν 0 | = ι 1 iff ν 0 | = ι 1 , where ν 0 (q) = if q F 1 and ν 0 (q) = ⊥, otherwise. Thus ε is accepted by A 1 iff it is not accepted by A 1 .

For the case n > 0, we compute:

∆ n (∆(ι 1 , a 1 . . . a n-1 ), a n ) ⇔ (by ind. hyp.)

∆ n (∆(ι 1 , a 1 . . . a n-1 ), a n ) ⇔ (by the def. of φ) ∆(ι 1 , a 1 . . . , a n ) .

Let ν, ν : (Q ∪ n i=0 x i ) → (B ∪ Data I ) be valuations such that: -ν(q) = and ν (q) = ⊥, for each q ∈ F, -ν(q) = ⊥ and ν (q) = , for each q ∈ Q \ F, -ν(x) = ν (x), for each x ∈ x 0 , -ν(x) = ν (x) = ν i (x), for each x ∈ x i and each i ∈

Algorithm 1

 1 Formally, for any two nodes n, m ∈ N, we have n m iff Post A (Λ(n), a) | = Λ(m) for some a ∈ Σ, in other words, if n has a successor whose label entails the label of m. Lazy Predicate Abstraction for ADA Emptiness input: an ADA A = x, Q, ι, F, ∆ over the alphabet Σ of input events output: true if L(A) = ∅ and a data word w ∈ L(A) otherwise 1: let T = N, E, r, Λ, be an ART 2: initially N = E = = ∅, Λ = {(r, ι)}, Π = {⊥}, WorkList = r , 3: while WorkList ∅ do 4: dequeue n from WorkList 5: N ← N ∪ {n} 6: let λ(n) = a 1 . . . a k be the label of the path from r to n 7:

17 :

 17 remove m from N and enqueue m into WorkList 18: remove S from T 19: enqueue p into WorkList recompute the subtree rooted at p 20: else 21:

Fig. 2 .

 2 Fig. 2. Proving Emptiness of the Automaton from Fig. 1 by Algorithm 1

Algorithm 2 7 : 9 :

 279 Impact for ADA Emptiness input: an ADA A = x, Q, ι, F, ∆ over the alphabet Σ of input events output: true if L(A) = ∅ and a data word w ∈ L(A) otherwise1: let T = N, E, r, Λ, R, T, be an ART 2: initially N = E = T = = ∅, Λ = {(r, ι)}, R = FV Bool (ι[Q 0 /Q]), WorkList = {r} 3: while WorkList ∅ do 4, a 1 , n 1 ), (n 1 , a 2 , n 2 ), . . . , (n k-1 , a k , n) be the path from r to n if Acc A (a 1 . . . a k ) is satisfiable then counterexample is feasible 8: get model (β, ν 1 , . . . , ν k ) of Acc A (λ(n))return w = (a 1 , ν 1 ) . . . (a k , ν k ) w ∈ L(A) , I 0 , . . . , I k , ⊥ be an interpolant for Θ(a 1 . . . a k )

Fig. 3 .

 3 Fig. 3. Proving Emptiness of the Automaton from Fig. 1 by Algorithm 2

  [1, n]. By Proposition 1, we haveI, ν | = ∆(ι 1 , a 1 . . . a n ) ⇐⇒ I, ν | = ∆(ι 1 , a 1 . . . a n ) ⇐⇒ I, ν | = ∆(ι 1 , a 1 . . . a n ). Thus for all w ∈ Σ[x] * , we have w ∈ L(A 1 ) ⇐⇒ w L(A 1 ). Proof of Lemma 2 Proof. Let A = x, Q, ι, F, ∆ in the following. "⇐" This direction is trivial. "⇒" We define I : (Q → B) → 2 x →Data I as follows. For each β : Q → B, let I(β) = {ν : x → Data I | ∃u ∈ Σ * . β∪ν | = Post A (ι, u)}.Checking that I is a safety invariant is straightforward.

Table 1 .

 1

	sec)

Example

|A| (bytes) L(A) = ∅ ? Algorithm 1 (sec) Algorithm 2 (sec) Includer (

The generalization to more than two sorts is without difficulty, but would unnecessarily clutter the technical presentation.

Since each state occurs positively in Acc A (u), this formula has a model iff it has a model with every q ∈ F set to true.

Given a partial order (D, ) an antichain is a set A ⊆ D such that a b for any a, b ∈ A.

Though termination is not guaranteed, we call it algorithm for conciseness.

Corresponding to the Close, Refine and Expand in[START_REF] Mcmillan | Lazy abstraction with interpolants[END_REF].

The implementation is available at https://github.com/cathiec/JAltImpact

http://mathsat.fbk.eu/

https://github.com/sosy-lab/java-smt

http://www.fit.vutbr.cz/research/groups/verifit/tools/includer/

Proof of Lemma 3

Proof. It is sufficient to show that there exists k ≥ 0 such that for all u ∈ Σ * there exists i ∈ [0, k] such that Post A (ι, u) | = Post A (ι, µ(i)). We have Post A (ι, u) | = Post A (ι, u) for all u ∈ Σ * . But since Π is a finite set, also the set {Post A (ι, u) | u ∈ Σ * } is finite. Thus there exists k ≥ 0 such that, for all u ∈ Σ * there exists i ∈ [0, k] such that Post A (ι, u) ⇔ Post A (ι, µ(i)), which concludes the proof.

Proof of Lemma 4

Proposition 2. Given a formula φ ∈ Form + (Q, x) and a ∈ Σ, we have ∆(φ, a) ⇔ ∃Q . φ[Q /Q]∧ q∈Q (q → ∆(q, a)).

Proof. "⇒" If I, β∪ν∪ν | = ∆(φ, a), for some valuations β : Q → B and ν : x → Data I , ν : x → Data I , then we build a valuation β :

For each occurrence of a formula ∆(q, a) in ∆(φ, a) we set β (q ) = true if I, β ∪ ν ∪ ν | = ∆(q, a) and β (q ) = false, otherwise. Since there are no negated occurrences of such subformulae, the definition of β is consistent, and the check

(1) We apply Proposition 2 recursively and get:

(2) If , I 0 , . . . , I n , ⊥ is an interpolant for Θ(u), the following entailments hold:

For the induction step n > 0, we compute:

Proof. We prove the following invariant: each time Algorithm 1 reaches line 3, the set W of nodes in WorkList contains all the frontier nodes in the ART N ∪ W, E, r, Λ, which are not covered by some node in N, namely that:

Initially, this is the case because W = {r} and E = = ∅. If the invariant holds previously, at line 3, it will hold again after line 19 is executed, because, when the subtree rooted at the pivot p is removed, p becomes a member of the set of uncovered frontier nodes, and is added to W at line 19. Otherwise, the invariant holds at line 3 and the control follows the else branch at line 20. In this case, the newly created frontier node s is added to W only if it is not covered by an existing node in N (line 23).

Next we prove that, if Algorithm 1 returns true, then n∈N Λ(n) defines a safety invariant. Suppose that Algorithm 1 returns at line 37. Then it must be that W = ∅. Because (3) is invariant, each node in N is either covered by another node in N, or all its successors are in N. We prove first that n∈N Λ(n) is an invariant: for any u ∈ Σ * , there exists some node n ∈ N such that Post A (ι, u) | = Λ(n). Let u ∈ Σ * be an arbitrary sequence. If u labels the path from r to some n ∈ N, we have To prove that n∈N Λ(n) is, moreover, a safety invariant, suppose, by contradiction, that there exists u ∈ Σ * such that Acc A (u) is satisfiable. By the previous point, there exists a node p ∈ N such that Post A (ι, u) | = Λ(p). But then we have Acc A (ι, u) | = Acc A (ι, λ(p)), thus Acc A (ι, λ(p)) is satisfiable as well. However, this cannot be the case, because p has been processed at line 8 and Algorithm 1 would have returned a counterexample, contradicting the assumption that it returns true. This concludes the proof that n∈N Λ(n) is a safety invariant, thus L(A) = ∅, by Lemma 2. We have then proved the second point of the statement.

For the first point, assume that L(A) 0 and let w = (a 1 , ν 1 ) . . . (a k , ν k ) ∈ L(A) be a word. By the above, Algorithm 1 cannot return true. Suppose, by contradiction that it does not terminate. Since the sequences from Σ * are explored in breadth-first order, every sequence of length k is eventually explored, which leads to the discovery of w at line 8. Then Algorithm 1 terminates returning w ∈ L(A).

Proof of Theorem 2

Lemma 5. Given an ART T = N, E, r, Λ, R, T, built by Algorithm 2, Post A (Λ(n), a) | = Λ(m), for all (n, a, m) ∈ E.

Proof. We distinguish two cases. First, if (n, a, m) occurs on a path in T that has never been refined, then Λ(m) = and the entailment holds trivially. Otherwise, let Ω be the set of paths ω = (n 0 , a 1 , n 1 ), . . . , (n k-1 , a k , n k ), where n 0 = r and (n, a, m) = (n i-1 , a i , n i ), for some i ∈ [1, k] and, moreover, a 1 . . . a k was found, at some point, to be a spurious counterexample. Let , I ω 0 , . . . , I ω k , ⊥ be an interpolant for Φ(a 1 . . .

According to Lyndon's Interpolation Theorem, it is possible to build such an interpolant, when Φ(a 1 . . . a k ) is unsatisfiable. By Proposition 2, we obtain

Proof. We prove first that, each time Algorithm 2 reaches the line 3, we have:

Initially, W = {r} and E = = ∅, thus (4) holds trivially. Suppose that (4) holds at when reaching line 3 and some node n was removed from W and inserted into N. We distinguish two cases, either:

n is covered, in which case W becomes W \ {n} and (4) holds, or n is not covered, in which case W becomes (W \{n})∪S , where S = {s N | (n, a, s) ∈ E, a ∈ Σ} is the set of fresh successors of n. But then no node s ∈ S is covered and has successors in E, thus (4) holds.

Then the condition (4) holds next time line 3 is reached, thus it is invariant. Suppose first that Algorithm 2 returns true, thus W = ∅ and, by (4), for each node in n ∈ N one of the following hold:

n is covered, or for each a ∈ Σ there exists s ∈ N such that (n, a, s) ∈ E. We prove that, in this case, n∈N Λ(n) defines a safety invariant and conclude that L(A) = ∅, by Lemma 2. To this end, let u = a 1 . . . a k ∈ Σ * be an arbitrary sequence and let v 1 be the largest prefix of u that labels a path from r to some node n 1 ∈ N. If v 1 = u we are done. Otherwise, by the choice of v 1 , it must be the case that a successor of n 1 is missing from (N, E), thus n 1 must be covered, by (4) and the fact that W = ∅. Let n 1 be the closest ancestor of n 1 such that (n 1 , n 1 ) ∈ , for some n 1 ∈ N, and let v 1 be the prefix of v 1 leading to n 1 . By the construction of (line 4 in function Close), we have Λ(n 1 ) | = Λ(n 1 ). Applying Lemma 5 inductively on v 1 , we obtain that Post A (ι, v 1 ) | = Λ(n 1 ), thus Post A (ι, v 1 ) | = Λ(n 1 ). Continuing inductively from n 1 , we exhibit a sequence of strings v 1 , . . . , v ∈ Σ * and nodes r = m 0 , m 1 , . . . , m such that, for all i ∈ [1, ]:

v i labels the path between m i-1 and m i in (N, E),

To prove that n∈N Λ(n) is, moreover, a safety invariant, suppose that Acc A (u) is satisfiable, for some u ∈ Σ * and let n ∈ N be a node such that Post A (ι, u) | = Λ(n). By the previous point, such a node must exist. But then Acc A (u) | = Acc A (λ(n)), thus Acc A (λ(n)) is satisfiable, and Algorithm 2 returns at line 9, upon encountering λ(n). But this contradicts the assumption that Algorithm 2 returns true, hence we have proved that n∈N Λ(n) is a safety invariant, and L(A) = ∅ follows, by Lemma 2. We have then proved the second point of the statement.

To prove the first point, assume that L(A) ∅. By the previous point, Algorithm 2 does not return true. Suppose, by contradiction, that it does not terminate and conclude using the breadth-first argument from the proof of Theorem 1.