Thomas Genet

Timothée Haudebourg

Thomas Jensen

Verifying Higher-Order Functions with Tree Automata

HAL is

Introduction

Higher-order functions are an integral feature of modern programming languages such as Java, Scala or JavaScript, not to mention Haskell and Caml. Higher-order functions are useful for program structuring but pose a challenge when it comes to reasoning about the correctness of programs that employ them. To this end, the correctness-minded software engineer can opt for proving properties interactively with the help of a proof assistant such as Coq [START_REF] Coq | The coq proof assistant reference manual: Version 8[END_REF] or Isabelle/HOL [START_REF] Paulson | The isabelle reference manual[END_REF], or write a specification in a formalism such as Liquid Types [START_REF] Rondon | Liquid types[END_REF] or Bounded Refinement Types [START_REF] Vazou | Abstract refinement types[END_REF][START_REF] Vazou | Bounded refinement types[END_REF] and ask an SMT solver whether it can prove the verification conditions generated from this specification. This approach requires expertise of the formal method used, and both the proof construction and the annotation phase can be time consuming.

Another approach is based on fully automated verification tools, where the proof is carried out automatically without annotations or intermediate lemmas. This approach is accessible to a larger class of programmers but applies to a more restricted class of program properties. The flow analysis of higher-order functions was studied by Jones [START_REF] Jones | Flow analysis of lazy higher-order functional programs[END_REF] who proposed to model higher-order functions as term rewriting systems and use regular grammars to approximate the result. More recently, the breakthrough results of Ong et al. [START_REF] Ong | On model-checking trees generated by higher-order recursion schemes[END_REF] and Kobayashi [START_REF] Kobayashi | Types and higher-order recursion schemes for verification of higherorder programs[END_REF][START_REF] Kobayashi | Predicate abstraction and CEGAR for higherorder model checking[END_REF][START_REF] Matsumoto | Automata-based abstraction for automated verification of higher-order tree-processing programs[END_REF] show that combining abstraction with model checking techniques can be used with success to analyse higher-order functions automatically. Their approach relies on abstraction for computing over-approximations of the set of reachable states, on which safety properties can then be verified.

In this paper, we pursue the goals of higher-order functional verification using an approach based on the original term rewriting models of Jones. We present a formal verification technique based on Tree Automata Completion (TAC) [START_REF] Genet | Equational approximations for tree automata completion[END_REF], capable of checking a class of properties, called regular properties, of higher-order programs in a fully automatic manner. In our approach, a program is represented as a term rewriting system R and the set of (possibly infinite) inputs to this program as a tree automaton A. The TAC algorithm computes a new automaton A * , by completing A with all terms reachable from A by R-rewriting. This automaton representation of the reachable terms contains all intermediate states as well as the final output of the program. Checking correctness properties of the program is then reduced to checking properties of the computed automaton. Moreover, our completion-based approach permits to certify automatically A * in Coq [START_REF] Boyer | Certifying a Tree Automata Completion Checker[END_REF], i.e. given A, R and A * , obtain the formal proof that A * recognizes all terms reachable from A by R-rewriting.

Example 1. The following term rewriting system R defines the filter function along with the two predicates even and odd on Peano's natural numbers. @(@(filter , p), cons(x, l)) → if @(p, x) then cons(x, @(@(filter , p), l)) else @(@(filter , p), l) @(@(filter , p), nil ) → nil @(even, 0) → true @(even, s(x)) → @(odd , x) @(odd , 0) → false @(odd , s(x)) → @(even, x)

This function returns the input list where all elements not satisfying the input boolean function p are filtered out. Variables are underlined and the special symbol @ denotes function application where @(f, x) means "x applied to f ".

We want to check that for all lists l of natural numbers, @(@(filter , odd ), l) filters out all even numbers. One way to do this is to write a higher-order predicate, exists, and check that there exists no even number in the resulting list, i.e. that @(@(exists, even), @(@(filter , odd ), l)) always rewrites to false. Let A be the tree automaton recognising terms of form @(@(exists, even), @(@(filter , odd ), l)) where l is any list of natural numbers. The completion algorithm computes an automaton A * recognising every term reachable from L(A) (the set of terms recognised by A) using R with the definition of the exists function. Formally,

L(A * ) = R * (L(A)) = {t | ∃s ∈ L(A), s → * R t}
To prove the expected property, it suffices to check that true is not reachable, i.e. true does not belong to the regular set L(A * ). We denote by regular properties the family of properties characterised by a regular set. In particular, regular properties do not count symbols in terms, nor relate subterm heights (a property comparing the length of the list before and after filter is not regular)

Termination of the tree automata completion algorithm is not ensured in general [START_REF] Genet | Termination criteria for tree automata completion[END_REF]. For instance, if R * (L(A)) is not regular, it cannot be represented as a tree automaton. In this case, the user can provide a set of equations that will force termination by introducing an approximation based on equational abstraction [START_REF] Meseguer | Equational abstractions[END_REF]: L(A * ) ⊇ R * (L(A)). Equations make TAC powerful enough to verify first-order functional programs [START_REF] Genet | Termination criteria for tree automata completion[END_REF]. However, state-of-the-art TAC has two short-comings. (i) Equations must be given by the user, which goes against full automation, and (ii) even with equations, termination is not guaranteed in the case of higher-order programs. In this paper we propose a solution to these shortcomings with the following contributions:

-We state and prove a general termination theorem for the Tree Automata Completion algorithm (Section 3); -From the conditions of the theorem we characterise a class of higher-order functional programs for which the completion algorithm terminates (Section 4). This class covers common usage of higher-order features in functional programming languages. -We define an algorithm that is able to automatically generate equations for enforcing convergence, thus avoiding any user intervention (Section 5).

All proofs missing in this paper can be found in the accompanying technical report [START_REF] Genet | Verifying higher-order functional programs with tree automata : Extended version[END_REF]. The paper is organised as follow: We describe the completion algorithm and how to use equations to ensure termination in Section 2. The technical contributions as described above are developed in Sections 3 to 5. In Section 6, we present a series of experiments validating our verification technique, and discuss the certification of results in Coq. We present related work in Section 7. Section 8 concludes the paper.

Background

This section introduces basic concepts used throughout the paper. We recall the usual definitions of term rewriting systems and tree automata, and present the completion algorithm which forms the basis of our verification technique.

Term rewriting and tree automata

Terms. An alphabet F is a finite set of symbols, with an arity function ar : F → N. Symbols represent constructors such as nil or cons, or functions such as filter , etc. For simplicity, we also write f ∈ F n when f ∈ F and ar(f ) = n.

For instance, cons ∈ F 2 and nil ∈ F 0 . An alphabet F and finite set of variables X induces a set of terms T (F, X ) such that:

x ∈ T (F, X ) ⇐ x ∈ X f (t 1 , . . . , t n ) ∈ T (F, X ) ⇐ f ∈ F n and t 1 , . . . , t n ∈ T (F, X )
A language is a set of terms. A term t is linear if the multiplicity of each variable in t is at most 1, and closed if it contains no variables. The set of closed terms is written T (F). A position in a term t is a word over N pointing to a subterm of t. Pos(t) is the set of positions in t, one for each subterm of t. It is defined by:

Pos(x) = {λ} Pos(f (t 1 , . . . , t n )) = {λ} ∪ {i.p | 1 ≤ i ≤ n ∧ p ∈ Pos(t i )}
where λ is the empty word and "." in i.p is the concatenation operator. For p ∈ Pos(t), we write t| p for the subterm of t at position p, and t[s] p for the term t where the subterm at position p has been replaced by s. We write s t if t is a subterm of s and s t if it is a subterm and s = t. If L ⊆ T (F), we write L for the language L and all its subterms. A substitution σ is an application of X → T (F, X ), mapping variables to terms. We tacitly extend it to the endomorphism σ : T (F, X ) → T (F, X ) where tσ is the result of the application of the term t to the substitution σ. Term rewriting systems [START_REF] Baader | Term Rewriting and All That[END_REF] provide a flexible way of defining functional programs and their semantics. A rewriting system is a pair F, R , where F is an alphabet and R a set of rewriting rules of the form l → r, where l, r ∈ T (F, X ), l ∈ X and Var (r) ⊆ Var (l). A TRS can be seen as a set of rules, each of them defining one step of computation. We write R a rewriting system F, R if there is no ambiguity on F. A rewriting rule l → r is said to be left-linear if the term l is linear. Example 1 shows a TRS representing a functional program, where each rule is left-linear. In that case we say that the TRS R is left-linear.

A rewriting system R induces a rewriting relation → R where for alls s, t ∈ T (F, X ), s → R t if it exists a rule l → r ∈ R, a position p ∈ Pos(s) and a substitution σ such that lσ = s| p and t = s[rσ] p . The reflexive-transitive closure of → R is written → * R . The rewriting system introduced in the previous example also derives a rewriting relation → R where @(@(f ilter, odd), cons(0, cons(s(0), nil))) → * R cons(s(0), nil)

The term cons(s(0), nil) is irreducible (no rule applies to it) and hence the result of the function call. We write IRR(R) for the set of irreducible terms of R.

Tree automata [START_REF] Comon | Tree automata techniques and applications[END_REF] are a convenient way to represent regular sets of terms. A tree automaton is a quadruple F, Q, Q f , ∆ where F is an alphabet, Q a finite set of states, Q f the set of final states, and ∆ a rewriting system on F ∪ Q. Rules in ∆, called transitions, are of the form l → q where q ∈ Q and l is either a state (∈ Q), or a configuration of the form f (q 1 , . . . , q n ) with f ∈ F, q 1 . . . q n ∈ Q. A term t is recognised by a state q ∈ Q if t → * ∆ q, which we also write t → * A q. We write L(A, q) for the language of all terms recognised by q. A term t is recognised by A if there exists q ∈ Q f s.t. t ∈ L(A, q). In that case we write t ∈ L(A). E.g., the tree automaton A = F, Q, Q f , ∆ with F = {0 : 0, s : 1}, Q f = {q pair } and ∆ = {0 → q pair , s(q odd ) → q pair , s(q pair ) → q odd , nil → q list , cons(q pair , q list ) → q list } recognises all lists of even natural numbers.

An -transition is a transition q → q where q ∈ Q. A tree automaton A is -free if it contains no -transitions. A is deterministic if for all terms t there is at most one state q such that t → * ∆ q . A is reduced if for all q there is at least one term t such that t → * ∆ q .

Tree Automata Completion algorithm

The verification algorithm is based on tree automata completion. Given a program represented as a rewriting system R, and its input represented as a tree automaton A 0 , the tree automata completion algorithm computes a new tree automaton A * recognising the set of all reachable terms starting from a term in L(A). For a given R, we write this set R * (L(A)) = {t | ∃s ∈ L(A), s → * R t}. It includes all intermediate computations and, in particular, the output of the functional program. The algorithm proceeds by computing iteratively A 1 , A 2 , . . .

such that A i+1 = C R (A i ) until it reaches a fix-point, A * .
Here, C R (A i ) represents one step of completion and is performed by searching and completing the critical pairs of

A i . lσ R / / * A i rσ q ⇒ lσ R / / A i+1 * rσ A i+1 *
n n q Definition 1 (Critical pair). A critical pair is a triple l → r, σ, q where l → r ∈ R, σ is a substitution, and q ∈ Q such that lσ → * A i q and rσ → * A i q. Completing a critical pair consists in adding the necessary transitions in A i+1 to have rσ → * A i+1 q, and hence rσ ∈ L(A i+1 , q). Example 2. Let A 0 be the previously defined tree automaton recognising all lists of even natural numbers. Let R = {s(s(x)) → s(x)}. A 0 has a critical pair s(s(x)) → s(x), σ, q pair with σ(x) = q pair . To complete the automaton, we need to add transition such that s(q pair ) → * A 1 q pair . Since we already have the state q odd recognising s(q pair ), we only add the transition q odd → q pair . The formal definition of the completion step, including the procedure of choosing which new transition to introduce, can be found in [START_REF] Genet | Verifying higher-order functional programs with tree automata : Extended version[END_REF].

Every completion step has the following property:

L(A i ) ⊆ L(A i+1 ) and s ∈ L(A i ) ⇒ s → R t ⇒ t ∈ L(A i+1 ) It implies that, if a fix-point A * then it recognises every term of R * (L(A)).
However it is in general impossible to compute a tree automaton recognising R * (L(A)) exactly, and this may cause the completion algorithm to diverge. Instead we shall over-approximate it by an automaton A * such that L(A * ) ⊇ R * (L(A)). The approximation is performed by introducing a set E of equations of the form l = r where l, r ∈ T (F, X ). From E we derive the relation = E , the smallest congruence such that for all equation l = r and substitution σ we have lσ = E rσ. In this paper we also write E for the TRS {l → r | l = r ∈ E}. At each completion step, the algorithm simplifies the automaton by merging states together according to E.

Definition 2 (Simplification Relation). Let

A = F, Q, Q f ,
∆ be a tree automaton and E be a set of equations. If s = t ∈ E, σ : X → Q, q, q ∈ Q such that sσ → * A q, tσ → * A q and q = q then A can be simplified into A = A{q → q} (where q has been substitued by q), denoted by A E A .

We write S E (A) for the unique automaton (up to renaming) A such that A * E A and A is irreducible by E . One completion step is now defined by

A i+1 = S E (C R (A i )). sσ E A i * tσ A i * q q ⇒ sσ E A i+1 * tσ A i+1 *
m m q Example 3. This example shows how using equations can lead to approximations in tree automata. Let A be the tree automaton defined by the set of transitions ∆ = {0 → q 0 , s(q 0 ) → q 1 }. This automaton recognises the two terms 0 in q 0 and s(0) (also known as 1) in q 1 . Let E = {s(x) = x} containing the equation that equates a number and its successor. For σ = {x → 0} we have s(x)σ → A q 1 , xσ → A q 0 and s(x)σ = E xσ. Then in S E (A), q 0 and q 1 are merged. The resulting automaton has transitions {0 → q 0 , s(q 0 ) → q 0 }, which recognises N in q 0 . The idea behind the simplification is to overapproximate R * (L(A)) when it is not regular. It has been shown in [START_REF] Genet | Termination criteria for tree automata completion[END_REF] that it is possible to tune the precision of the approximation. For a given TRS R, initial state automaton A and set of equations E, the termination of the completion algorithm is undecidable in general, even with the use of equations. Our contribution in this paper consists in finding a class of TRS/programs and equations E for which the completion algorithm with equations terminates.

Termination of Tree Automata Completion

In this section, we show that termination of the completion algorithm with a set of equations E is ensured under the following conditions: if (i) A k is reduced -free and deterministic (written REFD in the rest of the paper) for all k; (ii) every term of A k can be rewritten into a term of a given language L ⊆ T (F) using R (for instance if R is terminating); (iii) L has a finite number of equivalence classes w.r.t E. Completion is known to preserve -reduceness and -determinism if E ⊇ E r ∪ E R [START_REF] Genet | Termination criteria for tree automata completion[END_REF] where The contracting equations ensure that the completion algorithm will merge enough states during the simplification steps to terminate. Note that E c L cannot be empty, unless L is finite. To prove termination of completion, we first prove that it is possible to bound the number of states needed in A * to recognise a language L by the number of normal forms of L with respect to E c L . In our case L will be the set of output terms of the program. Since A * does not only recognises the output terms, we need additional states to recognise intermediate computation terms. In the proof of Theorem 1 we show that with E R , the simplification steps will merge the states recognising the intermediate computation with the states recognising the outputs. If the latter set of states is finite then we can show that A * is finite.

E R = {s = t | s → t ∈ R} and E r = {f (x 1 , . . . , x n ) = f (x 1 , . . . , x n ) | f ∈ F n }. Condition (i)
Theorem 1. Let A be an REFD tree automaton, R a left-linear TRS, E a set of equations and L a language closed by subterms such that for all k ∈ N and for all s ∈ L (A k ), there exists t

∈ L s.t. s → * R t. If E ⊇ E r ∪ E c L ∪ E R then the completion of A by R and E terminates with a REFD A * .

A Class of Analysable Programs

The next step is to identify a class of functional programs and a language L for which Theorem 1 applies. By choosing L = T (F) and providing a set of contracting equations E c T (F ) , the termination theorem above proves that the completion algorithm terminates on any functional program R. If this works in theory, in practice we want to avoid introducing equations over the application symbol (such as @(x, y) = y). Contracting equations on applications makes sense in certain cases, e.g., with idempotent functions (@(sort, @(sort, x)) = @(sort, x)), but in most cases, such equations dramatically lower the precision of the completion algorithm. Hence, we want to identify a language L with no contracting equations over @ in E c

L . Since such a language L still has to have a finite number of normal forms w.r.t. E c L (Theorem 1), it cannot include terms containing an un-bounded stack of applications. For instance, L cannot contain all the terms of the form @(f, x), @(f, @(f, x)), @(f, @(f, @(f, x)), etc. The @ stack must be bounded, even if the applications symbols are interleaved with other symbols (e.g. @(f, s(@(f, s(@(f, s(x))))))). To do that we (i) define a set B d of all terms where such stack size is bounded by d ∈ N; (ii) define a set K n and a class of TRS called K-TRS such that for any TRS R in this class, K n is closed by R and K n ∩ IRR(R) ⊆ B φ(n) . This is done by first introducing a type system over the terms; (iii) finally define L = B φ(n) ∩ IRR(R) that can be used to instantiate Theorem 1.

Definition 4. For a given alphabet F = C ∪ {@}, B d is the set of terms where every application depth is bounded by d. It is the smallest set defined by:

f ∈ B 0 ⇐ f ∈ C 0 f (t 1 , . . . , t n ) ∈ B i ⇐ f ∈ C n ∧ t 1 . . . t n ∈ B i @(t 1 , t 2 ) ∈ B i+1 ⇐ t 1 , t 2 ∈ B i t ∈ B i+1 ⇐ t ∈ B i
In Section 5, we show how to produce E c such that B d ∩ IRR(R) has a finite number of normal forms w.r.t. E c with no equations on @. However we don't have for all k, for all term

t ∈ L (A k ) a term s ∈ B d ∩ IRR(R) s.t. t → * R s in general. Theorem 1 cannot be instantiated with L = B d ∩ IRR(R). Instead we define (i) a set K n ⊆ T (F) and φ such that K n ∩ IRR(R) ⊆ B φ(d)
and (ii) a class of TRS, called K-TRS for which L (A k ) ⊆ K n . In K-TRS, the right hand sides of TRS rules are contained in a set K whose purpose is to forbid the construction of unbounded partial applications during rewriting. If the initial automaton satisfies L (A) ⊆ K n then we can instantiate Theorem 1 with L = K n ∩ IRR(R) and prove termination.

Types

In order to define K and K n we require the TRS to be well-typed. Our definition of types is inspired by [START_REF] Baader | Term Rewriting and All That[END_REF]. Let A be a non-empty set of algebraic types. The set of types T is inductively defined as the least set containing A and all function types, i.e. A → B ∈ T ⇐ A, B ∈ T . The function type constructor → is assumed to be right-associative. The arity of a type A is inductively defined on the structure of A by:

ar(A) = 0 ⇐ A ∈ A ar(A → B) = 1 + ar(B) ⇐ A → B ∈ T
Instead of using alphabets, in a typed terms environment we use signatures F = C ∪ {@} where C is a set of constructor symbols associated to a unique type and @ the application symbol (with no type). We also assign a type to every variable. We write f : A if the symbol f has type A and t : A a term t ∈ T (F, X ) of type A. We write W(F, X ) for the set of all well typed terms using the usual definition. We extend the definition of term rewriting systems to typed TRS. A TRS is well typed if all rules are of the form l : A → r : A (type is preserved). In the same way, an equation s = t is well typed if both s and t have the same type. In the rest of this paper we only consider well typed equations and TRSs.

Definition 5 (Functional TRS). A higher-order functional TRS is composed of rules of the form @(. . . @(f, t 1 : A 1 ) . . . , t n :

A n ) : A → r : A where f : A 1 → . . . → A n → A ∈ C n , t 1 . . . t n ∈ W(C, X
) and r ∈ W(F, X ). A functional TRS is complete if for all term t = @(t 1 , t 2 ) : A such that ar(A) = 0, it is possible to rewrite t using R. In other words, all defined functions are total.

Types provides information about how a term can be rewritten. For instance we expect the term @(f : A → B, x : A) : B to be rewritten by every complete (no partial function) TRS R if ar(A → B) = 1. Furthermore, for certain types, we can guarantee the absence of partial applications in the result of a computation using the type's order. For a given signature F, the order of a type A, written ord(A), is inductively defined on the structure of A by:

ord(A) = max{ord(f ) | f : • • • → A ∈ C n } ord(A → B) = max{ord(A) + 1, ord(B)}
where ord(f : A 1 → . . . → A n → A) = max{ord(A 1 ), . . . , ord(A n )} (with, for A i = A, ord(A i ) = 0). For instance ord(int) = 0 and ord(int → int) = 1.

Example 5. Define two different types of lists list and list . The first defines lists of int with the constructor consA : int → list → list ∈ C, while the second defines lists of functions with the constructor consB : (int → int) → list → list ∈ C. The importance of order becomes manifest here: in the first case a fully reduced term of type list cannot contain any @ whereas in the second case it can. ord(list) = 0 and ord(list ) = 1.

Lemma 1. If R is a complete functional TRS and A a type such that ord(A) = 0, then all closed terms t of type A are rewritten into an irreducible term with no partial application:

∀s ∈ IRR(R), t → * R s ⇒ s ∈ B 0 .

The class K-TRS

Recall that we want to define (i) a set K n ⊆ T (F) and φ such that K n ∩IRR(R) ⊆ B φ(n) and (ii) a class of TRS K-TRS for which L (A k ) ⊆ K n . Assuming that L (A) ⊆ K n we instantiate Theorem 1 with L = K n ∩ IRR(R) and prove termination.

Definition 6 (K-TRS).

A TRS R is part of K-TRS if for all rules l → r ∈ R, r ∈ K where K is inductively defined by:

x : A ∈ K ⇐ x : A ∈ X f (t 1 , . . . , t n ) : A ∈ K ⇐ f ∈ C n ∧ t 1 , . . . , t n ∈ K @(t 1 : A → B, t 2 : A) : B ∈ K ⇐ t 1 ∈ Z, t 2 ∈ K ∧ B ∈ A (1)
@(t 1 : A → B, t 2 : A) : B ∈ K ⇐ t 1 , t 2 ∈ K ∧ ord(A) = 0 (2)
with Z defined by:

t ∈ Z ⇐ t ∈ K @(t 1 , t 2 ) ∈ Z ⇐ t 1 ∈ Z, t 2 ∈ K
By constraining the form of the right hand side of each rule of R, K defines a set of TRS that cannot construct unbounded partial applications during rewriting. The definition of K takes advantage of the type structure and Lemma 1. The rules (1) and (2) ensure that an application @(t 1 , t 2 ) is either: (1) a total application, and the whole term can be rewritten; or (2) a partial application where t 2 can be rewritten into a term of B 0 (Lemma 1). In (1), Z allows partial applications inside the total application of a multi-parameter function.

Example 6. Consider the classical map function. A typical call to this function is @(@(map, f ), l) of type list, where f is a mapping function, and l a list. The whole term belongs to K because of rule (1): list is an algebraic type and its subterm @(map, f ) : list → list belongs to Z. This subterm is a partial application, but there is no risk of stacking partial applications as it is part of a complete call (to the map function).

Example 7. Consider the function stack defined by: @(@(stack, x), 0) → x @(@(stack, x), S(n)) → @(@(stack, @(g, x)), n)

Here g is a function of type (A → A) → A → A. The stack function returns a stack of partial applications whose height is equal to the input parameter: @(@(stack, f ), S(S(S . . . S k (0) . . . ))) → * R @(g, @(g, @(g, . . . @(g

k , f ) . . . )))
The depth of partial applications stacks in the output language is not bounded. With no equations on the @ symbol, the completion algorithm may not terminate. Notice that x is a function and @(g, x) a partial application. Hence the term @(@(stack, @(g, x)), n) is not in K, so the TRS does not belong to the K-TRS class.

We define K n as {tσ | t ∈ K, σ : X → B n ∩ IRR(R)} and claim that if for all rule l → r of the functional TRS R, r ∈ K and if L(A) ⊆ K n then with Theorem 1 we can prove that the completion of A with R terminates. The idea is the following:

-Prove that if A recognises terms of K n , then it is preserved by completion using the notion of

K n -coherence of A. -Prove that K n ∩ IRR(R) ⊆ B n+2B ∩ IRR(R) where B ∈ N is a fixed upper
bound of the arity of all the types of the program. -Prove that there is a finite number of normal form of

B n+2B ∩ IRR(R) w.r.t E c L .
-Finally, we use those three properties combined, and instantiate Theorem 1 with L = B n+2B ∩ IRR(R) to prove Theorem 2, defined as follows.

Theorem 2. Let A be a K n -coherent REFD tree automaton, R a terminating functional TRS such that for all rule l → r ∈ R, r ∈ K and E a set of equations.

Let L = B n+2B ∩ IRR(R). If E = E r ∪ E c L ∪ E R then the completion of A by R and E terminates.
To prove that after each step of completion, the recognised language stays in K n , we require the considered automaton to be K n -coherent.

Definition 7 (K n -coherence). Let L ⊆ W(F) and n ∈ N. L is K n -coherent if L ⊆ K n ∨ L ⊆ Z n \ K n

By extension we say that a tree-automaton

A = F, Q, Q f , ∆ is K n -coherent if the language recognised by all states q ∈ Q is K n -coherent.
If K n -coherence is not preserved during completion, then some states in the completed automaton may recognise terms outside of K n . Our goal is to show that it is preserved by C R (•) (Lemma 2) then by S E (•) (Lemma 3).

Lemma 2 (C R (A) preserves K n -coherence). Let A be a REFD tree automa- ton. If A is K n -coherent, then C R (A) is K n -coherent.
Lemma 3 (S E (A) preserves K n -coherence). Let A be a REFD tree automaton, R a functional TRS and E a set of equations such that

E = E r ∪ E c L ∪ E R with L = B n+2B ∩ IRR(R). If A is K n -coherent then S E (A) is K n -coherent.
By using Lemma 2 and Lemma 3, we can prove that the completion algorithm, which is a composition of C R (A) and S E (A), preserves K n -coherence. The proofs of these two lemmas are based on a detailed analysis of the completion algorithm itself. The complete proofs are provided in [START_REF] Genet | Verifying higher-order functional programs with tree automata : Extended version[END_REF].

Lemma 4 (Completion preserves K n -coherence). Let A = F, Q, Q f , ∆ be a tree automaton, R a functional TRS and E a set of equations.

If E = E r ∪ E c L ∪ E R with L = B n+2B ∩ IRR(R) and A is K n -coherent then for all k ∈ N, A k is K n -coherent. In particular, A * is K n -coherent.
By construction we can prove that the depth of irreducible K n terms is bounded, which correspond to the following lemma.

Lemma 5. For all t : T ∈ K n , t : T ∈ IRR(R) ⇒ t : T ∈ B n+2B-arity(T ) .

Proof of Theorem 2

Proof. According to Lemma 4, for all k ∈ N, the completed automaton A k is K n -coherent. By definition this implies that L (A k ) ⊆ K n . Moreover, we know that IRR(R) ∩ K n ⊆ B n+2B (Lemma 5). Let L = B n+2B ∩ IRR(R). R is terminating, so for every term s ∈ L (A k ) there exists t ∈ L such that s → * R t. Since the number of normal form of L is finite w.r.t E, Theorem 1 implies that the completion of A by R and E terminates.

Theorem 2 states a number of hypotheses that must be satisfied in order to guarantee termination of the completion algorithm:

-The initial automaton A must be K n -coherent and REFD.

-R must be terminating.

-All left-hand sides of rules of R are in the set of terms K. This is a straightforward syntactic check. If it is not verified, we can reject the TRS before starting the completion. -The set of equations E must be of the form E r ∪ E c

L ∪ E R . The equation sets E r and E R are determined directly from the syntactic structure of R. However, there is no unique suitable set of contracting equations E c L . This set must be generated carefully, because a bad choice of contracting equations (i.e., equations that equate too many terms) will have a severe negative impact on the precision of the analysis result.

In this section, we describe a method for generating all possible sets of contracting equations E c L . To simplify the presentation, we only present the case where L = W(C) and IRR(R) ⊆ W(C) (i.e., all results are first-order terms). Our approach looks for contracting equations for the set of closed terms W(C) instead of the set B n+2B mentioned in Theorem 2. More precisely, we generate the set of equations iteratively, as a series of equation sets E k c where the equations only equate terms of depth at most k. Recall that a contracting equation is of the form u = u| p with p = λ, i.e., it equates a term with a strict subterm of the same type. A set of contracting equations over the set W(C) is then generated as follows: (i) generate the set of left-hand side of equations as a covering set of terms [START_REF] Kounalis | Testing for the ground (co-)reducibility property in term-rewriting systems[END_REF], so that for each term t ∈ W(C) there exists a left-hand side u of an equation and a substitution σ such that t = uσ. (ii) for each left-hand side, generate all possible equations of the form u = u| p , satisfying that both sides have the same type. (iii) from all those equations, we build all possible E c L (with

L = W(C)) such that the set of normal forms of W(C) w.r.t. E c L is finite. Since E c
L is left-linear and L = W(C), this can be decided efficiently [START_REF] Comon | Sequentiality, Monadic Second-Order Logic and Tree Automata[END_REF].

Example 8. Assume that C = {0 : 0, s : 1}.. For k = 1, the covering set is {s(x), 0} and E 1 c = {{s(x) = x}}. For depth 2, the covering set is {s(s(x)), s(0), 0} and

E 2 c = E 1 c ∪ {{s(s(x)) = x}, {s(s(x)) = s(x)}, {s(0) = 0}, {s(0) = 0, s(s(x)) = x}, {s(0) = 0, s(s(x)) = s(x)}}. All equation sets of E 1
c and E 2 c satisfy Definition 3 and lead to different approximations.

To verify a property ϕ on a program, we use completion and equation generation as follows. The program is represented by a TRS R and function calls are represented by an initial tree automaton A. Both have to respect the hypothesis of Theorem 2. The algorithm searches for a set of contracting equations E c such that verification succeeds, i.e. L(A * ) satisfy ϕ. Starting from k = 1, we apply the following algorithm:

1. We first complete the tree automaton A k recognising the finite subset of L(A) of terms of maximum depth k. Since L(A k ) is finite and R is terminating, the set of reachable terms is finite, completion terminates without equations and computes an automaton A * k recognising exactly the set R * (L(A k )) [START_REF] Genet | Equational approximations for tree automata completion[END_REF]. If there exists a set of equations E c able to verify the program, this algorithm will find it eventually, or find a counter example. However if there is no set of equations that can verify the program, this algorithm does not terminate.

Experiments

The verification technique described above has been integrated in the Timbuk library [START_REF] Genet | Reachability Analysis and Tree Automata Calculations[END_REF]. We implemented the naive equation generation where all possible equation sets E c are enumerated. Despite the evident scalability issues of this simple version of the verification algorithm, we have been able to verify a series of properties of several classical higher-order functions: map, filter , exists, forall , foldRight, foldLeft as well as higher-order sorting functions parameterised by an ordering function. Most examples are taken from or inspired by [START_REF] Ong | Verifying higher-order functional programs with patternmatching algebraic data types[END_REF][START_REF] Matsumoto | Automata-based abstraction for automated verification of higher-order tree-processing programs[END_REF] and have corresponding TRSs in the K set defined above. The property ϕ consists in checking that a finite set of forbidden terms is not reachable (Patterns section of Timbuk specifications).

Given A, R and A * , the correctness of the verification, i.e. the fact that L(A * ) ⊇ R * (L(A)), can be checked in a proof assistant embedding a formalisation of rewriting and tree automata. It is enough to prove that (a) L(A * ) ⊇ L(A) and that (b) for all critical pairs l → r, σ, q of A * we have rσ → * A * q. Property (a) can be checked using standard algorithms on tree automata. Property (b) can be checked by enumerating all critical pairs of A * (there are finitely many) and by proving that all of them satisfy rσ → * A * q. Since there exists algorithms for checking properties (a) and (b), the complete proof of correctness can automatically be built in the proof assistant. For instance, the automaton A * can be used as a certificate to build the correctness proof in Coq [START_REF] Boyer | Certifying a Tree Automata Completion Checker[END_REF] and in Isabelle/HOL [START_REF] Felgenhauer | Reachability, confluence, and termination analysis with state-compatible automata[END_REF]. It is also used to build unreachability proofs in Isabelle/HOL [START_REF] Felgenhauer | Reachability, confluence, and termination analysis with state-compatible automata[END_REF]. Besides, since verifying (a) and (b) is automatic, the correctness proof may be run outside of the proof assistant (in a more efficient way) using a formally verified external checker extracted from the formalisation. All our (successful) completion attempts output a comp.res file, containing A, R and A * , which has been certified automatically using the external certified checker of [START_REF] Boyer | Certifying a Tree Automata Completion Checker[END_REF]. Timbuk's site http://people.irisa.fr/Thomas.Genet/ timbuk/funExperiments/ lists those verification experiments. Nine of them are automatically proven. Two other examples show that correct counter-examples are generated when the property is not provable. On one example equation generation times out due to our naïve enumeration of equations. For this last case, by providing the right set of equations in mapTree2NoGen the verification of the function succeeds.

Related Work

When it comes to verifying first-order imperative programs, there exist several successful tools based on abstract interpretation such as ASTREE [START_REF] Blanchet | A static analyzer for large safety-critical software[END_REF] and SLAM [START_REF] Ball | The SLAM project: debugging system software via static analysis[END_REF]. The use of abstract interpretation for verifying higher-order functional programs has comparatively received less attention. The tree automaton completion technique is one analysis technique able to verify first-order Java programs [START_REF] Boichut | Rewriting Approximations for Fast Prototyping of Static Analyzers[END_REF]. Until now, the completion algorithm was guaranteed to terminate only in the case of first-order functional programs [START_REF] Genet | Termination criteria for tree automata completion[END_REF].

Liquid Types [START_REF] Rondon | Liquid types[END_REF], followed by Bounded Refinement Types [START_REF] Vazou | Abstract refinement types[END_REF][START_REF] Vazou | Bounded refinement types[END_REF], and also Set-Theoretic Types [START_REF] Castagna | Polymorphic functions with set-theoretic types: part 1: syntax, semantics, and evaluation[END_REF][START_REF] Castagna | Polymorphic functions with settheoretic types: part 2: local type inference and type reconstruction[END_REF], are all attempts to enrich the type system of functional languages to prove non-trivial properties on higher-order programs. However, these methods are not automatic. The user has to express the property he wants to prove using the type system, which can be tedious and/or difficult. In some cases, the user even has to specify straightforward intermediate lemmas to help the type checker.

The first attempt in verifying regular properties came with Jones [START_REF] Jones | Flow analysis of lazy higher-order functional programs[END_REF] and Jones and Andersen [START_REF] Jones | Flow analysis of lazy higher-order functional programs[END_REF]. Their technique computes a grammar over-approximating the set of states reachable by a rewriting systems. However, their approximation is fixed and too rough to prove programs like Example 1 (filter odd). Our program and property models are close to those of Jones and Andersen. However, the approximation in our analysis is not fixed and can be automatically adapted to the verification objective.

Ong et al. proposes one way of addressing the precision issue of Jones and Andersen's approach using a model checking technique on Pattern Matching Recursion Schemes [START_REF] Ong | Verifying higher-order functional programs with patternmatching algebraic data types[END_REF] (PMRS). This technique improves the precision but is still not able to verify functions such as Example 1 (see [START_REF] Salmon | Analyse d'atteignabilité pour les programmes fonctionnels avec stratégie d'évaluation en profondeur[END_REF] page 85). As shown in our experiments, our technique handles this example.

Kobayashi et al. developed a tree automata-based technique [START_REF] Matsumoto | Automata-based abstraction for automated verification of higher-order tree-processing programs[END_REF] (but not relying on TRS and completion), able to verify regular properties (including safety properties on Example 1). We have verified a selection of examples coming from [START_REF] Matsumoto | Automata-based abstraction for automated verification of higher-order tree-processing programs[END_REF] and observed that we can verify the same regular properties as they can. Our prototype implementation is inferior in terms of execution time, due to the slow generation of equations. A strength of our approach is that our verification results are certifiable and that they can be used as certificates to build unreachability proofs in proof assistants (see Section 6).

Our verification framework is based on regular abstractions and uses a simple abstraction mechanism based on equations. Regular abstractions are less expressive than Higher-Order Recursion Schemes [START_REF] Ong | On model-checking trees generated by higher-order recursion schemes[END_REF][START_REF] Kobayashi | Types and higher-order recursion schemes for verification of higherorder programs[END_REF] or Collapsible Pushdown Au-tomata [START_REF] Broadbent | C-shore: a collapsible approach to higher-order verification[END_REF], and equation-based abstractions are a particular case of predicate abstraction [START_REF] Kobayashi | Predicate abstraction and CEGAR for higherorder model checking[END_REF]. However, the two restrictions imposed in this particular framework result in two strong benefits. First, the precision of the approximation is formally defined and precisely controlled using equations: L(A * ) ⊆ (R/E) * (L(A)) [START_REF] Genet | Equational approximations for tree automata completion[END_REF]. This precision property permits us to prove intricate properties with simple (regular) abstractions. Second, using tree automata-based models facilitates the certification of the verification results in a proof assistant. This significantly increases the confidence in the verification result compared e.g., to verdicts obtained by complex CEGAR-based model-checkers.

Conclusion & Future Work

This paper shows that tree automata completion is a simple yet powerful, fully automatic verification technique for higher-order functional programs, expressed as term rewriting systems. We have proved that the completion algorithm terminates on a subset of TRS encompassing common functional programs, and provided experimental evidence of the viability of the approach by verifying properties on fundamental higher-order functions including filtering and sorting.

One remaining question is whether this approach is complete: if there exists a regular approximation of the reachable terms of a functional program, can we build it using equations? We can already answered this question in the positive when L = W(C), i.e., all results are first order terms [START_REF] Genet | Automata Completion and Regularity Preservation[END_REF]. Extending this result to all kind of results, including higher-order ones, is a promising research topic.

The generation of the approximating equations is automatic but simpleminded, and too simple to turn the prototype into a full verification tool. Further work will look into how sets of contracting equations can be generated in a more efficient manner, notably by taking the structure of the TRS into account and using a CEGAR approach.

The present verification technique is agnostic to the evaluation strategy. An interesting research track would be to experiment completion-based verification techniques with different term rewriting semantics of functional programs such as outlined by Clemente et al. [START_REF] Clemente | Ordered tree-pushdown systems[END_REF]. This would permit us to take a particular evaluation strategy into account, and in certain cases, improve the precision of the verification. We already experimented with this in [START_REF] Genet | Reachability Analysis of Innermost Rewriting -extended version[END_REF]. This is in line with our long-term research goal of providing a light-weight verification tool to assist the working OCaml programmer.

Our work focuses on verifying regular properties represented by tree automata. Dealing with non-regular over-approximations of reachable terms would allow us to verify relational properties like comparing the length of the list before and after f ilter. This is one of the objective of techniques like [START_REF] Kobayashi | Predicate abstraction and CEGAR for higherorder model checking[END_REF]. Building non-regular over-approximations of reachable terms for TRS, using a form of completion, is possible [START_REF] Boichut | Towards more precise rewriting approximations[END_REF]. However, up to now, adapting automatically the precision of such approximations to a given verification goal is not possible. Extending their approach with equations may provide a powerful verification tool worth pursuing.

  is ensured by showing that, in our verification setting, completion preserve REFD. The last condition is ensured by having E ⊇ E cL where E c L is a set of contracting equations.Definition 3 (Contracting Equations). Let L ⊆ T (F).A set of equations is contracting for L, denoted by E c L , if all equations of E c L are of the form u = u| p with u a linear term of T (F, X ), p = λ and if the set of normal forms of L w.r.t the TRS E c L = {u → u| p | u = u| p ∈ E c L } is finite. Example 4. Assume that F = {0 : 0, s : 1}. The set E c L = {s(x) = x} is contracting for L = T (F) because the set of normal forms of T (F) with respect to E c L = {s(x) → x} is the (finite) set {0}. The set E c L = {s(s(x)) = x} is contracting because the normal forms of {s(s(x)) → x} are {0, s(0)}.

2 .

 2 If L(A * k ) does not satisfy ϕ then verification fails: a counterexample is found. 3. Otherwise, we search for a suitable set E c . All E c of E k c that introduce a counterexample in the completion of A k with R and E c are filtered out.[START_REF] Boichut | Rewriting Approximations for Fast Prototyping of Static Analyzers[END_REF]. Then for all remaining E c , we try to complete A with R andE = E r ∪E R ∪E cand check ϕ on the completed automaton. If ϕ is true on A * then verification succeeds. Otherwise, we try the next E c . 5. If there remain no E c , we start again with k = k + 1.


Thomas Genet

Tristan Gillard

Timothée Haudebourg

Sébastien Lê Cong

Extending Timbuk to Verify Functional Programs

Timbuk implements the Tree Automata Completion algorithm whose purpose is to over-approximate sets of terms reachable by a term rewriting system. Completion is parameterized by a set of equations defining which terms are equated in the approximation. In this paper we present two extensions of Timbuk which permit us to automatically verify safety properties on functional programs. The first extension is a language, based on regular tree expressions, which eases the specification of the property to prove on the program. The second extension automatically generates a set of equations adapted to the property to prove on the program.

Motivations

. In this paper we focus on static analysis of safety properties on functional programs. Let us illustrate this on a simple example. Assume that we want to analyze the following delete OCaml function: let rec delete x l= match l with

In Timbuk [START_REF] Genet | Timbuk 3.2 -a Tree Automata Library[END_REF], this program will be translated in the following TRS, where ite encodes the if-then-else construction and eq encodes a simple equality on two arbitrary constant symbols A and B. The Ops section defines the symbols with their arity, the Const section defines the constructor symbols (symbols that are not associated with a function), the Vars section defines variables and the TRS section associates the name of the TRS with its rules. In the following, we denote by F the set of symbols defined in the Ops section and T (F) the set of ground terms built on F. We denote by C the set of constructor symbols defined by Const, and T (C) the set of ground terms defined on C.

Ops delete:2 cons:2 nil:0 A:0 B:0 ite:3 true:0 false:0 eq:2 Const A B nil cons true false Vars X Y Z TRS R delete(X,nil)->nil delete(X,cons(Y,Z))->ite(eq(X,Y),delete(X,Z),cons(Y,delete(X,Z))) ite(true,X,Y)->X ite(false,X,Y)->Y eq(A,A)->true eq(A,B)->false eq(B,A)->false eq(B,B)->true

Let us denote by L the set of all possible lists of A's and B's. On this program, we are interested in proving that for all l ∈ L, delete(A,l) can only result into a list where A does not occur. This is equivalent to proving that for all l∈ L, delete(A,l) never rewrites to a list containing an A. This can be done using reachability analysis on rewriting with the above TRS R. We denote by I the set of all initial terms, i.e., I = {delete(A, l) | l ∈ L} and let Bad be the set of lists containing at least one A. We denote by R * (I) the set of terms reachable by rewriting terms of I with R, i.e., R * (I) = {t | s ∈ I and s → R * t}, where → R * is the reflexive and transitive closure of → R . If R * (I) ∩ Bad = ∅ then there is no way to rewrite a term of the form delete(A,l) with l∈ L into a list containing an A and the property is also true on the functional program. Note that the property proved on the TRS is stronger than the property proved on the functional program. In particular, it is independent of the evaluation strategy: it can be call-by-value as well as call-by-name. Thus, the property is true for OCaml as well as for Haskell programs. 1 This paper presents two extensions of Timbuk making the above analysis possible and automatic.

-The first extension are simplified regular tree expressions which let the user easily and intuitively define the set of initial terms I. -The second extension automatically generates abstraction equations, using algorithms described in [START_REF] Genet | Verifying higher-order functions with tree automata[END_REF] and [START_REF] Genet | Automata Completion and Regularity Preservation[END_REF]. This makes it possible to automatically build a regular over-approximation App of R * (I) such that App ∩ Bad = ∅, if it exists.

In Section 2, we define simplified regular expressions. In Section 3, we explain why abstraction equations are necessary and we show how to generate them in Section 4. In Section 5, we show how to interact with Timbuk in order to carry out a complete analysis, as the one shown above. Finally, in Section 6, we conclude and give further research directions.

Simplified regular tree expressions

We defined the TRS but we still need to define the set of initial terms I in Timbuk. Until now, it could only be defined using a tree automaton [START_REF] Comon | Tree Automata Techniques and Applications[END_REF]. Defining I with this formalism is possible but it is error-prone and lacks readability. As in the case of word languages, there exists an alternative representation for regular tree languages: regular tree expressions [START_REF] Comon | Tree Automata Techniques and Applications[END_REF]. However, unlike classical regular expressions for words, regular tree expressions are difficult to read and to write. For instance, the regular tree expression defining terms of the form f (g n (a),

h m (b)) with n, m ∈ N is f (g( 1 ) * , 1 . 1 a, h( 2 ) * , 2 . 2 b)
, where 1 and 2 are new constants. In this expression, the sub-expression g( 1 ) * , 1 . 1 a represents the language g n (a). The effect of * , 1 is to iteratively replace 1 by g( 1 ), and the effect of . 1 a is to replace 1 by a. Regular tree expressions are expressive enough to define any regular tree language. To be complete w.r.t. regular tree languages, this formalism needs named placeholders (like 1 and 2 above) because the effect of the iteration symbol * depends on the position where it occurs. However, named placeholders make regular tree expressions difficult to read and to write, even if they define simple languages. For instance, the set I = {delete(A, l) | l ∈ L} defined above can be written delete(A, cons((A|B), 1 ) * , 1 . 1 nil) where 1 is a new constant.

In this paper, we propose a new formalism for defining regular tree languages: simplified regular tree expression (SRegexp for short). Those expressions are not complete w.r.t. regular languages but are easier to read and to write. For instance, the set I is defined by the SRegexp delete(A,[cons((A|B),*|nil)]). Those regular expressions are defined using only 3 operators: '|' to build the union of two languages, '*' to iterate a pattern and the optional brackets '[ ... ]' to define the scope of the embedded *. The SRegexp cons((A|B),*|nil) repeats the pattern cons(A, _) or cons(B,_) as long as possible and terminates by nil. Thus, it defines the language {nil, cons(A,nil), cons(B,nil), cons(A,cons(A,nil)), cons(A,cons(B,nil)),. . .}. The brackets define the scope of the pattern to repeat with *. In the SRegexp delete(A,[cons((A|B),*|nil)]), the iteration applies on cons(A, _) or cons(B,_) but not on delete(A,_). Thus, this expression represents the language {delete(A, nil), delete(A,cons(A,nil)), delete(A,cons(B,nil)), . . .}. 2We implemented SRegexp in Timbuk together with a translation to standard regular tree expressions. We also implemented the translation from regular tree expressions to tree automata defined in [START_REF] Kuske | Construction of tree automata from regular expressions[END_REF]. Thus, from a SRegexp I, Timbuk can automatically generate a tree automaton A whose recognized language L(A) is equal to I. We also implemented the converse operations: tree automata to regular expression using the algorithm [START_REF] Guellouma | Construction of rational expression from tree automata using a generalization of Arden's lemma[END_REF] and regular tree expressions to SRegexp. Note that, since SRegexp are incomplete w.r.t. regular tree languages, conversion from regular tree expression to SRegexp may fail. Thus, the over-approximation of reachable terms computed by Timbuk is presented as a SRegexp if it is possible, or as a tree automaton otherwise.

The need for abstraction equations

Starting from R and I = L(A), computing R * (I) is not possible in general [START_REF] Gilleron | Regular tree languages and rewrite systems[END_REF]. Nevertheless, if R is a left-linear TRS then R * (I) can be over-approximated with tree automata completion [START_REF] Genet | Decidable Approximations of Sets of Descendants and Sets of Normal Forms[END_REF]. From A and R, completion builds a tree automaton

A * such that L(A * ) ⊇ R * (I). If Bad is regular, to prove R * (I) ∩ Bad = ∅,
it is enough to check that L(A * ) ∩ Bad = ∅, which can be done efficiently [START_REF] Comon | Tree Automata Techniques and Applications[END_REF]. For this technique to succeed, the precision of the approximation A * is crucial. For instance, L(A * ) = T (F) is a valid regular over-approximation but it cannot be used to prove any safety property since it also contains Bad. In Timbuk, approximations are defined using sets of abstraction equations, following [START_REF] Meseguer | Equational abstractions[END_REF] and [START_REF] Genet | Equational tree automata completion[END_REF].

Example 1. Let L be the set of terms defined with the symbol s of arity 1 and the constant symbol 0. Let X be a variable. The effect of the equation s(s(X)) = s(X) is to merge in the same equivalence class terms s(s(0)) and s(0), s(s(s(0))) and s(s(0)), etc. Thus, with this single equation, L/ = E consists of only two equivalence classes: a class containing only 0 and the class containing all the other natural numbers {s(0), s(s(0)), . . .}. An equation s(X) = X would define a single equivalence class containing all natural numbers. It would thus define a rougher abstraction. An equation s(s(X)) = X defines two equivalence classes: the class of even numbers {0, s(s(0)), . . .} and the class of odd numbers {s(0), s(s(s(0))), . . .}.

For completion to terminate, the set T (F)/ = E (E-equivalence classes of T (F)) has to be finite [START_REF] Genet | Automata Completion and Regularity Preservation[END_REF]. When dealing with functional programs, this restriction can be relaxed as follows. Functional programs manipulate sorted terms and the associated TRSs preserve sorts. Provided that equations also preserve sorts, having a finite set T (F) S / = E , where T (F) S is the set of well-sorted terms, is enough. Besides, since well-sorted terms define a regular language, this information can be provided to Timbuk using tree automata, regular expressions or SRegexp. Going back to the delete example that we want to analyze, with set E = {cons(X, cons(Y, Z)) = cons(Y, Z)}, L/ = E is finite but T (F) S / = E may not be. For instance, terms delete(A, nil), delete(A, delete(A, nil)), etc. are all in separate equivalence classes. Again, we can take advantage from the fact that delete is a functional program and relax the termination condition of completion by focusing it on the data manipulated by the program. Instead of asking for finiteness of T (F) S / = E , we only require finiteness of T (C) S / = E , where T (C) S is the set of well-sorted constructor terms. Let us note E c the above set of equations {cons(X, cons(Y, Z)) = cons(Y, Z)}. As shown in Example 2, E c defines a finite set of equivalence classes on T (C) S , i.e., lists of A's and B's. 3 Provided that delete is a terminating and complete functional program, it is possible to extend E c so that completion terminates. This has been shown for first-order functional programs [START_REF] Genet | Termination Criteria for Tree Automata Completion[END_REF] and for higher-order functional programs [START_REF] Genet | Verifying higher-order functions with tree automata[END_REF]. The extension of E c consists in adding two sets of equations

E R = {l = r | l → r ∈ R} and E r = {f (X 1 , . . . , X n ) = f (X 1 , . . . , X n ) | f ∈ F
, arity of f is n, and X 1 , . . . , X n are variables}. Since E R and E r are fixed by the program, the precision of the approximation only depends on the equivalence classes defined by E c . Thus, to explore approximations, it is enough to explore all possible E c .

Generating abstraction equations E c

Additionally to the fact that (1) T (C) S / =Ec has to be finite, the termination theorems of [START_REF] Genet | Termination Criteria for Tree Automata Completion[END_REF][START_REF] Genet | Verifying higher-order functions with tree automata[END_REF] imposes additional constraints on E c . Equations in E c have to be contracting, i.e., they are of the form u = u| p where (2) u| p is a strict subterm of u and (3) u| p has the same sort as u. 4 Conditions ( 2) and (3) makes it possible to prune the search space of equations in E c . For instance the following equations do not need to be considered: cons(X, Y ) = Z because of condition (2), cons(X, cons(Y, Z)) = cons(X, Z) because of condition (2), cons(X, Y ) = X because of condition [START_REF] Boichut | Towards more precise rewriting approximations[END_REF].

Timbuk implements two different algorithms to explore the space of possible E c . Those algorithms are parameterized by a natural number k ∈ N and, for a given k, they generate a set EC(k) of possible E c . By increasing k, we increase the precision of equations sets E c in EC(k). The first algorithm is based on covering sets [START_REF] Kounalis | Testing for the Ground (Co-)Reducibility Property in Term-Rewriting Systems[END_REF] and generates contracting equations with variables [START_REF] Genet | Verifying higher-order functions with tree automata[END_REF]. In this algorithm k defines the depth of the covering set used to generate the equations. From a covering set S, we generate all equations sets E c = {u = u| p | u ∈ S} satisfying conditions (1) to (3).

Example 3. Let X be a variable and T (C)

S be the set of well-sorted constructor terms defined with symbol s of arity 1 and the constant symbol 0. For k = 1, the covering set is {s(X), 0} and EC(1) = {{s(X) = X}}. For k = 2, the covering set is {s(s(X)), s(0), 0} and EC(2) = {{s(s(X)) = X}, {s(s(X)) = s(X)}, {s(0) = 0}, {s(0) = 0, s(s(X)) = X}, {s(0) = 0, s(s(X)) = s(X)}}.

The second algorithm generates ground contracting equations [START_REF] Genet | Automata Completion and Regularity Preservation[END_REF]. In this algorithm k represents the number of equivalence classes expected in T (C) S / =Ec . Since equation sets have to be ground and meet conditions (2) and (3), we can finitely enumerate all the possible equations sets E c for a given k.

Example 4. Let T (C)

S be the set of well-sorted constructor terms defined with symbol s of arity 1 and the constant symbol 0. For k = 1 the set EC(1) = {{s(0) = 0}}. For k = 2, the set EC(2) = {{s(s(0)) = 0}, {s(s(0)) = s(0)}.

A systematic way to build ground EC(k), based on tree automata enumeration, is given in [START_REF] Genet | Automata Completion and Regularity Preservation[END_REF]. Using the first or second algorithm to generate EC(k), to prove that there exists a tree automaton A * over-approximating R * (L(A)) and such that L(A * ) ∩ Bad = ∅, we run the following algorithm: It has been shown in [START_REF] Genet | Automata Completion and Regularity Preservation[END_REF] that the ground enumeration of EC(k) is complete w.r.t. tree automata that are closed by R-rewriting. Thus, if there exists such a A * , the above iterative algorithm will find it. However, on properties that cannot be shown using a regular approximation, such as [START_REF] Boichut | A theoretical limit for safety verification techniques with regular fix-point computations[END_REF], this algorithm may diverge.

1. Start with k = 1 2. Build EC(k) 3. Pick one E c in EC(k) 4. Complete A into A * using R and E c ∪ E R ∪ E r 5. If L(A * ) ∩ Bad = ∅ then

Interacting with Timbuk

Download http://people.irisa.fr/Thomas.Genet/timbuk/timbuk3.2.tar.gz and compile and install Timbuk 3.2. The online version of Timbuk does not integrate all the features presented here. In Timbuk's archive, the full specification of the delete example can be found in the file FunExperiments/deleteBasic.txt. This file contains the TRS, the SRegexp presented above and a tree automaton named TC which defines well-sorted constructor terms as explained in Example 2. This automaton is used to prune equation generation. Note that this automaton could be inferred from the typing information of the functional program. Here, the automaton TC states that lists are built with cons and nil, that elements of the list are either A or B, and that true and false are of the same type but cannot appear in a list. Thus, ill-typed terms of the form cons(nil, true) are not considered for equation generation. Finally, the Patterns section defines the set Bad of terms that should not be reachable. Currently, the pattern section is limited to terms or patterns (terms with holes '_') and cannot handle SRegexp or automata. In the present example, we only consider a subset of bad terms: terms of the form cons(A,_), i.e., lists starting by A. Assuming that your working directory is FunExperiments, you can run Timbuk on this example by typing: timbuk --fung 30 deleteBasic.txt. Where --fung is the option triggering ground equation generation (the second algorithm for generating EC(k)) and 30 is a maximal number of completion steps. We get the following output:

Generated equations: ------------------- cons(A,cons(A,nil)) = cons(A,nil) cons(B,cons(A,nil)) = cons(A,nil) cons(B,nil) = nil B = B nil = nil delete(X,Y) = delete(X,Y) A = A true = true cons(X,Y) = cons(X,Y) false = false ite(X,Y,Z) = ite(X,Y,Z) eq(X,Y) = eq(X,Y) eq(A,A) = true eq(A,B) = false eq(B,A) = false eq(B,B) = true delete(X,nil) = nil delete(X,cons(Y,Z)) = ite(eq(X,Y),delete(X,Z),cons(Y,delete(X,Z))) ite(true,X,Y) = X ite(false,X,Y) = Y Regular expression: ------------------- [cons(B, *|nil)]
Proof done! -----------Completion time: 0.006595 seconds

The three first generated equations belong to E c , reflexive equations of the form B = B, nil = nil, . . . belong to E r and the last eight equations belong to E R . The set T (C)

S / =Ec has two equivalence classes: the class containing nil and all lists containing only B's and the class of lists containing at least one A. Thus, the effect of E c is to forget any B and preserve any A that appears in a list. Using the --fun option instead of --fung while running Timbuk, triggers the first algorithm for generating EC(k), i.e., E c with variables. On this example, the generated E c part has two equations instead of three: cons(X,cons(A,Y)) = cons(A,Y) and cons(B,X) = X. The effect of this set E c is the same as the ground E c above. Indeed, this E c splits lists into two equivalence classes: the class of lists without A's and the class of lists with at least one A.

Finally, in Timbuk's output, Proof done! means that Timbuk manages to build a regular approximation of R * (I) that contains no term of the Patterns section. Timbuk outputs the resulting simplified regular expression [cons(B, *|nil)]. This proves that results are lists without any occurrence of A's. Here, one can read the outputted SRegexp to check that the property is true. How-ever, this can be difficult when the outputted SRegexp is more complex. Thus, on most examples, we use additional predicates to check properties like it is commonly done with proof assistants. On our previous example, given a predicate member (testing membership on lists), we can check that terms of the language member(A,delete(A,cons((A|B),*|nil))) never rewrite to true. We can also check the dual property expected on delete: deleting A's should not delete all B's. We hope to check this property using initial terms member(B,delete(A, [cons((A|B),*|nil)])) and a patterns section set to false. However, the property is not true and, during completion, Timbuk finds a counterexample:

Found a counterexample: ---------------------- Using this initial set of terms, Timbuk succeeds to do the proof and produces a slightly different E c : cons(A,cons(B,nil)) = cons(B,nil), cons(B,cons(B,nil)) = cons(B,nil), cons(A,nil) = nil. This time, E c forgets about A's and preserves B's. More than 20 other examples (with ground/non-ground equations generation) can be found on the Timbuk page http://people.irisa.fr/Thomas.Genet/ timbuk/funExperiments/, including functions on lists, trees, sorting functions, higher-order functions, etc.

Conclusion and further Research

We know that completion is terminating on higher-order functional programs thanks to the recent result of [START_REF] Genet | Verifying higher-order functions with tree automata[END_REF]. Besides, we also know that ground equation generation of E c is complete w.r.t. tree automata that are closed by R [START_REF] Genet | Automata Completion and Regularity Preservation[END_REF]. In other words, if there exists a tree automaton A * , closed by R and overapproximating the set of reachable terms, then it will eventually be found by generating ground equations. With the first algorithm where equations of E c may contain variables, we do not have a similar completeness result, yet. However, generating equations with variables remains an interesting option because the set E c can be smaller. This is the case in the previous example where E c with variables defines the same set of equivalence classes but with fewer equations.

From a theoretical perspective, Tree Automata Completion can be seen as an alternative to well-established higher-order model-checking techniques like PMRS [START_REF] Ong | Verifying higher-order functional programs with patternmatching algebraic data types[END_REF] or HORS [START_REF] Matsumoto | Automata-Based Abstraction for Automated Verification of Higher-Order Tree-Processing Programs[END_REF] to verify higher-order functional programs. Timbuk implements Tree Automata Completion but was missing several features for those theoretical results to be usable in practice. First, stating the property to prove using a tree automaton was error-prone and lacked readability. Using simplified regular expressions significantly improves this step and makes property definition closed to what is generally used in a proof assistant. Second, equations which are necessary to define the approximation, had to be given by the user [START_REF] Genet | Termination Criteria for Tree Automata Completion[END_REF]. Now, Timbuk can automatically generate a set of equations adapted to a given verification objective. Combining those two extensions makes Timbuk a competitive alternative to higher-order model checking tools like [START_REF] Ong | Verifying higher-order functional programs with patternmatching algebraic data types[END_REF] and [START_REF] Matsumoto | Automata-Based Abstraction for Automated Verification of Higher-Order Tree-Processing Programs[END_REF].

In those model-checking tools and in Timbuk, the properties under concern are "regular properties", i.e. properties proven on regular languages. Those regular properties are stronger than what offers tests (they prove a property on an infinite set of values) but weaker than what can be proven using induction in a proof assistant. However, unlike proof assistants, Timbuk does not require to write lemmas or proof scripts to prove a regular property. An interesting research direction is to explore how to lift those regular properties to general properties. In other words, how to build a proof that ∀ x l. not(member(x,delete(x,l))) from the fact that all terms from member(A,delete(A,cons((A|B),*|nil))) rewrite to false. We believe that this is possible by taking advantage of parametricity such as in [START_REF] Wadler | Theorems for free![END_REF]. This is ongoing work.

In this paper, the verification is performed on a TRS representing the functional program. To directly perform the verification on real functional programs rather than on TRSs, we need a transformation. We could reuse the HOCA transformation of [START_REF] Avanzini | Analysing the complexity of functional programs: higher-order meets first-order[END_REF]. However, it does not take the priorities of the pattern matching rules of the functional program into account when producing the TRS. Furthermore, this translation needs to be certified, i.e., we need a formal proof that the behavior of the outputted TRS R covers all the possible behaviors of the functional program. With such a proof on R, if Timbuk can prove that no term of member(A,delete(A,cons((A|B),*|nil))) can be rewritten to true with R, then we have a similar property on the functional program.

The equation generation process does not cover all TRSs but only TRSs encoding terminating, complete, higher-order, functional programs. We currently investigate how to generate equations without the termination and completeness restrictions on the program. Another research direction is to extend this verification principle to more general theorems. For the moment, theorems that can be proved using Timbuk need to have a regular model. For instance, Timbuk is able to prove the theorem member(A,delete(A,l)) →R * true for all lists l=cons((A|B),*|nil) because the language of terms reachable from the initial language member(A,delete(A,cons((A|B),*|nil))) is, itself, regular. Assume that we have a predicate eq encoding equality on lists. To prove a theorem of the form eq(delete(A,l),l) →R * false for all list l=cons(B,*|nil), the language of reachable terms is no longer regular. However, recent advances in completionbased techniques for non-regular languages [START_REF] Boichut | Towards more precise rewriting approximations[END_REF] should make such verification goals reachable.

Example 2 .

 2 Let us consider the set L of well-sorted lists of A and B. The set L is the regular language associated with the SRegexp cons((A|B), * |nil). Let X, Y, Z be variables. The set E = {cons(X, cons(Y, Z)) = cons(Y, Z)} defines a set of E-equivalence classes L/ = E with three classes: one class only contains nil, one class contains all lists ending with an A and the last class contains all lists ending with a B.

  Ops delete:2 cons:2 nil:0 A:0 B:0 ite:3 true:0 false:0 eq:2 Const A B nil cons true false Vars X Y Z TRS R delete(X,nil)->nil delete(X,cons(Y,Z))->ite(eq(X,Y),delete(X,Z),cons(Y,delete(X,Z))) ite(true,X,Y)->X ite(false,X,Y)->Y eq(A,A)->true eq(A,B)->false eq(B,A)->false eq(B,B)->true SRegexp A0 delete(A,[cons((A|B),*|nil)]) Automaton TC States qe ql qb Final States qe ql qb Transitions A->qe B->qe nil->ql cons(qe,ql)->ql true->qb false->qb Patterns cons(A,_)

  -Term member(B,delete(A,nil)) rewrites to a forbidden pattern For the property to hold, lists in initial terms should contain at least one B: member(B,delete(A,[cons((A|B),*|[cons(B,*|[cons((A|B),*|nil)])])]))

  verification is successful Otherwise, if EC(k) not empty, pick a new E c in EC(k) and go to 4. 6. When EC(k) is empty, increment k and go to 2.

When the analysis depends on the evaluation strategy, completion can be extended to take it into account[START_REF] Genet | Reachability Analysis of Innermost Rewriting[END_REF].

See the page http://people.irisa.fr/Thomas.Genet/timbuk/funExperiments/ simplifiedRegexp.html for more examples.

In fact, in T (C) S there are also terms true and false but they cannot be embedded in lists. Thus, each of them defines its own equivalence class. In the end, in T (C) S /=E c there are 5 equivalence classes.

Note that the sort information can be inferred from the tree automaton recognizing well-sorted terms. For instance, the automaton associated to the SRegexp of Example 2 recognizes A and B by into the same state, thus A and B will have the same sort (see automaton TC in

Section 5)

Acknowledgements

Many thanks to the anonymous referees for their valuable comments.