Vijay D'silva

Caterina Urban

Abstract Interpretation as Automated Deduction

ou non, émanant des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

Introduction

Two major approaches to automated reasoning about programs are those based on sat and smt solvers and those based on abstract interpretation. In the solverbased approaches, a property of a program is encoded by formulae in a logic or theory and a solver is used to check if the property holds. In abstract interpretation, a property of a program is expressed in terms of fixed points and fixed point approximation techniques are used to calculate and reason about fixed points [START_REF] Cousot | Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF]. The complementary strengths of these approaches has led to a decade of theoretical and practical effort to combine them.

The strengths of smt solvers include efficient Boolean reasoning, complete reasoning in certain theories, theory combination, proof generation and interpolation. Recent research has demonstrated that deduction algorithms have applications in program analysis besides solving formulae. dpll(t) and cdcl have been lifted to implement property-guided, path-sensitive analyses [START_REF] Silva | Abstract conflict driven learning[END_REF][START_REF] Harris | Program analysis via satisfiability modulo path programs[END_REF]. Stålmarck's method has been used to refine abstract transformers [START_REF] Thakur | A generalization of Stålmarck's method[END_REF], interpolants have been used to refine widening operators [START_REF] Gulavani | Automatically refining abstract interpretations[END_REF] and unification has been used to obtain complete reasoning about restricted families of programs [START_REF] Tiwari | Logical interpretation: Static program analysis using theorem proving[END_REF]. The Nelson-Oppen procedure, though less general than reduced product [START_REF] Cousot | Systematic design of program analysis frameworks[END_REF][START_REF] Cousot | Theories, solvers and static analysis by abstract interpretation[END_REF], works as an algorithmic domain combinator [START_REF] Gulwani | Combining abstract interpreters[END_REF].

Conversely, the strengths of abstract interpreters are the use of approximation to overcome the theoretical undecidability and practical scalability issues in program verification and the use of widening operators to derive invariants. The

Reachability as Second-Order Satisfiability

The contribution of this section is the logic ws1s(t), which is an extension of Büchi's ws1s with a theory. To simplify reasoning about programs in this logic, we restrict the class of models that are usually considered for ws1s.

Notation. We use = for definition. Let P(S) denote the set of all subsets of S, called the powerset of S, and F(S) denote the finite subsets of S. Given a function f : A → B, f [a → b] denotes the function that maps a to b and maps c distinct from a to f (c).

Weak Monadic Second Order Theories of One Successor

Our syntax contains first-order variables Vars, functions Fun and predicates Pred . The symbols x, y, z range over Vars, f, g, h range over Fun and P, Q, R range over Pred . We also use a set Pos of first-order position variables whose elements are i, j, k and a set SVar of monadic second-order variables denoted X, Y, Z. Second-order variables are uninterpreted, unary predicates. We also use a unary successor function suc and a binary, successor predicate Suc.

Our logic consists of three families of formulae called state, transition and trace formulae, which are interpreted over first-order structures, pairs of firstorder structures and finite sequences of first-order structures respectively. The formulae are named after how they are interpreted over programs.

t ::= x | f (t 0 , . . . , t n ) Term ϕ ::= P (t 0 , . . . , t n ) | ϕ ∧ ϕ | ¬ϕ State Formula ψ ::= suc(x) = t | ψ ∧ ψ | ¬ψ Transition Formula Φ ::= X(i) | Suc(i, j) | ϕ(i ) | ψ(i ) | Φ ∧ Φ | ¬Φ
x s = s(x) f (t 1 , . . . , t k ) s = I(f )( t 0 s , . . . , t n s )
As is standard, s |= T ϕ denotes that s is a model of ϕ in the theory T .

s |= T P (t 0 , . . . , t n ) if ( t 0 s , . . . , t n s ) ∈ I(P ) s |= T ϕ ∧ ψ if s |= T ϕ and s |= T ψ s |= T ¬ϕ if s |= T ϕ
The semantics of Boolean operators is defined analogously for transition and trace formulae, so we omit them in what follows. A transition is a pair of states (r, s) and a transition formula is interpreted at a transition.

(r, s) |= P (t 0 , . . . , t n ) if ( t 0 r , . . . , t n r ) ∈ I(P

) (r, s) |= suc(x) = t if x s = T t r A trace of length k is a sequence τ : [0, k -1] → State. We call τ (m) the state at position m, with the implicit qualifier m < k. A k-assignment σ : (Pos → N) • ∪ (SVar → F(N)) maps position variables to [0, k -1] and second-order variables to finite subsets of [0, k -1]. A k-assignment satisfies that {σ(X) | X ∈ SVar } partitions the interval [0, k -1].
We explain the partition condition shortly. A ws1s(t) structure (τ, σ) consists of a trace τ of length k and a k-assignment σ. A trace formula is interpreted with respect to a ws1s(t) structure.

(τ, σ) |= X(i ) if σ(i ) is in σ(X) (τ, σ) |= ϕ(i ) if τ (σ(i)) |= T ϕ (τ, σ) |= ψ(i ) if σ(i) < k -1 and (τ (σ(i)), τ (σ(i) + 1)) |= ψ (τ, σ) |= Suc(i, j) if σ(i) + 1 = σ(j) (τ, σ) |= ∃i : Pos.Φ if (τ, σ[i → n]) |= Φ for some n in N
Note that ϕ(i) is interpreted at the state at position σ(i) and ψ(i) at the transition from σ(i). The semantics of ψ(i) is only defined if σ(i) is not the last position on τ . A trace formula Φ is satisfiable if there exists a trace τ and assignment σ such that (τ, σ) |= Φ. We assume standard shorthands for ∨ and ⇒ and write

Φ |= Ψ for |= Φ ⇒ Ψ .
Example 1. The ws1s formula First(i) = ∀j.¬Suc(j, i) is true at the first position on a trace and Last(i) = ∀j.¬Suc(i, j) is true at the last position. See [START_REF] Vardi | Automata: from logics to algorithms[END_REF][START_REF] Van Den Elsen | Weak monadic second-order theory of one successor[END_REF] for more examples. ws1s(t) has no second-order quantification so the encoding of transitive closure in ws1s does not carry over. Transitive closure may be encoded if the underlying theory is powerful enough.

Encoding Reachability in WS1S(T)

Büchi showed that the models of a ws1s formula form a regular language and vice-versa. The modern proof of this statement [START_REF] Vardi | Automata: from logics to algorithms[END_REF][START_REF] Van Den Elsen | Weak monadic second-order theory of one successor[END_REF] encodes the structure of a finite automaton using second-order variables. We now extend this construction to encode a control-flow graph (cfg) by a ws1s(t) formula.

A command is an assignment x := t of a term t to a first-order variable x, or is a condition [ϕ], where ϕ is a state formula. A cfg G = (Loc, E, in, Ex , stmt) consists of a finite set of locations Loc including an initial location in, a set of exit locations Ex , edges E ⊆ Loc × Loc, and a labelling stmt : E → Cmd of edges with commands. To assist the presentation, we require that every location is reachable from in, and that exit locations have no successors. This requirement is not fundamental to our results.

We define an execution semantics for cfgs. We assume that terms in commands are interpreted over the same first-order structure as state formulae. The formula Same V = x∈V succ(x) = x expresses that variables in the set V are not modified in a transition and Trans c is the transition formula for a command.

Trans c = b =⇒ Same Vars if c = [b] suc(x) = t ∧ Same Vars\{x} if c = x := t
A transition relation for a command c is the set of models Rel c of Trans c . We write Trans e and Rel e for the transition formula and relation of the command stmt(e). An execution of length k is a sequence ρ = (m 0 , s 0 ), . . . , (m k-1 , s k-1 ) of location and state pairs in which each e = (m i , m i+1 ) is an edge in E and the pair of states (s i , s i+1 ) is in the transition relation Rel e . A location m is reachable if there is an execution ρ of some length k such that ρ(k -1) = (m, s) for some state s.

The safety properties checked by abstract interpreters are usually encoded as reachability of locations in a cfg. The formula Reach G,L below encodes reachability of a set of locations L in a cfg G as satisfiability in ws1s(t). The first line below is an initial constraint, the second is a set of transition constraints indexed by locations, and the third line encodes final constraints.

Reach G,L = ∀i.First(i) =⇒ X in (i) ∧ v∈Loc ∀i.∀j.X v (j) ∧ Suc(i, j) =⇒ (u,v)∈E Trans (u,v) (i) ∧ X u (i) ∧ ∀j.Last(j) =⇒ u∈L X u (j)
We explain this formula in terms of a structure (τ, σ). The trace τ contains valuations of variables but has no information about locations. A second-order variable X v represents the location v and σ(X v ) represents the points in τ when control is at v. The initial constraint ensures that execution begins in in. The final constraint ensures that execution ends in one of the locations in L. In a transition constraint, X v (j) ∧ Suc(i, j) expresses that the state τ (j) is visited at location v and its consequent expresses that the state τ (i) must have been visited at a location u that precedes v in the cfg and that (τ (i), τ (j)) must be in the transition relation (u, v).

Theorem 1. Some location in a set L in a cfg G is reachable if and only if the formula Reach G,L is satisfiable. Proof. [⇐] If a location w ∈ L is reachable, there is an execution ρ = (u 0 , s 0 ), . . ., (u k-1 , s k-1 ) with u 0 = in and u k-1 = w. Define the structure (τ, σ) with τ = s 0 , . . . , s k-1 and σ = {X u → {i | ρ(i) = (u, s), s ∈ State} | u ∈ Loc}.
We show that (τ, σ) is a model of Reach G,L . Since u 0 = in and u k-1 = w, the initial and final constraints are satisfied. In the transition constraint, if X v (j) holds, there is some (u i , s i ), (u i+1 , s i+1 ) in ρ with u i+1 = v. Thus, the transition (s i , s i+1 ) satisfies the transition formula Trans (ui,v) .

[⇒]Assume (τ, σ) is a model of Reach G,L . Define a sequence ρ with ρ(i) = (u, τ (i)) where i ∈ σ(X u ). As σ induces a partition, there is a unique u with i in σ(X u ). We show that ρ is an execution reaching L. The initial constraint guarantees that ρ(0) is at in and the final constraints guarantee that ρ ends in L. The transition constraints ensure that every step in the execution traverses an edge in G and respects the transition relation of the edge.

We believe this is a simple yet novel encoding of reachability, a property widely checked by abstract interpreters, in a minor extension of a well-known logic. The translation from second-order logics is at the heart of the automatabased verification, so we believe this work connects abstract interpretation to the automata-theoretic approach to program verification in a fundamental, yet novel way. In other second-order characterizations of correctness [START_REF] Aiken | Introduction to set constraint-based program analysis[END_REF][START_REF] Grebenshchikov | Synthesizing software verifiers from proof rules[END_REF], it is invariants and not executions that are encoded by satisfying assignments. Moreover, those encodings do not connect to the automata-theoretic approach.

Example 2. A cfg G and the formula Reach G,Ex for a program with a variable x of type Z are shown in Fig. 1. Executions that start with a strictly negative value of x neither terminate nor reach ex. For brevity, we write a state as the value

(∀i.First(i) ⇒ Xin(i)) ∧ (∀i.Last(i) ⇒ Xex(i)) ∧ ∀i.∀j.Xin(j) ∧ Suc(i, j) ⇒ (suc(x) = x -1)(i) ∧ Xa(i) ∧ ∀i.∀j.Xa(j) ∧ Suc(i, j) ⇒ ((x = 0 ⇒ suc(x) = x)(i) ∧ Xin(i) ∧ ∀i.∀j.Xex(j) ∧ Suc(i, j) ⇒ (x = 0 ⇒ suc(x) = x)(i) ∧ Xin(i)) in a ex [x = 0] [x = 0] x := x -1
Fig. 1. A cfg for a program with non-terminating executions and a ws1s(t) formula over the theory of integer arithmetic encoding the reachability of ex. of x. The execution (in, 1), (a, 1), (in, 0), (ex, 0) reaches ex. It is encoded by the model (τ, σ), with σ = {X in → {0, 2} , X a → {1} , X ex = {3}} and τ = 1, 1, 0, 0. Note that σ partitions SVar because each position on the trace corresponds to a unique location. No structure (τ, σ) in which x is strictly negative in τ (0) satisfies Reach G,Ex .

Note that a program invariant would include all reachable states, but a model of Reach G,L only involves states that occur on a single execution. We emphasise that we are not considering arbitrary formulae in ws1s(t). The formula Reach G,L is a conjunction of constraints in which the initial, final and transition constraints have a fixed structure. The second-order variables and first-order program variables are free, but the first-order position variables are bound.

Lattices and Substructural First-Order Theories

The contribution of this section is to relate first-order substructural theories with the lattices in abstract domains. We show that certain lattices used in practice are Lindenbaum-Tarski algebras of theories that we introduce here.

First-Order Substructural Theories

For this section, assume a set of variables Vars and a first-order theory of integer arithmetic with the standard functions and relations and let |= Z define the semantics of quantifier-free first-order formulae. A logical language (L, L ) consists of a set of formulae and a proof system. The grammar below defines a set of formulae in terms of atomic formulae, logical constants and connectives.

We introduce formulae and calculi for a sign logic, a constant logic and an interval logic, with the names deriving from the abstract domains being modelled. The formulae in our logics are closed under conjunction but not under disjunction or negation. There are only three atomic formulae in S. The infinitely many atomic formulae in C are equalities between a variable and an integer, and atomic formulae in I-formulae involve upper bounds and lower bounds on variables. The three logics contain the logical constant tt, denoting true, but instead

The core calculus core i ϕ ϕ

ffl ffx ϕ(x) Γ ϕ ϕ, Σ ψ cut Γ, Σ ψ ttr Γ tt Γ ψ wl Γ, ϕ ψ Γ, ϕ, ϕ ψ cl Γ, ϕ ψ Γ, ϕ, ψ θ pl Γ, ψ, ϕ θ Γ, ϕ θ ∧l1 Γ, ϕ ∧ ψ θ Γ, ψ θ ∧l2 Γ, ϕ ∧ ψ θ Γ ϕ Σ ψ ∧r Γ, Σ ϕ ∧ ψ Table 1.
Proof rules for the core calculus and its extensions. The core calculus core contains rules for introduction (i), cut (cut), weakening (wl), contraction (cl) and permutation (pl) on the left, conjunction (∧l1, ∧l2, ∧r), false (ffl), in which ϕ(x) has only one free variable x, and true (ttr).

of a constant for false, we have a family ff x parameterized by variables.

ϕ ::= x < 0 | x = 0 | x > 0 | ff x | tt | ϕ ∧ ϕ S ϕ ::= x = k | ff x | tt | ϕ ∧ ϕ C ϕ ::= x ≤ k | x ≥ k | ff x | tt | ϕ ∧ ϕ I
A calculus core for the logical core of these logics is shown in Table 1. We use sequents of the form Γ, Σ L ϕ, where the antecedents Γ and Σ are sequences of formulae, and the consequent ϕ is a single, first-order formula. We write Γ for the conjunction of the sequence elements in Γ . A calculus L is sound if every derivable sequent Γ L ψ satisfies that |= Z Γ ⇒ ψ. The semantics of ff x in |= Z is ff. Two formulae are inter-derivable if the sequents ϕ L ψ and ψ L ϕ are both derivable. Sequent calculi usually contain structural, logical and cut rules, and in the case of theories also theory rules. Our logics are substructural because the sequents have a restricted structure, lack right structural rules, and lack rules for disjunction, negation and implication. Our non-standard treatment of false is influenced by the way abstract domains reason about contradictions.

We review the theory rules for our logics. The reader should be warned that these logics have a restricted syntax and weak proof systems so the set of derivations is limited. We claim no responsibility for any disappointment arising from how uninteresting the derivable theorems are. The calculus S , in Fig. 2, extends core with rules for deriving ff x from conjunctions of atomic formulae. The calculus for C is similar to that for S with the theory rule below instead. The calculus I in Fig. 4 contains rules for modifying upper and lower bounds.

[m = Z n] ffr4 Γ, x = m ∧ x = n ff x
Example 3. Fig. 3 contains a derivation of x < 0 S x < 0 ∧ tt. The converse x < 0∧tt S x < 0 is derivable with i and ∧l 1 , showing that x < 0 and x < 0∧tt are inter-derivable.

x < 0 x = 0 x > 0 ⊥ S core ffr1 Γ, x < 0 ∧ x = 0 ffx ffr2 Γ, x = 0 ∧ x > 0 ffx ffr3 Γ, x < 0 ∧ x > 0 ffx
Fig. 2. A lattice of signs and a calculus that generates it. The proof is by induction on the structure of a derivation. This soundness theorem is used to show an isomorphism between the lattices generated by these calculi and the lattices they model.

i x < 0 S 1 x < 0 ttr x < 0 S 1 tt ∧r x < 0, x < 0 S 1 x < 0 ∧ tt cl x < 0 S 1 x < 0 ∧ tt

Lattices from Substructural Theories

We recall elementary lattice theory. A lattice (A, , , ) is a partially ordered set (poset) with a binary greatest lower bound , called the meet, and a binary least upper bound , called the join. A poset with only a meet is called a meetsemi-lattice. A lattice is bounded if it has a greatest element , called top, and a least element ⊥ called bottom. The notion of isomorphism for lattices is standard.

Pointwise lifting is an operation that lifts the order and operations of a lattice to functions on the lattice. Consider the functions f, g : S → A, where S is a set and A a lattice as above. The pointwise order f g holds if f (x) g(x) for all x, while the pointwise meet f g maps x in S to f (x) g(x). The pointwise lift of other relations and operations on A is similarly defined.

Tarski related logic and lattices by extending a construction of Lindenbaum to generate Boolean algebras from propositional calculi and first-order sentences. We use a generalization of this construction to formulae with free variables [START_REF] Rasiowa | The mathematics of metamathematics[END_REF]. We write [ϕ] L for the equivalence class of ϕ with respect to an equivalence relation ≡ L . A logic (L, L ) that is closed under conjunction generates the

x ≤ 100 x ≤ 99 y ≤ 100 y ≤ 99 x ≥ 0 x ≥ 1 y ≥ 0 y ≥ 1
x: [START_REF] Abramsky | Domain Theory and the Logic of Observable Properties[END_REF]99] x ≤ 99, y ≤ 99

x ≥ 1, y ≥ 1

x: [START_REF] Bjørner | Accelerating lemma learning using joins -DPLL[END_REF][START_REF] Silva | Abstract conflict driven learning[END_REF], y: [START_REF] Abramsky | Domain Theory and the Logic of Observable Properties[END_REF][START_REF] Cousot | Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF] x: [START_REF] Bjørner | Accelerating lemma learning using joins -DPLL[END_REF][START_REF] Cousot | Systematic design of program analysis frameworks[END_REF], y: [START_REF] Abramsky | Domain Theory and the Logic of Observable Properties[END_REF][START_REF] Brain | Deciding floatingpoint logic with abstract conflict driven clause learning[END_REF] x: [START_REF] Cousot | Systematic design of program analysis frameworks[END_REF][START_REF] Silva | Abstract conflict driven learning[END_REF], y: [START_REF] Brain | Deciding floatingpoint logic with abstract conflict driven clause learning[END_REF][START_REF] Cousot | Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF] x:3, y:1 x:7, y:4 x:9, y:6 Lindenbaum-Tarski algebra (L/≡ L , , ) below.

⊥ I core Γ, x ≤ n ϕ [m ≤ n] ub-l Γ, x ≤ m ϕ Γ x ≤ m [m ≤ n] ub-r Γ x ≤ n Γ, x ≥ m ϕ [m ≤ n] lb-l Γ, x ≥ n ϕ Γ x ≥ n [m ≤ n] lb-r Γ x ≥ m [m < n] ffr5 Γ, x ≤ m ∧ x ≥ n ffx
ϕ ≡ L ψ if ϕ L ψ and ψ L ϕ. [ϕ] L [ψ] L if θ 1 L θ 2 for some θ 1 ∈ [ϕ] L , and θ 2 ∈ [ψ] L . [ϕ] L [ψ] L = [θ 1 ∧ θ 2 ] L where θ 1 ∈ [ϕ] L , and θ 2 ∈ [ψ] L .
The relation ≡ L , defined by inter-derivability, is an equivalence whose classes form the carrier set of the algebra. Logical connectives generate operators. Though Lindenbaum-Tarski algebras of standard logics have been studied in depth, the algebras for the substructural theories we consider have not. To prove the lemma below, we show that derivability induces a partial order on the equivalence classes of ≡ L and that conjunction induces a greatest lower bound. Lemma 1. Let (L, ) be a quantifer-free first-order language closed under conjunction and be a sound calculus that extends core . The Lindenbaum-Tarski algebra of L is a meet-semi-lattice.

We now recall certain lattices used in abstract interpretation and show that they are isomorphic to the Lindenbaum-Tarski algebras of the logics we introduced. The lattice of signs (Sign, ) is shown in Fig. 2 To provide intuition for the proof, we detail here the case for the logic S and the lattice Sign over one variable. To prove that the Lindenbaum-Tarski algebra of S over a variable x is isomorphic to Sign we have to show that there are five equivalence classes, and that and are as in Fig. 2. The five candidate equivalence classes are

{[ff x ] S , [tt] S , [x < 0] S , [x = 0] S , [x > 0] S }.
The proof that there are at most five equivalence classes is by induction on the structure of formulae. The proof argument is that every conjunct in S is inter-derivable from a formula in one of these classes. The proof that there are at least five equivalence classes relies on the soundness of S . If there are fewer than five equivalence classes, there are consequences derivable in S that do not hold semantically. Observe that this proof argument holds only because every lattice element represents a different set of structures. In abstract interpretation parlance, this argument only applies to abstractions in which the concretization function is injective.

Next, we define a function h : S/≡ S → Sign that maps equivalence classes to corresponding lattice elements. To show that h is an isomorphism we argue by induction on formula structure for comparable equivalence classes and by appeal to soundness for incomparable equivalence classes. This argument generalizes to a finite number of variables because all the logics we have considered only involve one-place predicates. The shaded elements in Fig. 4 are the images of the formulae shown under the isomorphism.

Abstract Transformers, Deduction and Abduction

The constant and interval domains are used in practice even though, as shown in the previous section, they have weak proof systems. In this section, we adapt Tarski's notion of consequence operators to logically model abstract transformers for conditionals. Consequence operators provided an approach to algebraically modelling deduction. These transformers can be viewed as enriching a weak proof system L with the ability to reason about formulae that are not definable in L.

We consider again a quantifier-free first-order theory T with semantics |= T and a logical language (L, L ), where L ⊆ T . Deduction in L with respect to a formula ϕ ∈ T is formalized by a deduction function ded ϕ : F(L) → F(L) between finite sets of formulae in L. A deduction function is sound if for finite Θ ⊆ L, and θ ∈ ded ϕ (Θ), ϕ ∧ Θ |= T θ. That is, the deduced formulae are consequences of the arguments and, crucially, the parameter ϕ. The formula ϕ acts as an external hint to boost the capabilities of a weak deductive system. The parameter ϕ may not exist in L, so there may not be a rule of the form ϕ, Γ L θ corresponding to an application of the deduction function.

Similarly, we model abduction by a function that generates antecedents given consequents. An abduction function abd ϕ : F(L) → F(L) derives antecedents in L with respect to a parameter ϕ. An abduction function is sound if for all Θ, and θ ∈ abd ϕ (Θ), ϕ ∧ θ |= T Θ.

Example 4. This examples illustrates how deduction with respect to a formula enables reasoning that is not possible in the lattice itself. Let ϕ = 3y -1 > 0 ∧ x = -y be a formula in a theory. We define one possible sound deduction function ded ϕ for consequences in S.

ded ϕ ({tt}) = ded ϕ ({y > 0}) = ded ϕ ({x < 0}) = {y > 0, x < 0} ded ϕ ({ff x }) = ded ϕ ({x = 0}) = ded ϕ ({x > 0}) = ded ϕ ({y = 0}) = {ff x , ff y }
The results of applying ded ϕ shown above are the only two possibilities, even for sets of formulae not shown above.

The difference between ded ϕ and classical consequence operators is that we make fewer assumptions on properties of ded ϕ in the same way our lattices make fewer structural assumptions than classical logics. Recall that a set of formulae C is consequence-closed with respect to L if for all ϕ in C, if ϕ L θ, then θ is in C. The consequence closure of C is the smallest consequence-closed set containing C. If Γ L θ, the consequence closure of Γ contains the consequence closure of θ. A deduction function inverts this relationship, because it strengthens its argument using ϕ. That is, the consequence closure of ded ϕ (Θ) is a superset of the consequence closure of Θ because it contains formulae derived using ϕ.

Deduction functions, when factored through the Lindenbaum-Tarski equivalence relation, give rise to sound transformers for conditionals. To make this precise, we require the notion of a concretization function from abstract interpretation. Let (A, , ) be a bounded lattice and (P(State), ⊆, ∩) be the powerset of states with the subset order. We say that A is an abstraction of P(State) if there is a monotone function γ : A → P(State) satisfying that γ( ) = State and γ(⊥) = ∅. Requiring that ⊥ has an empty concretization is non-standard but is required for a logical treatment of false.

Recall that Rel To relate these transformers to deduction and abduction functions, we lift the functions above to operate on the Lindenbaum-Tarski algebra. We write ≡ instead of ≡ L for brevity.

ded ≡ ϕ : L/≡ → L/≡ ded ≡ ϕ ([θ] ≡ ) = {[ψ] ≡ | ψ ∈ ded ϕ ([θ] ≡ )} abd ≡ ϕ : L/≡ → L/≡ abd ≡ ϕ ([θ] ≡ ) = [ψ] ≡ for some ψ ∈ abd ϕ ([θ] ≡ )
The result of deduction on the Lindenbaum-Tarski algebra is a meet of equivalence classes of formulae in order to obtain the strongest consequence possible.

Assuming that an equivalence class consists of only finitely many formulae, this result is well-defined. If an equivalence class is not finite, a finite number of representatives can be used instead. The lift of abduction is not the dual of deduction. Instead, the result of lifting abduction is the equivalence class of one of the formulae that result from abduction. This is because we want the weakest possible abduction but our logics lack disjunction. Using the lattice-theoretic join in algebras where the join exists may lead to unsound abduction.

Theorem 4. Let ded ϕ and abd ϕ be sound deduction and abduction transformers and (L, L ) be a logical language closed under conjunction with a calculus that extends core . Then, the lifted functions ded ≡ ϕ and abd ≡ ϕ are sound successor and predecessor transformers for the conditional [ϕ].

We have not modelled transformers for assignment because we have not identified a satisfying treatment of substitution and quantification that factors through the Lindenbaum-Tarski construction.

Abstract Interpreters as Second-Order Solvers

An abstract interpreter for reachability analysis combines a lattice with transformers to derive program invariants. We have shown that lattices approximate state formulae, and that deduction and abduction functions approximate transition formulae. We now show that the steps in fixed point iteration can be understood as second-order propagation. Logically, a fixed point iterator can be viewed as an smt solver for trace formulae.

We introduce abstract assignments to model approximations of trace formulae. We have chosen this term to emphasise the similarity to partial assignments in sat solvers. Let (A, , ) be a lattice that is an abstraction of the lattice of states (P(State), ⊆, ∩). Recall that SVar is the set of second-order variables. The lattice of abstract assignments is (Asg A , , ), where Asg A = SVar → A is the set of abstract assignments and the order and meet are defined pointwise.

Let Struct be the set of pairs (τ, σ) of ws1s(t) structures. We show that the lattice of abstract assignments is an abstraction of (P(Struct), ⊆, ∪). An abstract assignment represents sets of ws1s(t) structures analogous to the way a partial assignment in a dpll-based sat solver represents all assignments that extend to undefined variables. The set of ws1s(t) structures represented by an abstract assignment is given by the concretization conc :

Asg A → P(Struct) below. conc(asg) = {(τ, σ) | for all X ∈ SVar . {τ (i) | i ∈ σ(X)} ⊆ γ(asg(X))}
Explained in terms of states, an abstract assignment represents structures by the set of states at each program location but forgets the order between states.

We present the run of an abstract interpreter as a solver for Reach G,L . An abstract interpreter begins with the variable map λY. indicating that nothing is known about the satisfiability of Reach G,L , so every structure is potentially a model of Reach G,L . An abstract assignment is updated using a propagation rule. If a location is not reachable, the formula is unsatisfiable, as deduced by the conflict rule.

asg asg[X v → d], where d = (u,v)∈E post (u,v) (asg(X v )) Propagate asg unsat if asg(X v ) = ⊥, for some v ∈ L Conflict
Propagation modifies an abstract assignment similar to the way Boolean constraint propagation (bcp) updates a partial assignment with two key differences. One is that rather than values, the assignment is updated with elements of a lattice. The second is that in bcp, before decisions are made, every value that is undefined becomes tt or ff, becoming strictly more precise. With abstract assignments, the assignments to X v within an scc with more than one node, will, in general, get weaker. We have not modelled termination concerns, which are addressed with widening and narrowing operators. The theorem below expresses the soundness of fixed point iteration without widening and narrowing in terms of satisfiability.

Theorem 5. If the repeated application of the propagation and conflict rules leads to unsat, the formula Reach G,L is unsatisfiable.

Related Work, Discussion and Conclusion

The development of novel combinations of automated deduction and abstract interpretation is a driving force behind much current research, which we surveyed in the introduction. Consult the dissertations [START_REF] Haller | [END_REF][START_REF] Thakur | Symbolic Abstraction: Algorithms and Applications[END_REF] and Dagstuhl seminar notes [START_REF] Kroening | Decision procedures and abstract interpretation (Dagstuhl seminar 14351)[END_REF] for a detailed treatment of this research. Such work has been applied to design new smt solvers [START_REF] Brain | Deciding floatingpoint logic with abstract conflict driven clause learning[END_REF], program analyzers [START_REF] Silva | Numeric bounds analysis with conflict-driven learning[END_REF][START_REF] Thakur | Satisfiability modulo abstraction for separation logic with linked lists[END_REF], and has helped automate the construction of program analyzers [START_REF] Thakur | A method for symbolic computation of abstract operations[END_REF][START_REF] Thakur | Bilateral algorithms for symbolic abstraction[END_REF][START_REF] Thakur | Posthat and all that: Automating abstract interpretation[END_REF]. However, our experience has been that crucial aspects of solvers such as branching and conflict analysis heuristics are difficult to characterize latticetheoretically due to their combinatorial nature. In this work, we have initiated a complementary research programme by giving logical characterizations of instances of abstract interpretation. To relate logics to lattices, we have combined ideas from substructural logic with the Lindenbaum-Tarski construction [START_REF] Rasiowa | The mathematics of metamathematics[END_REF] and Tarski's algebraic treatment of deduction.

A more abstract approach would be to use the framework of Stone duality, which uses category theory to relate lattices, topological spaces and logics. Stone duality was extended to programs by Abramsky [START_REF] Abramsky | Domain Theory and the Logic of Observable Properties[END_REF] who related domains in semantics to intuitionistic, modal, fixed point logic. Jensen [START_REF] Jensen | Strictness analysis in logical form[END_REF] applied Abramsky's work to extract a logic from a specific abstract interpretation: strictness analysis.

In this paper, we have modelled logics that lack disjunction and have weaker proof systems than those considered in approaches based on Stone duality. The closest study to ours is by Schmidt [START_REF] Schmidt | Internal and external logics of abstract interpretations[END_REF], who articulated the idea that the partial order of an abstract domain defines its proof theory. In terms of algebraic logic, Schmidt's work can be understood as identifying logical characterization of families of lattices in abstract interpretation as free algebras of the Lindenbaum-Tarski construction. In comparison, our work has focused on characterizing specific lattices as theories.

Conclusion. This work is a first step towards a logical description of the internals of an abstract interpreter in the mathematical and algorithmic vocabulary of sat and smt solvers. The results in this paper make precise widespread folk intuition about the logical basis of certain abstract interpreters. Though our results are unsurprising, we believe the techniques we have used are novel and connect ideas from substructural logic, algebraic logic and satisfiability research. In using Büchi's construction, we have also connected abstract interpretation with the automata-theoretic approach to logic and verification. Folk knowledge asserts that transformers for assignments provide a form of quantifier elimination. We have not modelled these transformers here because we are missing a rigorous treatment that integrates with the Lindenbaum-Tarski construction.

In terms of solver architecture, the simple abstract interpreter we have considered can be viewed as a second-order theory solver that only updates assignments. This view provides a direct route to integrating branching heuristics, conflict analysis, and variable selection. We have begun these investigations and hope that this exposition enables the automated deduction community to participate in the same.

Fig. 3 .Theorem 2 .

 32 Fig. 3. A derivation in the sign calculus S .

Fig. 4 .

 4 Fig. 4. The domain of intervals over two variables and a calculus for interval logic.

Theorem 3 .

 3 . The lattice of integer constants (Const, ) consists of the elements Z ∪ {⊥, }, with ⊥ and as bottom and top, and all other elements being incomparable. The lattice of integer intervals(Itv , ), consists of the set {[a, b] | a ≤ b, a ∈ Z ∪ {-∞} , b ∈ Z ∪ {∞}}and a special element ⊥ denoting the empty interval. The partial order is standard and [-∞, ∞] is the top element.An abstract environment is a function ε : Vars → D, from program variables to a lattice D that represents approximations of variable values. A lattice of abstract environments is derived from a lattice D by pointwise lifting. The Lindenbaum-Tarski algebra of each of the logics S, C, I over a set of variables Vars, is isomorphic to the pointwise lift of each of the lattices Sign, Const, and Itv to abstract environments over Vars.

  [ϕ] is the transition relation for a conditional. A function post [ϕ] : A → A is a sound successor transformer for the conditional [ϕ] if the set of structures obtained by applying post [ϕ] overapproximates the structures obtained by applying the transition relation: Rel [ϕ] (γ(a)) ⊆ γ(post [ϕ] (a)). Dually, a function p re [ϕ] : A → A is a sound predecessor transformer for the conditional [ϕ] if the set of structures obtained by applying p re [ϕ] underapproximates the structures obtained by applying the transition relation backwards: γ( p re [ϕ] (a)) ⊆ s | Rel [ϕ] ({s}) ⊆ γ(a) .


Vijay D'silva

Caterina Urban

Conflict-Driven Conditional Termination

Keywords:

Conflict-driven learning, which is essential to the performance of sat and smt solvers, consists of a procedure that searches for a model of a formula, and refutation procedure for proving that no model exists. This paper shows that conflict-driven learning can improve the precision of a termination analysis based on abstract interpretation. We encode non-termination as satisfiability in a monadic second-order logic and use abstract interpreters to reason about the satisfiability of this formula. Our search procedure combines decisions with reachability analysis to find potentially non-terminating executions and our refutation procedure uses a conditional termination analysis. Our implementation extends the set of conditional termination arguments discovered by an existing termination analyzer.

Conflict-Driven Learning for Termination

Conflict-driven learning procedures are integral to the performance of sat and smt solvers. Such procedures combine search and refutation to determine if a formula is satisfiable. Conflicts discovered by search drive refutation, and search learns from refutation to avoid regions of the search space without solutions.

Our work is driven by the observation that discovering a small number of disjunctive termination arguments is crucial to the performance of certain termination analyzers [?]. Fig. ?? summarizes our lifting of conflict-driven learning to termination analysis. We use reachability analysis to find a set of states that constitute potentially non-terminating execution. We apply a conditional termination analysis to this set to eliminate states from which all executions terminate. Unlike termination analysis, which solves a decision problem and returns a yes or no answer, conditional termination analysis is concerned with discovering sufficient conditions for termination. Sufficient conditions for termination play the role of learned clauses in our analysis. They prevent subsequent runs of reachability analysis from revisiting states from which termination is guaranteed.

Our conflict driven conditional termination procedure (cdct) can be viewed as a sound but incomplete solver for a family of monadic, second-order formulae. Büchi's theorem shows that the language of a Büchi automaton is non-empty exactly if a formula in the monadic second-order theory of one successor (s1s) is satisfiable [?]. This theorem can be viewed encoding non-termination of a finite-state program as satisfiability in s1s. We introduce s1s(t), an extension of s1s to sequences of first-order structures, and encode non-termination in a Fig. 1: Conflict Driven Learning as applied to Termination control-flow graph (cfg) as satisfiability in s1s(t). A model of a formula is an infinite execution that respects the transition constraints in the cfg.

Formulating non-termination as satisfiability provides a clear route for lifting cdcl to non-termination. We combine decisions with reachability in an abstract domain to construct and refine assignments to second-order variables in the same way that sat solvers construct and refine partial assignments. A notable difference to standard abstract interpretation is that our assignments are neither over-nor under-approximations of the set of reachable states. Our conflict analysis uses backwards abstract interpretation to enlarge the set of states from which termination is guaranteed. We present a generalized unit rule for combining ranking functions with reachability analysis. These components are combined in our new analysis, which we have implemented and evaluated against state-of-the-art termination provers.

Non-Termination as Second-Order Satisfiability

The two contributions of this section are the logic s1s(t), which extends the monadic second-order logic of one successor (s1s) with a theory and an encoding of program non-termination as satisfiability in this theory.

Monadic Second-Order Theories of One Successor

We use = for definition. Let P(S) be the powerset of S. For f : A → B, the function f [a → b] maps a to b and c distinct from a to f (c). The symbols x, y, z range over first-order variables in Vars, f, g, h over functions in Fun, and P, Q, R over predicates in Pred . We use a set Pos of first-order position variables whose elements are i, j, k, a set SVar of monadic second-order variables denoted X, Y, Z, a unary successor function suc and a binary successor predicate Suc.

Our logic consists of three families of formulae called state, transition and trace formulae, which are interpreted over first-order structures, pairs of firstorder structures and infinte sequences of first-order structures respectively. The formulae are named after how they are interpreted over programs.

t ::= x | f (t 0 , . . . , t n ) Term ϕ ::= P (t 0 , . . . , t n ) | ϕ ∧ ϕ | ¬ϕ State Formula ψ ::= suc(x) = t | ψ ∧ ψ | ¬ψ Transition Formula Φ ::= X(i) | Suc(i, j) | ϕ(i ) | ψ(i ) | Φ ∧ Φ | ¬Φ
) ∈ I(P ) (r, s) |= ϕ ∧ ψ if (r, s) |= ϕ and (r, s) |= ψ (r, s) |= ¬ϕ if (r, s) |= ϕ (r, s) |= suc(x) = t if x s = t r A trace τ : N → (Vars → Val
) is an infinite sequence of states and τ (m) is the state at position m. A position assignment σ : (Pos → N) • ∪ (SVar → P(N)) maps position variables to N and second-order variables to subsets of N such that {σ(X) | X ∈ SVar } partitions N. We explain this partition condition shortly. A trace formula is interpreted with respect to an s1s(t) structure (τ, σ).

Note that there are first-order variables of two sorts in a trace formula. A trace formula Φ asserting that the transition formula ψ(x, y) = suc(x) = y + 1 is true at the trace position denoted by i has the form ψ(x, y)(i). The predicate Suc(i, j) asserts that the position j occurs immediately after i.

(τ, σ) |= Suc(i, j) if σ(i) + 1 = σ(j) (τ, σ) |= ϕ(i ) if τ (σ(i)) |= ϕ (τ, σ) |= ψ(i ) if (τ (σ(i)), τ (σ(i) + 1)) |= ψ (τ, σ) |= X(i ) if σ(i ) ∈ σ(X) (τ, σ) |= Φ ∧ Ψ if (τ, σ) |= Φ and (τ, σ) |= Ψ (τ, σ) |= ¬Φ if (τ, σ) |= Φ (τ, σ) |= ∃i : Pos.Φ if (τ, σ[i → n]) |= Φ for some n in N An s1s(t) structure (τ, σ) is a model of Φ if (τ, σ) |= Φ,
and is a countermodel otherwise. A trace formula is satisfiable if it has a model. An s1s(t) structure is defined using an infinite trace, so finite traces cannot be models of a formula.

Encoding Non-Termination in S1S(T)

We now recall control flow graphs (cfgs) and encode non-termination as satisfiability. A command in Cmd is an assignment x := t of a term t to a firstorder variable x, or is a condition [ϕ], where ϕ is a state formula. A cfg G = (Loc, E, in, ex, stmt) consists of a finite set of locations Loc including an

(∀i.First(i) ⇒ Xin(i)) ∧ (∀i.Xex(i) ⇒ Last(i)) ∧ ∀i.∀j.Xin(j) ∧ Suc(i, j) ⇒ (suc(x) = x -1)(i) ∧ Xa(i) ∧ ∀i.∀j.Xa(j) ∧ Suc(i, j) ⇒ (x = 0 ⇒ suc(x) = x)(i) ∧ Xin(i) ∧ ∀i.∀j.Xex(j) ∧ Suc(i, j) ⇒ (x = 0 ⇒ suc(x) = x)(i) ∧ Xin(i) in a ex [x = 0] [x = 0] x := x -1
Fig. 2: A formula encoding non-termination of the program shown in the monadic second-order theory of one successor over integer arithmetic. initial location in, an exit location ex, edges E ⊆ Loc × Loc, and a labelling stmt : E → Cmd of edges with commands. To assist the presentation, we assume that the exit location ex has no successors.

The formula Trans c below defines the semantics of commands using the condition Same V = x∈V suc(x) = x, that variables in V are not modified. The set of models of Trans c is the transition relation Rel c . We write Trans e and Rel e for the transition formula and relation of the command stmt(e). The formula Inf G extends the translation of Büchi automata to s1s to encode cfgs in s1s(t). We write First(i) = ∀j.¬Suc(j, i) for the first position on a trace and Last(i) = ∀j.¬Suc(i, j) for a position that cannot be on an infinite trace.

Trans c = b =⇒ Same Vars if c = [b] suc(x) = t ∧ Same Vars\{x} if c = x := t Inf G = (∀i.First(i) =⇒ X in (i)) ∧ (∀j.X ex (j) =⇒ Last(j)) ∧ v∈Loc ∀i.∀j.X v (j) ∧ Suc(i, j) =⇒ (u,v)∈E Trans (u,v) (i) ∧ X u (i)
The formula Inf G encodes program behaviour as follows. Consider an s1s(t) structure (τ, σ). The interpretation σ(X ) of a second-order variable X represents positions on the trace when execution is at location . Such an interpretation partitions N because each position on a trace corresponds to a unique location. The entry constraint on First(i) ensures execution begins at in. The exit constraint implying Last(j) enforces that an infinite execution does not visit ex. The conditions involving Suc(i, j) are called transition constraints and express that consecutive states on a trace must respect the transition relation of G. Theorem ?? expresses non-termination as satisfiability.

Theorem 1. A cfg G has a non-terminating execution iff Inf G is satisfiable.
We believe this is a simple yet novel encoding of non-termination that allows the duality between search and refutation to be exploited for termination analysis. In contrast, the second-order encoding of termination in [?] uses a predicate for disjunctive well-foundedness and is solved in a different manner.

Example 1. A cfg G and the formula Inf G for a program with a variable x of type Z are shown in Fig. ??. We write a trace as a sequence of values of x. Let τ be the trace -1, -1, -2, -2, . . . and σ the assignment mapping X ex to the empty set, and X in and X a to even and odd positions, respectively. The structure (τ, σ) is a model of Inf G . Every structure (τ, δ), with τ as before, in which δ(X ex ) is not empty is a countermodel of Inf G because ex is not reachable if x is initially -1, so some transition in τ must violate a transition constraint in Inf G . Every structure (τ , δ ) with x non-negative in τ (0) is also a countermodel of Inf G because executions with x initially non-negative terminate. Since τ is infinite by definition, some transition in τ must be infeasible. Terminating executions cannot be models of Inf G because traces in s1s(t) structures are infinite.

The formula Inf G is a conjunction of formulae in which second-order variables and first-order program variables are free but first-order position variables are bound. We exploit this structure in our analysis.

Conflict-Driven Conditional Termination

The conflict-driven conditional termination procedure (cdct) in Alg. ?? generalizes cdcl from sat to termination analysis. The input is the formula Inf G . The output (result, ∆, Θ) is a result concerning a set of structures ∆ and a set Θ of piecewise-defined ranking functions (pdrfs).

The value of result is one of divergent, terminates, or unknown. cdct returns divergent if the traces represented by ∆ do not reach the exit location, which could be due to non-termination or undefined behaviour; It returns terminates if ∆ is empty and Θ guarantees termination for all states. It returns unknown if cdct cannot prove termination and cannot progress. This happens if the abstract domain cannot accurately represent non-terminating executions, if the ranking functions used cannot express a termination argument, or a bound on the number of decisions has been exceeded.

cdct maintains four global data structures. The trail tr is a sequence of assignments to second-order variables. The explanation array exp contains in each element exp[i], the decision or constraint used by propagation to add tr [i] to the trail. The set of pdrfs Θ, generated by conditional termination analysis, are our analogue of learned clauses. The blocking constraints Ψ contain constraints representing two types of states, which need not be revisited. One is states from which all executions terminate. The other is states for which cdct could neither prove termination nor demonstrate non-termination.

Each execution of the cdct loop begins with a call to Search(), which attempts to find a non-terminating execution. If Search() returns divergent, cdct returns. If Search() returns unknown, the trail represents a potential conflict because it has discovered a set of states from which some execution terminates. The conflict is potential because the trail may also contain models of Inf G . This is a difference to sat and smt solvers where a conflict contradicts a formula.

The conflict analysis procedure Analyze() extracts from a potential conflict a definite conflict θ, expressed as a ranking function. The domain of θ represents states from which all executions terminate. The learning step Learn() generates a blocking constraint to drive subsequent search away from these states. Learning

Algorithm 1: CDCT(Inf G ) Trail: tr ← Explanations: exp ← Blocking constraints: Ψ ← ∅ pdrfs: Θ ← ∅ while true do result ← Search() if result = divergent or (result = unknown and exceeded()) then return (result, [tr ], Θ) θ ← Analyze() Θ ← Θ ∪ {θ} Ψ ← Ψ ∪ Learn([tr ], θ) if Backtrack() =

An Example Run.

A program is shown in C-like syntax alongside Alg. ??. The location a is reached after the variables are initialized, b is the loop head, and ex is the exit location. The program terminates but the abstract interpretationbased tool FuncTion [?] cannot prove termination. cdct enables FuncTion to prove termination while also avoiding case explosion. Even though other tools may be able to prove termination, we believe cdct is interesting because similar ideas could be used to expand the programs handled by those tools.

In this example, we use an interval abstract domain and affine ranking functions. Search() uses reachability analysis to derive the intervals y:[-3, 3], i:[-3, 3] at ex but termination analysis fails. Decisions restrict the range of a variable at a location: for example, Search() heuristically uses conditions from the code to make the decisions y:[1, ∞] and y:[-∞, 10] at location a. Reachability derives the range y: [START_REF] Aiken | Introduction to set constraint-based program analysis[END_REF][START_REF] Albarghouthi | Beautiful interpolants[END_REF], i:[-1, -1] at ex, which is a conflict, because no trace with these states at ex satisfies Inf G . Analyze() represents this conflict as X ex → {y: [START_REF] Aiken | Introduction to set constraint-based program analysis[END_REF][START_REF] Albarghouthi | Beautiful interpolants[END_REF], i:[-1, -1] → 0}, which assigns a pdrf to the second-order variable X ex and expresses that the program terminates in 0 steps for the states shown. The pdrf is propagated backwards through the program by an abstract interpreter [?] to derive the second-order assignments below. We omit the interval on i, which is unchanged.

X ex → y:[1, 3] → 0, X b → y:[1, 3] → 1, X b → y:[4, 4] → 3, X b → y:[5, 5] → 5
If these assignments are propagated to location b, we could only prove that the program terminates for y: [START_REF] Aiken | Introduction to set constraint-based program analysis[END_REF][START_REF] Büchi | On a decision method in restricted second order arithmetic[END_REF] at a. Instead, we apply widening to the pdrfs to derive X b → {y:[1, 3] → 1, y:[4, 10] → 2x + 5}, which bounds the number of steps to termination at the loop head for y in the ranges shown. We heuristically expand the piece y: [START_REF] Brain | Deciding floatingpoint logic with abstract conflict driven clause learning[END_REF][START_REF] Silva | Abstract conflict driven learning[END_REF] of the pdrf to y:[1, ∞] and check if the 2x + 5 is still a ranking function. Since it is, we have proved termination for executions with y:[1, ∞], i:[-1, -1] at b, despite having explicitly only analyzed the range y:[0, 5].

The learning step complements the decision y:[1, ∞] and uses X a → y:[-∞, 0] to restrict future search. Learnt constraints typically have more structure. A similar run of cdct can show termination when y is initially non-positive.

Consider the program with the loop condition changed to (y > -3). Now, the program does not always terminate. Decisions and learning can infer a ranking function for positive y as before. Decisions can also discover that for X a → y:[-1, -1], ex is unreachable, indicating non-termination (as all locations lead to ex). In this way, cdct proves conditional termination using disjunctions of ranking functions and also identifies non-terminating executions.

Search for a Conflict

We now show how a trail, a data structure used by sat solvers, can be used to make explicit the incremental progress made by an abstract interpreter.

Abstract Domains. A bounded lattice (L, , , ) is a partially ordered set with a meet , a join , a greatest element (top), and a least element ⊥ (bottom).

∈ Z ∪ {-∞, ∞}. The intervals [-∞, k], [k, ∞] are meet-irreducibles, unlike [0, 2]. The set S = {[-∞, 2], [0, ∞], [-5, ∞]} satisfies S = [0, 2] but is not a meet decomposition because {[-∞, 2], [0, ∞]} ⊂ S. The concrete complements of [-∞, k] and [k, ∞] are [k + 1, ∞] and [-∞, k -1], while [0, 2] has no concrete complement.
Abstract Assignments. sat solvers use partial assignments to incrementally construct a model. We introduce abstract assignments, which use abstract domains to represent s1s(t) structures. Let Struct be the set of s1s(t) structures. The lattice of abstract assignments (Asg A , ) contains the set Asg A = SVar → A with the pointwise order : asg asg if asg(X) asg (X) for all X in SVar . The meet and join are also defined pointwise. An abstract assignment asg represents a set of s1s(t) structures as defined by the concretization conc : Asg A → P(Struct).

conc(asg) = {(τ, σ) | for all X ∈ SVar . {τ (i) | i ∈ σ(X)} ⊆ γ(asg(X))}
An abstract assignment asg is a definite conflict for Φ if no model of Φ is in conc(asg) and is a potential conflict if conc(asg) contains a countermodel of Φ.

Trail. We introduce a trail, which contains meet-irreducibles as in [?,?] and in which a second-order variable can appear multiple times. A trail over A is the empty sequence or the concatenation tr •(X:m), where X is a second-order variable and m is a complementable meet-

dc ← {j → | 0 ≤ j ≤ |tr |} dc[|tr |] ← {|tr | → [tr ](Xex) → 0} i ← |tr | repeat if dc[i] = or exp[i] = nil then continue rk ← Term(exp[i], dc[i]) dc[i] ← i ← i -1 Update(dc, tr , rk ) until Unique Implication Point return [dc]
Propagate(). Alg. ?? calls an abstract interpreter and stores the results in the trail in a form amenable to conflict analysis and learning. The notion of meet-difference makes explicit the incremental change between two calls to the abstract interpreter. Formally, the meet-difference of a, b ∈ A mdiff (a, b) = mdc(a) \ mdc(b). The meet-difference of two abstract assignments is the pointwise lift mdiff (asg, asg

) = {X v :m | m ∈ mdiff (asg(X v ), asg (X v )), X v ∈ SVar }.
In a transition constraint ψ = ∀i.∀j.X v (j) ∧ Suc(i, j) ⇒ . . ., we write sink (ψ) for

X v . A strongly connected ( scc) of Inf G is a set of transition constraints T such that the set of locations {v | ψ ∈ T, X v = sink (ψ)} is an scc of G. The set of sccs of Inf G is scc(Inf G ).
Propagate() calls a standard abstract interpreter on each scc and uses a meet-difference calculation to extend the trail with new information. Propagate() also applies a generalized unit rule gunit, explained in § ??. Propagation is sound in the sense that it does not eliminate models of the constraints involved. Decisions. The abstract assignment computed by (the abstract interpreter used by) Propagate() can be refined using decisions. Boolean decisions make variables true or false and first-order decisions use values [?,?] but our decisions, like those in [?], use abstract domain elements.

A decision is an element X:m that can be on a trail. A decision is sound if conc(X:m) ∪ conc(X:m) = Struct. That is, considering the structures in m and m amounts to considering all possible structures. Example 4. Recall the unsound decision X in :[9, ∞] from Ex. ??. The structure (τ, σ) with τ = 9, 9, 8, 8, . . . and σ partitioning X in and X a into even and odd values is not in conc(X in :[9, ∞]) as x cannot be 8 at in.

Similarly, it is not in conc(X in :[-∞, 8]) so conc(X in :[9, ∞]) ∪ conc(X in :[-∞, 8]) = Struct.
The unsoundness arises because pointwise lifting does not preserve concrete complements. Though m is the concrete complement of m in A, [X v :m] need not could be obtained in the concrete domain. A sound abduction transformer is underapproximating. A ranking assignment rk : SVar → aRank associates a pdrf with each second-order variable. Ranking assignments form a lattice with point-wise meet and join and have a special order for fixed point checks [?]. To exchange information between Analyze() and Search() we extract a meetirreducible representation of the domains of pdrfs. The meet-projection of a pdrf ρ = {a i → f i } is the set of sets of meet-irreducibles mpr (ρ) = {mdc(a i )} and provides a dnf-like representation of the abstract partition in ρ.

Analyze(). Alg. ?? uses an array dc to construct and generalize a definite conflict. Each dc[i] represents termination conditions for states in the trail. Executions from states at ex terminate immediately so the last element of dc is {X ex → {[tr ](X ex ) → 0}} and all other elements are . The conflict analysis loop walks backwards through the trail and extends dc[i]. Forward propagation through the scc exp[i] added tr [i] to the trail, so dc[i] is propagated backwards through exp[i] to generalize the conflict to a ranking assignment rk . New pdrfs are added to dc by the procedure Update(). Specifically, for each X v modified by Term(), and m ∈ mpr (rk (X v )), Update() finds trail indices with tr [j] X v :m and sets dc[j] to the appropriate pdrf. Analyze() continues until a unique implication point is reached, which is typically a dominator in the cfg at which a decision was made. Analyze() returns [dc], a representation of the pdrfs in dc.

Learn() and the Generalized Unit Rule. Information computed by Search() is communicated to Analyze() using the trail, while information from Analyze() is represented within Search() by a blocking constraint and is incorporated in search using generalized unit rule. We describe these very briefly.

A set C = {X 1 :m 1 , . . . , X k :m k } of elements can be complemented elementwise to obtain C = {X 1 :m 1 , . . . , X k :m k }. If C is viewed as a conjunction of literals representing a conflict, C is a clause the procedure can learn. Learn() applies meet-projection to a pdrf and complements this projection to obtain a blocking constraint. In practice, we simplify the partitions of the pdrf to avoid an explosion of blocking constraints, analogous to subsumption in sat.

The generalized unit rule [?] extends a trail using a blocking constraint. Assume that Ψ has the form {X 0 :m 0 , . . . , X k :m k }. The trail gunit(tr . The experiments were performed on a system with a 1.30GHz 64-bit Dual-Core CPU (Intel i5-4250U) and 4GB of RAM. For the other tools, since we did not have access to their competition version, we used the SV-COMP 2015 results obtained on more powerful systems with a 3.40GHz 64-bit Quad-Core CPU (Intel i7-4770) and 33GB of RAM. Fig. ?? summarizes our evaluation. The first column is the number of programs each tool could prove terminating. The second column reports the average running time in seconds, and the last column reports the number of time outs, which was set to 180 seconds. In Fig. ??, the first column ( ) lists the number of programs that FuncTion+cdct proved terminating and the tool could not, the second column ( ) reports the number of programs that the tool proved terminating and FuncTion+cdct could not, and the last two columns report the number of programs that the tool and FuncTion+cdct were both able (×) or unable ( ) to prove terminating. The same symbols are used in Fig. ??.

, Ψ ) is tr • (X k :m k ) if [tr ](X i ) m i = ⊥ for 0 ≤ i < k
Fig. ?? shows that cdct causes a 9% improvement in FuncTion+cdct compared to FuncTion without cdct. The increase in runtime is not evenly distributed, and about 2% of the test cases require more than 20 seconds to be analyzed by FuncTion+cdct (cf. Fig. ??). In these cases the decision heuristics do not quickly isolate sets of states on which the abstract interpreter makes progress. without cdct [?], we observed a 2x speedup in the SV-COMP 2015 machines, so the runtime comparison of FuncTion+cdct and HIPTnT+ is inconclusive. Finally, thanks to the support for piecewise-defined ranking functions, 1% of the programs could be proved terminating only by FuncTion+cdct (2.7% by AProVE, 1% by HIPTnT+, and 1.7% by Ultimate Automizer). No tool could prove termination for 0.7% of the programs.

Related Work and Conclusion

Büchi's work relating automata and logic [?] is the basis for automata-based verification and synthesis. We depart from most work in this tradition in two ways. One is the use of sequences of first-order structures as in first-order temporal logics [?] and the other is to go from a graph-based representation to a formula, which is opposite of the translation used in automata-theoretic approaches. The use of s1s for pointer analysis [?], and termination [?] is restricted to decidable cases, as is [?]. Program analysis questions have been formulated with setconstraints [?] and second-order Horn clauses [?], but solutions to these formulae are typically invariants and ranking functions, not errors, and the methods used to solve them differ from cdct.

A key intuition behind our work is to lift algorithmic ideas from sat solvers to program analysis. The same intuition underlies smpp [?], which lifts dpll(t) to programs, acdcl [?,?], which lifts cdcl to lattices, the lifting of Stålmarck's method [?], and lazy annotation, which uses interpolants for learning [?]. The idea of guiding an abstract interpreter away from certain regions appears in dagger [?] and Vinta [?], from which cdct differs in the use of a trail in search and a unit rule in learning. Our generalized unit rule is from acdcl, but the use of s1s(t), potential conflicts and the combination with pdrfs is all new. The widening used in cdct preserves a termination guarantee and we believe that algorithms for generating small interpolants [?] can help design better widening operators.

Finally, termination analysis is a thriving area with more approaches than we can discuss. A fundamental problem is the efficient discovery of disjunctions of ranking functions [?]. We use backward analysis, as in [?,?], and our combination of conditional termination [?] with non-termination [?,?] is crucial. The approach of [?] is similar ours with a different refutation step and information exchange mechanism. At a high level, cdct is the dual of [?], which underapproximates non-terminating executions and overapproximates terminating ones, while we overapproximate non-termination and underapproximate termination. We believe cdct can be extended to transition-based approaches [?], but the challenge is to develop search and learning.

Example 2 .

 2 A concrete domain for forward analysis (P(State), ⊆, F ) is a lattice of states with a set F = {post c | c ∈ Cmd } of monotone functions called transformers, where post c (S) is the image of S under the transition relation for c. An abstract domain is a bounded lattice (A, , G, ) with a set of abstract transformers G = post A c | c ∈ Cmd and a widening operator : A × A → A. There is a monotone concretization function γ : A → P(State) satisfying that γ( ) = State and γ(⊥) = ∅. The transformers satisfy the soundness condition post c (γ(a)) ⊆ γ(post A c (a)) that abstract transformers overapproximate concrete transformers. Literals are essential for propagation and conflict analysis in sat. The analogue of literals in abstract domains are complementable meet-irreducibles [?]. A lattice element c is a meet-irreducible if a b = c implies that a = c or b = c. Let M A be the meet-irreducibles of A. An abstract element a has a concrete complement if there exists an a in A such that γ(a) = ¬γ(a). A meet decomposition of an element a is a finite set mdc(a) ⊆ M A satisfying that mdc(a) = a and that there is no strict subset S ⊂ mdc(a) with S = a. A has complementable meet irreducibles if every m ∈ M A has a concrete complement m ∈ M A . The interval lattice has elements [a, b], where a ≤ b

Algorithm 2 : 2

 22 Search() while true do Propagate() if tr (Xex) = ⊥ then return divergent d ← dec(Inf G , Ψ, tr ) if [tr ] [tr •d] then return unknown Xex:[-∞, 0], Xex:[0, ∞] {in, a, ex} Propagation 3a → Xin:[9, ∞] Xin:[0, ∞] dec Decision 4a Xa:[1, ∞] {a, in} Propagation 5a Xin:[-∞, 0] dec Decision 6a Xa:⊥ {a, in} Propagation 3b Xin:[-∞, -7] dec Decision 4b Xa:[-∞, -7], Xex:⊥ {a, in} Propagation

Lemma 1 .

 1 If (τ, σ) satisfies Inf G and Ψ and is in conc([tr ]), it is also in conc([tr ]) after invoking Propagate().

Fig. 4 :

 4 Fig. 4: Detailed comparison of FuncTion against its previous version [?] (a), AProVe [?] (b), HIPTnT+ [?] (c), and Ultimate Automizer [?] (d).

  | ∃i : Pos.Φ Trace formula A first-order interpretation (Val , I) defines functions I(f ) and relations I(P ) over values in Val . The value t s of a term t in a state s : Vars → Val , is s(x) if t is x, and I(f )( t 0 s , . . . , t n s ) if t is f (t 0 , . . . , t n ). The interpretation of a state formula is the standard first-order semantics. A transition formula is interpreted

at a transition, that is, a pair of states (r, s). A formula ϕ in which the symbol suc does not occur is interpreted at the state r, while suc(x) = t compares the value of the term t in r with the value of x in the successor state s.

(r, s) |= P (t 0 , . . . , t n ) if ( t 0 r , . . . , t n r

  also generates a blocking constraint if cdct cannot make progress analyzing [tr ]. This happens if no more decisions can be made and no ranking function can be extracted. cdct then backtracks if possible.

		Z s t e p ( Z x ) {
		i f ( x>20)
		return 3 ;
		e l s e i f ( x>10)
		return 2 ;
		e l s e
		return 1 ;
		}
		void main ( ) {
		y , i : Z
		[ a ] i f ( y>0)
		i = -s t e p ( y ) ;
		e l s e
	false then return (terminates, [ ], Θ)	i = s t e p (-y ) ; [ b ] while ( y < -3||y>3) y = y+i ;
		[ ex ] }

  The table alongside Alg. ?? illustrates the construction of tr and exp during interval analysis of the program in Fig.??. The exp column shows the locations of the propagated constraints. The rows 1, 2, 3a, 4a, 5a, 6a represent a run of Search(). The trail is initially empty and the result of standard interval analysis is the trailX ex :[-∞, 0], X ex :[0, ∞] in step 2, representing the assignment {X in → , X a → , X ex → [0, 0]}.An arbitrary decision X in :[9, ∞] in step 3a is not sound (see Ex. ??) and the smallest sound decision containing it is [0, ∞]. Propagation yields X a :[1, ∞] in step 4a. The decision X in :[-∞, 0] in step 5a is sound, and when propagated, yields a conflict in step 6a, so search returns unknown. An alternative run is 1, 2, 3b, 4b. A decision X in :[-∞, -7] is sound, and propagation yields X a :[-∞, -7] and X ex :⊥, so search returns divergent.

	Algorithm 4: Analyze()
	Algorithm 3: Propagate()
	asg ← [tr ]
	foreach S ∈ scc(Inf G ) do
	asg ← Reach(S, asg)
	foreach Xv:m ∈ mdiff (asg , asg)
	do
	tr ← tr •(Xv:m)
	foreach ψ ∈ Ψ do
	tr ← gunit(tr , ψ)

irreducible. A trail tr defines the assignment

[tr ]

where [ ] = λY. and [tr •(X:m)] maps X to [tr ](X) m and all other Y to [tr ](Y ). A trail tr is in potential/definite conflict with Φ if [tr ] is. We write tr (X) for [tr ](X). An explanation exp for a trail of length n is a function from [0, n -1] to constraints in Inf G or learnt clauses.

Search().

Alg. ?? extends a trail tr by propagating constraints from the cfg, making decisions, or applying a generalized unit rule. It returns divergent if tr (X ex ) is ⊥, meaning that ex is unreachable. It returns unknown if tr (X ex ) is not ⊥ and no decisions can be made. This trail is a potential conflict because every structure in conc([tr ]) with a non-empty assignment to X ex violates the constraint X ex (i) =⇒ Last(i), hence is a countermodel of Inf G .

Example 3.

  and is tr otherwise. The generalized unit rule refines a trail in the sense that [gunit(tr , Ψ )] [tr ]. If tr is inconsistent with Ψ , [tr ] will represent ⊥. Having presented all components of the procedure, we now investigate how it works in practice. Overview of the experimental evaluation.pdrf can be represented with intervals, octagons or convex polyhedra, and ranking functions within the pieces are represented by affine functions. The precision of the analysis can also be controlled by adjusting the widening delay.Experimental Evaluation. We evaluated our tool against 288 terminating C programs from the termination category of SV-COMP 2015. In particular, we compared FuncTion+cdct with other tools from the termination category of SV-

			Tot Time Timeouts		FuncTion+cdct
		FuncTion+cdct 200 1.5s	15		×
	(a)	AProVE [?] FuncTion [?] 175 0.7s 256 15.9s	24 5	(b)	AProVE [?] 15 71 185 FuncTion [?] 25 0 175	17 88
		HIPTnT+ [?] 246 1.2s	4		HIPTnT+ [?] 22 68 178	20
		Ultimate [?]	226 15.3s	35		Ultimate [?] 41 67 159	21
		Fig. 3:
	6 Implementation
	We have incorporated cdct in our prototype static analyzer FuncTion (http:
	//www.di.ens.fr/ ~urban/FuncTion.html), which is based on piecewise-defined
	ranking functions [?]. A version without cdct [?] participated in the 4th Inter-
	national Competition on Software Verification (SV-COMP 2015).
	FuncTion+cdct accepts (non-deterministic) programs in a C-like syntax.
	It is implemented in OCaml and uses the APRON library [?]. The pieces of a

COMP 2015 : AProVE [?], FuncTion without cdct [?], HIPTnT+ [?], and Ultimate Automizer [?]

be the concrete complement of [X v :m] in Asg A . Unsound decisions can be extended by propagation to a post-fixed point to cover all structures. All decisions on variables X v in singleton sccs with no self-loops are sound.

A decision rule dec(Inf G , Ψ, tr ) returns an abstract domain element d such that [tr •(X v :d)]

[tr ]. The decision rule makes progress if this order is strict. Unlike in sat the decision rule can cause divergence of cdct because an infinite series of decisions like [0, ∞], [1, ∞], . . . may not change result of propagation.

Conflict Analysis

Unlike sat and smt solvers, which generate definite conflicts, Search() generates potential conflicts. We apply backwards abstract interpretation with ranking functions to extract definite conflicts, and use widening to generalize them.

Ranking Function Domains. Due to space limitations, we only briefly recall the concrete domain of ranking functions, which provides the intuition for conflict analysis, and discuss the abstract domain informally. See [?,?] for details.

We write f : A B for a partial function whose domain is dom(f ). A ranking function f : State O for a relation R is a map from states to ordinals satisfying that for all s in dom(f ) and (s, t) in R, t is in dom(f ) and f (t) < f (s). A concrete domain for termination analysis (Rank , , B) is a lattice of ranking functions with backwards transformers B = {bkw c | c ∈ Cmd } defined below. Informally f g if f is defined on a state when g is and yields a lower rank: f g = dom(f ) ⊇ dom(g) and for all x in dom(g), f (x) < g(x). The transformer bkw c maps a ranking function f to one defined on states with all their successors in dom(f ). Recall that Rel c is the transition relation for a command c.

Let Fun ⊆ Rank be a lattice of functions, for example, affine functions. A piecewise defined ranking function (pdrf) over Fun and A is a set ρ = {a 1 → f 1 , . . . , a k → f k } such that {a 1 , . . . , a k } is an abstract partition, and each f i is in Fun. The abstract domain of pdrfs (aRank , , Abd ) is a lattice aRank with abduction transformers Abd . The concretization γ r : aRank → Rank of a ρ as above maps states to ranking functions:

The order and lattice operations are defined in terms of partition refinement and unification [?]. To compare ρ 1 and ρ 2 , we consider the coarsest abstract partition that refines the abstract partitions of both and compare the ranking functions in each block pointwise.

Conflict analysis starts with a precondition for termination and finds a weaker precondition for termination, hence performs abduction. The abduction transformers satisfy the soundness condition: γ r (abd c (ρ)) bkw c (γ r (ρ)), which states that the termination bounds obtained with pdrfs are weaker than those that


Carole Knibbe
email: carole.knibbe@inria.fr

Souvenirs from ECAL 2017: Create, play, experiment, discover -revealing the experimental power of virtual worlds

Seven plenary talks have been presented, covering a wide range of artificial life topics, related to the conference theme -"Create, play, experiment, discover: revealing the experimental power of virtual worlds". Indeed, one goal of the conference was to investigate the place of the experimental approaches within the artificial life field, both in terms of how we can use experimental results from chemistry, biology or social sciences, and in terms of how we experiment with our own artefacts.

1 Figure 1: ECAL 2017 cartoon by Nicolas Comte. 15 elements related to ECAL 2017 keynotes, topics and events are hidden in the cartoon, will you be able to find them all? André Brack, an astrobiologist from the Centre de Biophysique Moléculaire in Orléans, France, opened the conference with an introductory lecture on the chemical "automata" at the origin of life. With a communicative enthusiasm, he presented the insights yielded by the last space missions, on the possible sources of prebiotic carbon for example. He also introduced us to dilemma faced by chemists like singularity (very specific local conditions, allowing for a few births of life seeding the whole primitive ocean) vs ubiquity (widespread conditions allowing for spontaneous births of life everywhere). Another one is about the best method to try and recreate the origin of life: "classical", step-by-step predictive chemistry, or alchemist-style stochastic chemistry? The latter is a new approach developed in Orléans, where one submits a maximum of prebiotic ingredients under prebiotic conditions and lets the system run for months.

Bill Sellers, a computational zoologist from University of Manchester, United Kingdom, made an exciting lecture on synthetic palaeontology, or how to reconstruct ancient life by designing virtual robots. Bill insisted on the importance of calibrating the simulations with ground-truth data, which he obtained by filming animal locomotion in zoos with a specific video photogrammetry system.

He also stressed that multi-goals and multi-physics simulations are in order for better simulation outcomes. Indeed, when reconstructing locomotion, it is generally assumed that the animal is either attempting to maximise economy or speed, but in reality "the locomotor system in most animals is not a single function organ and it has to cope with a range of performances and their associated control and mechanical issues" [START_REF] Sellers | Synthetic palaeontology: Reconstructing ancient life using virtual robots[END_REF]). In a memorable example, he showed us that contrary to what was shown in the Jurassik Park movie, Tyrannosaurus rex likely could not run, because running would have generated unacceptably high skeletal loads [START_REF] Sellers | Investigating the running abilities of Tyrannosaurus rex using stressconstrained multibody dynamic analysis[END_REF].

Philippe Faure, a neurophysiologist from Université Pierre et Marie Curie, Paris, France, presented the original experimental approaches he develops in his lab to investigate the decision making process in animals and the underlying neurobiological mechanisms. He presented for example "Souris City", a socially enriched setup where mice are housed in larger groups than in standard conditions, and where they can explore several connected compartments, resembling the natural living conditions of mice. Such a setting allows to gather information on the hierarchical structure within a group, for example. Philippe also presented his recent results on the molecular basis of decision-making with uncertain rewards. By combining experiments and computational modeling, he showed that wild-type mice are motivated to explore zones with uncertain rewards (while mutant mice lacking a part of the nicotinic acetylcholine receptor are less inclined to do so). Those results are "consistent with theoretical work on optimal exploration and intrinsic motivation. In this view, exploration and exploitation are entangled: uncertainty is given a value that can be compared to and added to the value of primary rewards" [START_REF] Naudé | Nicotinic receptors in the ventral tegmental area promote uncertainty-seeking[END_REF].

Csaba Pál, a molecular evolutionary biologist from the Biological Research

Centre of the Hungarian Academy of Sciences, Szeged, Hungary, addressed the critical question of how complex adaptations can evolve. He argued that com-plex adaptations are prevalent in molecular systems, with for example the evolution of new protein functions involving multiresidue interactions or the evolution of multi-step metabolic pathways. He presented the latest insights brought by experimental evolution and systems biology. Protein evolution studies, for instance, do not support the non-adaptive theory that neutral or slightly deleterious mutations would prepare the ground for later beneficial mutations that lead to new, beneficial traits. An alternative, adaptive scenario is that complex molecular traits can readily evolve through series of adaptive steps if the environment is dynamically changing [START_REF] Pál | Evolution of complex adaptations[END_REF].

The lecture of Sabine Hauert, a roboticist from University of Bristol, United Kingdom, addressed the problem of scaling to large numbers of robots or nanoparticles in swarm engineering. We learned that scaling to thousands of robots requires shifting paradigm in the way swarm behavior is designed. She showed us how, by removing assumptions regarding precise control of robot motion, it is possible to deploy swarm behaviors on large amounts of uncalibrated robots performing random motion and simple local exchanges of information [START_REF] Crosscombe | Robust distributed decision-making in robot swarms: Exploiting a third truth state[END_REF]. When swarm engineering is used in the context of cancer treatment by nanoparticles, the problem of scaling is even more acute, since it typically involves trillions of particles without a controller. Predicting and engineering these collective behaviors is often counterintuitive. To help researchers develop a working intuition of these systems, she developed Nanodoc, a game to crowd-source nanomedicine, where users can see the simulated behaviour of nanoparticles in a virtual tumour and iteratively design or tweak the nanoparticle system dynamics [START_REF] Hauert | Swarm engineering across scales: From robots to nanomedicine[END_REF].

In a lecture directly related to the conference theme, Viola Schiaffonati, a philosopher of science from Politecnico di Milano, Italy, told us how experimenting with computing and in computing requires to stretch the traditional notion of controlled experiment. She introduced the notion of exploratory experiments, where simulation results are not only used to test or reject a theory, but also used to shape the theoretical model supporting them. By investigating autonomous robotics in particular, she found that such exploratory experiments can be "driven by the desire of investigating the realm of possibilities pertaining to the functioning of an artefact and its interaction with the environment in the absence of a proper theory or theoretical background. So hypotheses cannot be clearly stated and, even if the ultimate goal is to acquire knowledge about the performance of the artefacts under investigation and to find out proper concepts to formulate possible regularities, the experimenter is not in full control of the experimental setting due to the impossibility of anticipating all the plausible outcomes. Therefore, when experiments are explorative, control should be intended in a posteriori form, in opposition to the a priori form of the traditional experimental contexts. (...) [With exploratory experiments] the possibility of full anticipation disappears and control is in part carried out after the artefact has been inserted into society" [START_REF] Schiaffonati | Experimenting with computing and in computing: Stretching the traditional notion of experimentation[END_REF].

Last but not least, and because artificial life and art often inspire each other, Andreas Wessel-Therhorn, an animator and film director, and Laurent Pujo-Menjouet, a biomathematician and Disney enthusiast from Université Lyon 1, France, introduced us to the animation principles used to give the illusion of life. In a lecture that turned into a show with live demos, Andreas and Laurent walked us through the twelve principles established by Disney's "Nine Old Men" in the 1930s [START_REF] Thomas | Disney animation: The illusion of life[END_REF]. These principles -squash and stretch, anticipation, staging, straight ahead action and pose to pose, follow through and overlapping action, arcs, slow in and slow out, secondary action, timing, exaggeration, solid drawing, appeal -are still the basis for Western character animation today. Andreas and Laurent asked whether such principles could be used in robotics to build robots able to give the illusion of life in such a way that we could feel sympathetic to them.

With its 64 contributed talks (for a total of 131 submissions) and 23 contributed posters, ECAL showed the diversity of the Artificial Life community. Indeed, these contributions covered all the topics of Artificial Life, the most represented being (i) Evolutionary dynamics, (ii) Complex dynamical sys-tems and networks, (iii) Perception, cognition and behavior and (iv) Bioinspired robotics and embodied systems. The best paper award was granted to Nick Moran and Jordan Pollack, for their work on the "Effects of Cooperative and Competitive Coevolution on Complexity in a Linguistic Prediction Game" [START_REF] Moran | Effects of cooperative and competitive coevolution on complexity in a linguistic prediction game[END_REF]. The best poster award was granted to Peter Aaser and collaborators, for their work on "Towards Making a Cyborg: A Closed-Loop Reservoir-Neuro System" [START_REF] Aaser | Towards making a cyborg: A closed-loop reservoirneuro system[END_REF]. This clearly illustrates the intricacy between ALife and SAB topics and communities... The whole proceedings [START_REF] Knibbe | Proceedings of the Fourteenth European Conference Artificial Life, ECAL 2017[END_REF] are available in open access at MIT Press (http://cognet.mit.edu/journal/ecal2017).

In addition, six workshops and ten tutorials have been organized during the conference, the diversity of the topics illustrating the vitality of the field: Another memorable moment of this cruise was Steen Rasmussen sharing anecdotes and memories of three decades of artificial life conferences. Indeed, 2017 marks the 30th anniversary of the first Artificial Life Workshop, held at Los Alamos National Laboratory in 1987. 2017 also happened to be the ultimate edition of ECAL, this series of fourteen conferences held in Paris, Brussels, Granada, Brighton, Lausanne, Prague, Dortmund, Canterbury, Lisbon, Budapest, Taormina, York and finally Lyon. But this closure is not an end. The two alternating conferences, ECAL and Alife, will be merged in a single event, to be held every year. The end of ECAL is a new starting point for the community. Indeed, as one can immediately see it when looking at the conference proceedings, by its contributors, by its audience or by its scientific committee, ECAL was not an exclusively European event. It was a world-renowned conference series that attracted the best contributions in its field every other year, like ALife did in alternation. Hence the fusion of both events in a single format is just logical: Let us meet again in Tokyo at the 2018 Conference on Artificial Life, a hybrid of the European Conference on Artificial Life (ECAL) and the International Conference on the Synthesis and Simulation of Living Systems (ALife)!

-

  Social Learning and Cultural Evolution, -What can Synthetic Biology offer to (Embodied) Artificial Intelligence (and vice versa)? -Agency In The Physical Sciences, -Living Architecture. • Tutorials: -ISAL School, -Using MABE (Modular Agent Based Evolution), -Building Artificial Life Systems for the Web with Empirical, -Evolutionary Game Theory: Models and Applications, -Evolutionary Robotics -A practical guide to experiments with real hardware, -Evolution In The Cloud, -Simulating Complex Systems with FLAME GPU, -Avida-ED: a web-based, GUI implementation of the Avida software platform, for educational use, -Digital Coevolution: a beginners approach, -Evolution of Neural Networks. During the conference dinner on the Hermes boat on the Rhône and Saône rivers, the 2017 ISAL awards were granted to Jordan B. Pollack (Lifetime Achievement in the field of Artificial Life), Jean-Baptiste Mouret (Distinguished Young Investigator in the field of Artificial Life), Kenneth O. Stanley and Risto Miikkulainen (Outstanding Paper of the Decade 2002 -2012), Richard A. Watson and Eörs Szathmáry (Outstanding Paper of 2016 in the field of Artificial Life), Rob Pennock (Education and Outreach using Artificial Life) and René Doursat (Exceptional Service to the Artificial Life Community).

Acknowledgments

As the chair of the conference the author would like to thank all the institutional sponsors of ECAL 2017 (INRIA, CNRS, INSA-Lyon, Université Claude Bernard Lyon 1, Université Pierre et Marie Curie, Fédération Informatique de Lyon, Institut Rhône-Alpin des Systèmes Complexes), as well as the members of the program committee and the members of the ISAL board for their invaluable help. Needless to say, organizing a conference like ECAL requires lot of work, and this conference would not have been a success without the precious help of the organisation committee and numerous volunteers that I would like to warmly thank here: Guillaume Beslon, David Parsons, Dusan Misevic, Jonathan Rouzaud-Cornabas, Nicolas Bredèche, Salima Hassas, Olivier Simonin, Hédi Soula, Vincent Liard, Nicolas Comte, Charles Rocabert, Priscila Biller, Laurent Turpin, Caroline Lothe, Sophie Azzaro, Nicolas Nadisic and Audrey Denizot.

About the Author


Sami Hage-Ali
email: sami.hage-ali@univ-lorraine.fr

Omar Elmazria

Gaël Pierson

Richard Kouitat Njiwa

Thierry Aubert

Moïse Deroh

Florian Bartoli

Abdelkrim Talbi

Richard Kouitat

Packageless acoustic wave sensors for wireless body-centric applications

Keywords: Surface acoustic wave, waveguiding layer acoustic wave, sensor, wireless, packageless I

INTRODUCTION

Surface Acoustic Wave (SAW) devices are widely used as filters, resonators or delay lines in electronic systems for a wide range of applications: mobile communications, radars, as stable resonators for clock generation. The resonance frequency and the signal transmission delay of SAW devices may depend on the physical parameters of the environment, and SAW devices are increasingly used as sensors for a large variety of parameters: gas, pressure, force, temperature, strain, radiation, etc.

The SAW-based sensors have the advantage to be fully passive (battery-less) and can be interrogated using wireless techniques. That is why SAW devices are particularly useful in so-called "harsh" environments like radiative or high temperature environment [START_REF] Aubert | Wireless and batteryless surface acoustic wave sensors for high temperature environments[END_REF]. One can argue that the human body is also a harsh environment due the potential high acoustic and electromagnetic loss in wireless sensors.

In any case, the packaging of the SAW sensor is critical and often challenging. An elegant solution is to use "packageless" Waveguiding Layer Acoustic Wave (WLAW) devices [START_REF] Bhattacharjee | Packageless SAW Devices with Isolated Layer Acoustic Waves (ILAW) and Waveguiding Layer Acoustic Waves (WLAW)[END_REF][START_REF] Elmazria | AlN/ZnO/Diamond structure combining isolated and surface acoustic waves[END_REF][START_REF] Legrani | AlN/ZnO/Si Structure: a Packageless Solution for Acoustic Wave Sensors[END_REF][START_REF] Legrani | AlN/IDT/AlN/Sapphire as Packageless Structure for SAW Applications in Harsh Environments[END_REF][START_REF] Legrani | Deposition of Crack-Free 30 μm AlN on IDT/ZnO/Si for Wave Guiding Layer Acoustic Wave Applications[END_REF]. WLAW devices allow the confinement of the acoustic wave using a combination of low acoustic velocity layer stacked between two high acoustic velocity layers (See Fig. 1), thus removing the need of a bulky package.

In this communication, we study numerically and experimentally a Al 2 O 3 / ZnO/ LiNbO 3 (LN-128 Y-X cut) structure and investigate its use for body-centric applications, especially for "epidermal electronics", i.e. skinprinted electronics. In order to assess experimentally the confinement of the acoustic wave in a flexible/on-skin electronics context, we put the LN/ZnO/Al 2 O 3 structure in contact with Solaris [START_REF] Huang | Materials and Designs for Wireless Epidermal Sensors of Hydration and Strain[END_REF] (Smooth-On Inc., USA), a modified silicone elastomer that closely matches the mechanical properties of the skin (E Young = ~50 kPa). We investigated the increase of the insertion loss of a delay line across the spectrum in these conditions, to see if the presence of the elastomer generates additional losses. Alumina deposition by RF magnetron sputtering using a 4in Al target has been optimized to ensure maximum deposition speed (O 2 , 3.5 sccm, Ar 16.5 sccm , 2x10 -3 mbar), 300 W, no heating. The result is an amorphous layer (as confirmed by TEM and electron diffraction), with nanogranular structure. EDX analysis confirmed a 40% Al and 60% O 2 ratio, i.e. a perfect alumina stoichiometry.

A 8 µm alumina layer was deposited using these parameters. In order to open the connection pads for RF measurements, these were protected using AZ9260 photoresist and Kapton tape, which were removed after ZnO and Al 2 O 3 depositions.

The cross section SEM picture of the Al 2 O 3 /ZnO/Si control sample is shown in Fig. 3a and the final device is depicted in Fig. 3b. To get a clearer picture of the results, the modes/harmonics, insertion loss and the increase of the insertion loss between configurations are summarized in Table 1.

It appears that the wave is not confined at both fundamental frequencies of the two modes, since the contact with Solaris generate 6 to 8 dB additional loss. The wave at the 3 rd harmonic of the mode 0 at 1024 MHz seems more confined since the contact with Solaris adds only 2.1 dB.

More interesting is that the wave at the 3 rd harmonic of the "new" mode seems fully confined with virtually no change of insertion loss with added Solaris.

DISCUSSION, CONCLUSION AND PERSPECTIVES

Experimental evidence of a confined acoustic wave has been found in a LN/IDT/ZnO/Al 2 O 3 which is promising for on and intra-body acoustic wave sensors.

Additional modelling and elastic parameter measurements need to be performed.

Fig 1 :

 1 Fig 1: WLAW device principle. Adapted from [2]II. FEM MODELLING Initial modelling has been performed using a commercial FEM Software (Comsol Multiphysics v4.3b). We modeled a 2D infinite periodic interdigital transducer (IDT) and computed the particle displacements for a Al 2 O 3 (20µm) /ZnO (2µm)/ LN-128 structure (see Fig.2) in order to study its eligibility for WLAW operation. As we can see in Fig2b,the particle displacement at the surface of Al 2 O 3 (at 22 µm "height") is negligible, thus validating this structure numerically. However this alumina thickness is not very practical for experiments and we chose a thickness of 8 µm for Al 2 O 3 , expecting a dual operation: non-confined waves for the fundamental mode and confined waves for the higher order harmonics.

Fig. 2 :

 2 2) in order to study its eligibility for WLAW operation. As we can see in Fig 2b, the particle displacement at the surface of Al 2 O 3 (at 22 µm "height") is negligible, thus validating this structure numerically. However this alumina thickness is not very practical for experiments and we chose a thickness of 8 µm for Al 2 O 3 , expecting a dual operation: non-confined waves for the fundamental mode and confined waves for the higher order harmonics. Wave displacements in a Al 2 O 3 (20µm)/ ZnO (2µm)/LN-128 structure in 2D (a) and 1D (b) formats. The 0 µm reference is at the interface between LN and ZnO layers. III. MICROFABRICATION AND CHEMICAL / STRUCTURAL ANALYSIS A layer of 70 nm of aluminum was deposited on a LN-128 Y-X cut wafer by RF magnetron sputtering. A SAW delay line with 12 µm periodicity was patterned by photolithography using S1813 positive photoresist, and wet etching. 2 µm of ZnO were deposited using RF magnetron sputtering, a 4-in ZnO target and additional oxygen (O 2 8 sccm, Ar 8 sccm, 2x10 -3 mbar), 100°C, 100 W.

Fig 3 :Fig 4 :Fig. 4 (

 344 Fig 3: (a) Cross-section SEM picture of the Al 2 O 3 /ZnO/Si control sample (b) Fabricated delay line IV. EXPERIMENTAL RF CHARACTERIZATIONS The AW delay line was characterized using an Agilent 5061B network analyzer and SOLT calibration in 3 configurations: a: before ZnO and Al 2 O 3 depositions (regular SAW device) b: after ZnO and Al 2 O 3 depositions c: with added Solaris elastomer on top of it These configurations are depicted in Fig 4(i)

This work was supported partly by Région Lorraine and European FEDER funding (Appel d'Offre Région )

ACKNOWLEDGMENT

The authors would like to thank Sylvie Migot at Institut Jean Lamour for the TEM/EDX characterizations, as well as Laurent Badie and Gwladys Lengaigne at Minalor platform at Institut Jean Lamour for the help with the microfabrication.