Théo Losekoot

Thomas Genet

Thomas Jensen

Automata-based verification of relational properties of functions over data structures

Keywords: 2012 ACM Subject Classification Theory of computation → Program verification; Theory of computation Formal verification, Tree automata, Constrained Horn Clauses, Model inference, Relational properties, Algebraic datatypes

This paper is concerned with automatically proving properties about the input-output relation of functional programs operating over algebraic data types. Recent results show how to approximate the image of a functional program using a regular tree language. Though expressive, those techniques cannot prove properties relating the input and the output of a function, e.g., proving that the output of a function reversing a list has the same length as the input list. In this paper, we built upon those results and define a procedure to compute or over-approximate such a relation. Instead of representing the image of a function by a regular set of terms, we represent (an approximation of) the input-output relation by a regular set of tuples of terms. Regular languages of tuples of terms are recognized using a tree automaton recognizing convolutions of terms, where a convolution transforms a tuple of terms into a term built on tuples of symbols. Both the program and the properties are transformed into predicates and Constrained Horn clauses (CHCs). Then, using an Implication Counter Example procedure (ICE), we infer a model of the clauses, associating to each predicate a regular relation. In this ICE procedure, checking if a given model satisfies the clauses is undecidable in general. We overcome undecidability by proposing an incomplete but sound inference procedure for such relational regular properties. Though the procedure is incomplete, its implementation performs well on 120 examples. It efficiently proves non-trivial relational properties or finds counter-examples.

Introduction

This paper is concerned with automatically proving properties about the input-output relation of functional programs operating over algebraic datatypes. We explore an approach in which both programs and properties are represented as Constrained Horn Clauses [START_REF] Bjørner | Horn clause solvers for program verification[END_REF],

i.e., Horn clauses with additional constraints expressed in an underlying theory. Using such representation, proving a property of a program is reduced to finding a model of the combined set of Horn clauses that represent the program and the property. We illustrate this using an example where we define the type of natural numbers and natural numbers lists, and two recursive functions, len computing the length of a list and less checking if a natural number is strictly less than another. We aim at (automatically) proving the logical properties ∀x l. less Z (len Cons(x, l)) and ∀x l. less (len l) (len Cons(x, l)). Here are the program in Ocaml-like syntax, the logical formulas for properties and their equivalent CHC representation. Note that n-ary functions (like unary len) are translated into n + 1-ary Our goal is thus to automatically infer a model of this set of clauses, i.e., solve the satisfiability problem for Constrained Horn Clauses over the theory of inductive datatypes. Tree automata [START_REF] Hubert Comon | Tree Automata Techniques and Applications[END_REF] are a well-know formalism to represent, approximate, and infer models on functional programs [11,[START_REF] Matsumoto | Automata-based abstraction for automated verification of higher-order tree-processing programs[END_REF] or even on CHCs [START_REF] Kostyukov | Beyond the elementary representations of program invariants over algebraic data types[END_REF]. In all those works, the inferred model is not relational, i.e., it only consists of a regular set of unrelated terms. For instance, in our example, the first property ∀x l. less Z (len (Cons(x, l))) is not relational and can thus be proven using regular sets like [11, [START_REF] Kostyukov | Beyond the elementary representations of program invariants over algebraic data types[END_REF][START_REF] Matsumoto | Automata-based abstraction for automated verification of higher-order tree-processing programs[END_REF] do. To perform the proof, the solvers only need to consider two regular languages: L lists containing all lists of natural numbers and L Cons+ containing all non-empty lists of natural numbers. Then, the proof is carried out by showing that if l ∈ L lists then, for any natural number x, the term Cons(x, l) belongs to L Cons+ . Finally, since any list l ∈ L Cons+ have a length strictly greater than 0 then the property is true.

On the opposite, the second property, ∀x l. less (len l) (len Cons(x, l)), is relational and, thus, out of the scope of the aforementioned approaches. We still have that if l ∈ L lists then cons(x, l) ∈ L Cons+ but for any l ∈ L lists and any l ∈ L Cons+ we cannot prove that less (len l) (len l ). To preserve the relation between the two occurrences of the list l, we use convoluted automata [START_REF] Hubert Comon | Tree Automata Techniques and Applications[END_REF] which can represent regular relations between terms. We build upon the preliminary results obtained in [START_REF] Haudebourg | Automatic Verification of Higher-Order Functional Programs using Regular Tree Languages[END_REF] and propose a sound but incomplete procedure for inferring an automaton that represents a model of the program and the property. This procedure is defined as an Implication Counter Example (ICE) procedure [START_REF] Garg | Ice: A robust framework for learning invariants[END_REF].

Contributions:

-Definition of a sound model-checking procedure for CHCs on convoluted tree automata.

We propose two sound optimisations of this procedure so as to make it efficient in practice;

-Definition of an ICE procedure for inferring models of CHCs;

-Definition of a specific over-approximation technique enlarging the class of properties which can be proved using regular models on CHCs programs;

T. Losekoot, T. Genet, T. Jensen

3:3

-Implementation of the ICE procedure;

-On more than 120 examples, we show that our implementation automatically proves and disproves non-trivial examples.

This paper is organised as follows: In Section 2, we give an overview demonstrating the verification technique presented in this paper. In Section 3, we introduce the notions and notations. In Section 4, we briefly present how to encode functional programs into Horn clauses. In Section 5, we present a transformation from the model-checking procedure for CHCs into a search for a proof in a proof system representing the model. In Section 6, we present our use of the proof system for an efficient search. In Section 7, the ICE-procedure for inferring a model is defined. In Section 8, we present our approximation method. In Section 9, we discuss implementation-specific details and experiments. In Section 10, we present related work. Finally, we conclude in Section 11.

An overview of the verification procedure on an example

We continue our example of Section 1. We first give more details about the proof of the non-relational property ∀x l. less Z (len (Cons(x, l))). To represent the set L lists containing all lists of natural numbers and the set L Cons+ containing all non-empty lists of natural numbers, we use tree automata. Tree automata recognize sets of terms into states using transitions. E.g., a tree automaton with states {q nat , q Nil , q Cons+ } and transitions {Z() → q nat , S(q nat ) → q nat , Nil() → q Nil , Cons(q nat , q Nil ) → q Cons+ , Cons(q nat , q Cons+ ) → q Cons+ } recognizes Nil into the state q Nil and any non-empty list of naturals into the state q Cons+ . To recognize a term, transitions are used to rewrite the term into a state, e.g, Nil →

q Nil , and Cons(S(Z), Nil) → * Cons(S(q nat ), q Nil ) → Cons(q nat , q Nil ) → q Cons+ . Similarly

Cons(Z, Cons(S(S(Z)), Nil)) → * q Cons+ . To prove the property ∀x l.less Z (len (Cons(x, l)))

using such an automaton, it is enough to show that if l belongs to L lists (whose terms are recognized by q Nil or q Cons+ ), then Cons(x, l) belongs to L Cons+ (whose terms are recognized by q Cons+ ). Using another automaton for Less, it is possible to show that (len l ), with l recognized by q Cons+ , belongs to the language L pos of strictly positive natural numbers, whereas (len Nil) belongs to the language {Z}. Now, we present a complete overview of our verification procedure for proving the second property ∀x l. less (len l) (len Cons(x, l)) which is relational and, thus, out of the scope of solvers like [11,[START_REF] Kostyukov | Beyond the elementary representations of program invariants over algebraic data types[END_REF][START_REF] Matsumoto | Automata-based abstraction for automated verification of higher-order tree-processing programs[END_REF]. As shown before, the functions and the property are all translated into a set of CHCs. In the following, we denote by C this set. Given C, we start the model inference phase whose objective is to infer a model of this set, named M in the following. For each relation R defined by the program, M contains an automaton A R recognizing a language for the relation R. This model inference is implemented as an Implication Counter-Example (ICE) procedure [START_REF] Garg | Ice: A robust framework for learning invariants[END_REF] between two entities: a learner and a teacher. The learner's goal is to infer a correct model

First iteration of the learner-teacher algorithm

The learner proposes the model M = {Len → A ∅ , Less → A ∅ }. The teacher checks if M satisfies each clause of C, i.e., for each ϕ ∈ C it checks if M |= ϕ. This is not true for the clause Len(Nil, Z) which imposes that the pair (Nil, Z) is part of the relation associated with Len. This is not the case here. Thus, the learner provides the ground clause Len(Nil, Z) as a counter-example.

Second iteration of the learner-teacher algorithm

Starting from M = {Len → A ∅ , Less → A ∅ } and the counter-example Len(Nil, Z), the learner improves M in order to add the pair (Nil, Z) into the relation associated with Len, i.e., refines the automaton so as to recognize the pair (Nil, Z). For recognizing a relation, we need to extend the tree automaton formalism to recognize regular sets of tuples of terms. A solution proposed in [START_REF] Hubert Comon | Tree Automata Techniques and Applications[END_REF] is to use a tree automaton recognizing convolutions of terms. A convolution transforms a tuple of terms into a term built on tuples of symbols. It does so by introducing new convoluted symbols which represent tuples of symbols. For example, to recognize the pair (Nil, Z) we define a new symbol Nil, Z and a tree automaton A 1 with the state q 0 and the unique transition Nil, Z () → q 0 . With such an automaton, the relation recognized by automaton A 1 is R(A 1 ) = {(Nil, Z)}. Finally, we now have

M = {Len → A 1 , Less → A ∅ }.
Again, this model is given to the teacher which checks if

M |= C. The teacher finds out that M |= Len(l, n) ⇒ Len(Cons(x, l), S(n)). Indeed, since (Nil, Z) ∈ L(A 1 ) we should have (Cons(i, Nil), S(Z)) ∈ L(A 1
) for all natural numbers i. The teacher provides a ground instance of this clause as a counter-example, e.g., Len(Nil, Z) ⇒ Len(Cons(Z, Nil), S(Z)).

Third iteration of the learner-teacher algorithm: Learner part

Starting from M = {Len → A 1 , Less → A ∅ } and the counter-example obtained from the previous iteration Len(Nil, Z) ⇒ Len(Cons(Z, Nil), S(Z)), the learner should refine A 1 into A 2 so that it also recognizes the pair (Cons(Z, Nil), S(Z)). This time, to build the convolution we have to overlay the terms Cons(Z, Nil) and S(Z). However, because of the different arities of Cons and S, the trees representing those two terms do not perfectly overlap. The convolution adds a padding symbol to complement trees in order to have a perfect overlap. Back to our example, with a convolution (known as right-convolution) the tree for S(Z) becomes Thus, a refined automaton A 2 recognizing both (Nil, Z) and (Cons(Z, Nil), S(Z)) has states {q 0 , q 1 , q 2 } and transitions { Nil, Z () → q 0 , Z, () → q 1 , Cons, S (q 1 , q 0 ) → q 2 }. If we declare states q 0 and q 2 as final (meaning that we ignore the languages recognized by non final states) then R(A 2 ) = {(Nil, Z), (Cons(Z, Nil), S(Z))}.

A last phase of the ICE learning process is to reduce the number of states of the automaton and, doing so, possibly enlarge the recognized language. Note that this phase was skipped on automaton A 1 because it has only one state. Reducing the number of states consists in finding state merging which are coherent w.r.t. the ground clauses sent by the teacher and coherent w.r.t. types of recognized languages. For instance, on A 2 , merging q 0 with q 2 is possible because both recognize pairs of lists and natural numbers. On the opposite, merging q 0 with q 1 is incorrect because q 0 recognize pairs of lists and q 1 only recognizes a unique natural T. Losekoot, T. Genet, T. Jensen 3:5 number (omitting padding). After renaming q 2 to q 0 , transitions of the automaton A 2 become { Nil, Z () → q 0 , Z, () → q 1 , Cons, S (q 1 , q 0 ) → q 0 }. Note that this automaton now recognizes {(Nil, Z), (Cons(Z, Nil), S(Z)), (Cons(Z, Cons(Z, Nil)), S(S(Z))), . . .}, i.e., all pairs (l, n) where l is a list of Z whose length is n.

Conclusion of the learner-teacher algorithm

During following iterations, the learner-teacher proceed similarly to infer an automaton for Less and to finish inferring that of Len. Finally, during the 6-th iteration, the learner ends up on the following model M = {Len → A Len , Less → A Less } where A Len has final states {q 0 } and the transitions { , S (q 1 ) → q 1 , , Z () → q 1 , Nil, Z () → q 0 , Cons, S (q 1 , q 0 ) → q 0 }. This automaton is close to automaton A 2 except that it recognizes any natural number in place of Z in the list, i.e., it recognizes all pairs (l, n) where l is a list of natural numbers whose length is n. The automaton A Less has the final states {q 3 } and the transitions { , Z () → q 4 , , S (q 4 ) → q 4 , Z, S (q 4 ) → q 3 , S, S (q 3 ) → q 3 }. This model is given to the teacher which then checks that it satisfies all the clauses of C. This terminates the verification and proves that ∀x l. less (len l) (len Cons(x, l)).

Prerequisites

Typed alphabet and term

Definition 1 (Typed alphabet). A typed alphabet (Σ, τ, Γ) is a set of symbols Σ, a set of types Γ, and a typing function τ which assigns to each symbol f a type τ( f ) = τ 1 × . . . × τ n → τ 0 with ∀i ∈ 0, n , τ i ∈ Γ and n ∈ N varying for each symbol f . When n = 0, the symbol is a constant and does not take input. For f ∈ Σ and τ( f ) = τ 1 × . . . × τ n → τ 0 , we say that f is of arity n, written

| f | = n, and that τ 0 is the output type of f , written τ out ( f ) = τ 0 . When clear from context, we identify the tuple (Σ, τ, Γ) with Σ.

Definition 2 (Term). A (typed) term t over an alphabet Σ is the data of a symbol f ∈ Σ, called the root symbol of t and written Root(t), together with a list t 1 , . . . ,

t | f | of | f | terms, called children of t,
such that their type is compatible, i.e. τ( f ) = τ out (Root(t 1 ))

× . . . × τ out (Root(t | f | )) → τ out ( f ).
A term t is also written f (t 1 , . . . , t | f | ). We overload τ with τ(t) = τ out (Root(t)). The set of terms over an alphabet Σ is written T (Σ).

Definition 3 (Substitution).

A substitution σ is a finite map between variables and terms (which may contain variables). The application of a substitution σ to a variable x, written σ(x), is defined as t if there exists a binding (x, t) ∈ σ and x otherwise. The application of a substitution is generalized to terms by σ( f (t 1 , . . . , t n )) = f (σ(t 1 ), . . . , σ(t n )). Even more generally, a substitution can be applied to any structure containing variables. The composition of substitution, which first applies σ 1 and then σ 2 , is written σ 1 ; σ 2 . The domain of a substitution is the set of variables for which a binding is defined and is written dom(σ).

A function Vars is used without definition, if unambiguous, to fetch the set of variables contained in a structure. It can be called, for example, on a term or on a tuple of structures containing variables.

Tree automaton

Definition 4 (Tree automaton). A (bottom-up) tree automaton A = (Q, Q f , ∆) over an alphabet Σ is given by a finite set of states Q, a set of final states Q f ⊆ Q, and a set of transitions (or rules) ∆ F S C D 2 0 2 3

3:6

Automata-based verification of relational properties of functions over data structures such that transitions are of the form f (q 1 , . . . , q | f | ) → q 0 , where f ∈ Σ and ∀i ∈ 0, | f | , q i ∈ Q.

Definition 5 (Language recognized by an automaton). The set of terms recognized (or accepted) in a state q of an automaton A is inductively defined as L(A, q) = { f (t 1 , . . . , t n ) | f (q 1 , . . . , q n ) → q ∈ ∆ ∧ i∈ 1,n t i ∈ L(A, q i )}. The language recognized by an automaton is

L(A) = q f ∈Q f L(A, q f ).
Definition 6 (Typed tree automaton). A typed tree automaton is a tree automaton whose states are typed by types of the alphabet. We write τ(q) for the type of the state q. Transitions have to be compatible with the types of the symbols, i.e., for any rule f (q 1 , . . . , q n ) → q 0 ∈ ∆,

τ( f ) = τ(q 1 ) × . . . × τ(q n ) → τ(q 0 ).
All final states must be of the same type. The type of the automaton, written τ(A), is the type of its final states.

We write A for the complement of the automaton A w.r.t its type, i.e., L(A)

= {t | τ(t) = τ(A) ∧ t / ∈ L(A)}.
We also use Q, Q f , and ∆ as accessors, that is, as functions to respect- ively extract states, final states, and transitions from an automaton. We usually write t or f (t 1 , . . . , t n ) for terms, q for a state, and A for an automaton. Tuple of elements (e 1 , . . . , e n )

are also written e and e[i] means e i .

Automata recognizing a relation

There exist multiple formalism for representing a relation on terms with an automaton. They differ in their expressive power, closure properties, and decision procedure complexity. The most well known are tuple automata, ground tree transducers, and automata on convoluted terms, all described in [START_REF] Hubert Comon | Tree Automata Techniques and Applications[END_REF]. We will pursue an approach based on automata on convoluted terms, or simply convoluted automata.

Convoluted automata are defined w.r.t an operation called convolution which transforms an n-tuple of terms into a unique term whose symbols are n-tuple of symbols. Intuitively, an automaton defined on this alphabet of tuple reads n terms at the same time, thereby recognizing a relation. The standard convolution operator amounts to overlaying the (syntax tree of the) terms, starting from the root, and adding a padding symbol / ∈ Σ (of type τ ) as there is an arity mismatch between symbols. To this end, we extend any alphabet Σ to Σ = Σ ∪ { }. We call this standard convolution the left convolution, in order to distinguish it from other convolutions, e.g. the right convolution, that has been used in section 2 and in the rest of the paper. We first define left-convolution of a tuple of tuple, and then use it to define convolution of terms.

Definition 7 (Left-convolution). ⊕ L ((e 1 1 , . . . , e k 1 1 ), . . . , (e 1 n , . . . , e k n n )) = (e 1 1 , . . . , e 1 n ), . . . , (e k 1 , . . . , e k n ) with k = max i∈ 1,n (k i ) and ∀i ∈ 1, n , ∀j ∈ 1, k , e j i = e j i if j ≤ k i

and otherwise

Definition 8 (Left-convolution of terms). The n-ary left-convolution, written ⊕ t L , takes n terms (t 1 , . . . , t n ) on an alphabet Σ and returns a term ⊕ t L (t 1 , . . . , t n ) on a convoluted alphabet Σ ⊕ L = Σ n whose elements are written f 1 , . . . , f n or f . The left-convolution of n terms is recursively defined as: With l ex and n ex as defined below,

⊕ t L ( f 1 ( t 1 ), . . . , f n ( t n )) = f 1 , . . . , f n (⊕ t L ( t 1 ), . . . , ⊕ t L ( t k )) with t 1 , . . . , t k = ⊕ L ( t 1 , . . . , t n ) Example 9 (Left convoluted terms). Let Σ ex = {Z, S, Nil, Cons}, with τ(Z) = nat, τ(S) = nat → nat, τ(Nil) = natlist, τ(Cons) = nat × natlist → natlist,
l ex = Cons l ex = Z Cons Z Nil n ex = S n ex = S Z ⊕ t L (l ex , n ex ) = Cons, S Z, S , Z Cons, Z, Nil,
Note that, due to type constraints,

T (Σ ) = T (Σ) ∪ { }. The left-convolution ⊕ t L of n
terms is an isomorphism between T (Σ ) n and T (Σ ⊕ L ). Automata recognizing convoluted terms thus recognize relations on T (Σ ) n .

Definition 10 (Regular relation).

A relation recognized by a tree automaton is said to be regular.

The relation recognized by automaton

A is R(A) = ⊕ L -1 (L(A)) = { t | ⊕ L ( t) ∈ L(A)}.
Similarly, the relation recognized by state q of A is R(A, q) = ⊕ L -1 (L(A, q)).

We impose that the type of any final state

q f is τ -free, that is, τ(q f ) = (τ 1 , . . . , τ n ) with ∀i ∈ i, n , τ i = τ .
This ensures that an automaton defines a relation between terms of T (Σ), i.e. terms without padding.

Example 11 (Convoluted automata). Let A < be the automaton with states {q, q f }, of which q f is final, and transitions { , Z () → q, , S (q) → q, Z, S (q) → q f , S, S (q f ) →

q f }. R(A < ) is
q f q f , Z () → q -→ , S (q) → q -→ Z, S (q) → q f -→ S, S (q f ) → q f -→

Convolutions and their expressivity

Which relations are representable by convoluted tree automaton highly depends on the precise datatypes definition. For example, when using the left-convolution, the Len relation can only be represented if the Cons constructor had its arguments swapped. This is because left-convoluting a list l and a natural number n will relate n with the left-most branch of l.

Instead of modifying constructors, we can define other convolutions. The right convolution, written ⊕ R , is defined similarly to ⊕ L but adds padding to the left of terms instead of to the right. This right convolution is effective for proving properties relating lists and unary natural numbers. Finally, we define the complete convolution, written ⊕ C , which is more expressive than both the left and the right convolution. This complete convolution relates every combination of tuple's element, which results in overlaying every same-depth constructor when convoluting terms. The complete convolution has the advantage of not On the left is depicted the right convolution of l ex and n ex (of example 11), and on the right their complete convolution. Note how n ex 's constructors have been duplicated in the complete convolution.

⊕ t R (l ex , n ex ) = Cons, S Z, Cons, S Z, Nil, Z ⊕ t C (l ex , n ex ) = Cons, S Z, S , Z Cons, S Z, Z Nil, Z
Since definitions of this paper hold for any convolution, we write for any of ⊕ L , ⊕ R , or

⊕ C .

Functional programs and their logical representation

Regular models of functional programs

We consider first-order monomorphic functional programs. Such programs define a set of functions of the form f : τ 1 → . . . → τ n and of the form f : τ 1 → . . . → τ n → bool, with each τ i being an algebraic datatype. Each of these can be viewed as a relation on τ 1 × . . . × τ n .

Formally, these relations constitute a (relational) first-order structure on L, with L being the signature (the set of relation symbols together with their type). In our setting, the structures are typed, i.e. a relation R of type τ(R) = τ 1 × . . . × τ n only relates terms t 1 , . . . , t n satisfying ∀i ∈ 1, n , τ(t i ) = τ i .

Definition 13 (Regular model).

A regular model is a function M mapping each relation symbol R ∈ L to an automaton A R . M denotes S M , the L-structure where every R ∈ L is interpreted as R(A R ). We naturally extend first-order semantic judgement to write M |= ϕ for S M |= ϕ.

Regular models are close in essence to automatic structures. Automatic structures [START_REF] Grädel | Automatic structures: twenty years later[END_REF][START_REF] Hodgson | Théories décidables par automate fini (Decidable theories via finite automata[END_REF][START_REF] Khoussainov | Automatic Presentations of Structures[END_REF] are a kind of recursive structures [START_REF] Hirst | More about recursive structures: Descriptive complexity and zero-one laws[END_REF], which are part of the study of finite representation of structures. Automatic structures have been studied for their decidable first-order theory. We shall use tree automata to represent first-order structures that model functional programs.

This allows us to use specific and efficient methods for property checking.

We use Constrained Horn Clauses (CHCs) [START_REF] Bjørner | Horn clause solvers for program verification[END_REF] as representation of our programs. CHCs are first-order Horn clauses with additional constraints from a theory T (see example in the

Introduction). A CHC on a signature L is a closed formula of the form ∀ x, ψ( x) ∧ R 1 ( x 1 ) ∧ . . . ∧ R n ( x n ) ⇒ R 0 ( x 0 ), where ∀i ∈ 0, n , R i ∈ L.
The formula ψ( x) adds theory-related constraints. The semantic judgement S |= ϕ is standard first-order logic (modulo theory T). We usually leave out the universal quantifiers in front of CHCs: every variable in a formula is implicitly universally quantified. In our setting, we use the theory of inductive datatypes [START_REF] Barrett | An abstract decision procedure for a theory of inductive data types[END_REF] over an alphabet Σ, which means that the value of variables are within T (Σ)

and constraints are of the form x = f ( y), where f ∈ Σ, x is a variable and y is a tuple of variables. For simplicity, we sometimes write R(t) for x = t ∧ R(x). A ground CHC is one that has no variables or, in our context, where every variable's value is completely determined by datatypes constraints (for example, x = Nil ⇒ R(x) is considered ground).

Our encoding of functional programs into clauses prevents us from using Horn clauses in the translation of the if-then-else construct. For example, the simple translation of let f x = if p x then e else e ' yields the two clauses {P(x) ⇒ F(x, e), ¬P(x) ⇒ F(x, e )}. We therefore use non-Horn constrained clauses for modeling such functions. In the following, we handle a negated literal in the body as a positive head, in disjunction with the other heads. Other work [START_REF] Unno | Automating induction for solving horn clauses[END_REF] models similar programs with Horn clauses by reifying the truth of a predicate in the terms as its last argument, allowing to negate it in the body of a clause.

Both ways of treating negation seems viable for our purpose but we have only experimented with the first one.

Model-checking of regular structures

In this section, we present the procedure for checking the truth of a given CHC ϕ in a model M, i.e., check if M |= ϕ. This model-checking fulfills the teacher role of the ICE model inference procedure (See sections 2 and 7). This procedure is devised as a counterexample search. A counter-example is a ground instantiation of each variable of ϕ, written as a ground substitution σ, that disproves M |= ϕ. This procedure either returns None if M |= ϕ, and otherwise Some(σ), with σ a counter-example. However, this problem is undecidable in general, as showed in [START_REF] Shimoda | Symbolic automatic relations and their applications to SMT and CHC solving[END_REF]. Therefore the procedure given here is correct but incomplete, that is, it may diverge.

The model checking problem can be seen as a type checking procedure where typing rules correspond to rules of automata.

Definition 14 (Type checking instance). A typing obligation

ω = [ x 1 , . . . , x n : (A, q)]
is the data of a tuple x 1 , . . . , x n , with each x i being a variable or , and of a target type (A, q).

A typing problem (E, Ω) is a set of typing obligations Ω together with a set of constraints E, each of the form x = f ( y) with f a symbol of Σ. A solution for a typing problem is a substitution σ : X → T (Σ) that satisfies every typing obligation and constraint:

σ |= (E, Ω) . = σ |= Ω ∧ σ |= E with σ |= Ω . = ∀[ x : (A, q)] ∈ Ω, σ( x) ∈ R(A, q) and σ |= E . = ∀(x = f ( y)) ∈ E, σ(x) = f (σ( y))
Definition 15 (Coherence of a constraint set). A set of constraints E is said to be coherent if it admits a syntactic unifier. The most general unifier (MGU) of a coherent set E is written σ E .

Note that, given a typing problem (E, Ω) with a coherent E, any σ such that σ |= (E, Ω)

is equivalent to a σ such that σ E ; σ |= Ω (by characterisation of the MGU).

Definition 16 (Model checking as type checking).

Let some CHC formula

ϕ = ψ( x) ∧ R 1 ( x 1 ) ∧ . . . ∧ R n ( x n ) ⇒ R 0 ( x 0 ) and model M.
The set of typing problems associated to ϕ and

M is tp(ϕ, M) = {(ψ( x), Ω) | Ω ∈ Ω s } with Ω s = {[ x 1 : (A 1 , q 1 )], . . . , [ x n : (A n , q n )], [ x 0 : (A 0 , q 0 )]} | A 1 = M(R 1 ) ∧ . . . ∧ A n = M(R n ) ∧ A 0 = M(R 0 ) ∧ ∀i ∈ 0, n , q i ∈ Q f (A i )
The set of solutions σ to tp(M, ϕ) is the same as the set of counter-examples to M |= ϕ. Intuitively, for such a counter-example to exist, it should validate the atoms R 1 ( x 1 ), . . . , R n ( x n )

(i.e. be recognized by M(R 1 ) . . . , M(R n )) and invalidate the atom R 0 ( x 0 ) (i.e. be recognized by M(R 0 )). q, (B) : S, (q) → q, (C) : Cons, S (q, q f ) → q f , (D) : Nil, Z () → q f }. A Even has states {q e , q o }, final states {q e }, and rules {(1) : Z () → q e , (2) : S (q o ) → q e , (3) : S (q e ) → q o }.

To check whether M |= ϕ, we first translate (M, ϕ) into a typing problem instance. Note that Even appears in the head of the property ϕ, therefore we will need to complement A Even . We write its complement A Odd , which is the same automaton but with final states

{q o }. tp(M, ϕ) = (E 0 , Ω 0 ) with E 0 = ∅ and Ω 0 = [ l, n : (A Len , q f )], [ n : (A Odd , q o )]
In this case, tp(M, ϕ) only contains one element (as each automaton only has one final state), therefore M |= ϕ ⇐⇒ ∃σ, σ |= (∅, Ω 0 ).

Proof system

A proof obligation is the assertion that some typing problem (E, Ω) admits a solution, which is written as (E, Ω). We first define the unfolding of typing obligations and then the proof system. Any solution for a typing obligation ω = [ x 1 , . . . , x n : (A, q)] can be found by following transitions of the automaton A. A transition f 1 , . . . , f n (q 1 , . . . , q k ) → q of A (note that q is the same between the typing obligation and the rule's goal state) can act as a typing rule whose application generates k new typing obligations (one for each sub-state q j of the rule) and n new algebraic datatype constraints, the i th stating that variable x i is of the form f i ( x i ) with x i some fresh variables. We formally define this step as unfolding a typing obligation.

Definition 19 (Unfolding a typing obligation).

un f old([ x 1 , . . . , x n : (A, q)]) = { E r , Ω r | r ∈ ∆(A) ∧ r = f 1 , . . . , f n (q 1 , . . . , q k ) → q} with E r = {x i = f i ( x i ) | i ∈ 1, n } and Ω r = {[ ( x 1 , . . . , x n )[j] : (A, q j )] | j ∈ 1, k } where ∀i ∈ 1, n , x i are fresh variables.
Example 20 (Unfolding). Continuing with Example 18, we set ω 1 = [ l, n : (A Len , q f )]

and ω 0 = [ n : (A Odd , q o )]. Now, ω 0 can be unfolded by rules {(3)} and ω 1 by {(C), (D)}.

un f old(ω 0 ) = { E (3) , Ω (3) } with E (3) = {n = S(m)} and Ω (3) = [ m : (A Odd , q e )]
.

un f old(ω 1 ) = { E (D) , Ω (D) , E (C) , Ω (C) } with E (D) = {l = Nil, n = Z}, Ω (D) = ∅, E (C) = {l = Cons(l 1 , l 2 ), n = S(n 1 )}, Ω (C) = {[ l 1 , : (A Len , q n )], [ l 2 , n 1 : (A Len , q f )]}.
We define the unfolding of a set of typing obligations as the (combination of) unfolding of each typing obligation at the same time, that is the application of one rule of the automaton to each typing obligation.

T. Losekoot, T. Genet, T. Jensen

3:11

Definition 21 (Unfolding a typing problem).

un f olds(Ω) = {( ω∈Ω E ω , ω∈Ω Ω ω , ) | ∀ω ∈ Ω, (E ω , Ω ω ) ∈ un f old(ω)} Example 22. un f olds({ω 0 , ω 1 }) = (E (3) ∪ E (D) , Ω (3) ∪ Ω (D) ), (E (3) ∪ E (C) , Ω (3) ∪ Ω (C) )
Finally, the proof system on typing problems consists of two deduction rules. The rule CONCLUDE concludes a proof when no typing obligation are left and when the algebraic datatype constraints are consistent. The rule STEP applies unfolding of typing problems using rules of the tree automaton.

Definition 23 (Proof system). Our proof system contains two rules.

CONCLUDE (E, ∅) STEP (E ∪ E , Ω ) (E, Ω) if Coherent(E) if Coherent(E ∪ E ) and (E , Ω ) ∈ un f olds(Ω)
Example 24. Continuing example 20, we build a proof tree of (E 0 , Ω 0 ). Rule CON-CLUDE cannot be immediately applied, so let us consider STEP, and thus un f olds(Ω 0 ).

Its element (E (3) ∪ E (D) , Ω (3) ∪ Ω (D) ) can be discarded because E (3) ∪ E (D) is con-
tradictory, as both constraints n = Z and n = S(m) are present. Its other element,

(E (3) ∪ E (C) , Ω (3) ∪ Ω (C) )
, is coherent, so we can apply the STEP rule. We write it (E 1 , Ω 1 )

where

E 1 = {l = Cons(l 1 , l 2 ), n = S(n 1 ), n = S(m)} and Ω 1 is the set of typing oblig- ations Ω 1 = {[ l 1 , : (A Len , q n )], [ l 2 , n 1 : (A Len , q f )],
[ m : (A Odd , q e )]}. We now have the new typing problem (E 0 ∪ E 1 , Ω 1 ). Rule CONCLUDE still cannot be applied. Then, un f olds(Ω 1 ) has 8 elements, only 4 of which are coherent. Its four coherent element can be seen as two times the almost-same two elements, the only difference being which rule has been applied to [ l 1 , : (A Len , q n )]. For this example, we only show the two elements that used rule (A), (E 2 , Ω 2 ) and (E 2 , Ω 2 ) with

E 2 = {l 1 = Z, l 2 = Nil, n 1 = Z, m = Z}, Ω 2 = ∅, E 2 = {l 1 = Z, l 2 = Cons(l 21 , l 22 ), n 1 = S(n 11 ), m = S(m 1 )}, Ω 2 = {[ l 21 , : (A Len , q n )], [ l 22 , n 11 : (A Len , q f )], [ m 1 : (A Odd , q o )]} Constraints E 1 ∪ E 2 are
coherent and Ω 2 is empty, so rule CONCLUDE can be applied and a solution can be built from

E 0 ∪ E 1 ∪ E 2 , that is {n → S(Z), l → Cons(Z, Nil)}.
The final proof tree is depicted on the right. For now, every proof tree is a single line. This will no longer be true with the introduction of the rule SPLIT in section 6.

STEP STEP CONCLUDE (E 1 ∪ E 2 , ∅) (E 1 , Ω 1 ) (∅, Ω 0 )
Definition 25 (Heights). We define a useful metric for proofs, the height:

-The height of a term t = f (t 1 , . . . , t n ) is inductively defined as h(t) = 1 + max i∈ 1,n (h(t i )).

-The height of a ground formula ϕ, written h(ϕ), is defined as the height of the highest term occurring in it.

-The height of a substitution σ together with a typing obligation ω = [ x 1 , . . . , x n : (A, q)] is defined as h(σ, ω) = max i∈ 1,n (h(σ(x i ))).

F S C D 2 0 2 3

3:12

Automata-based verification of relational properties of functions over data structures -The height of a substitution with a set of typing obligations is h(σ, Ω) = max ω∈Ω (h(σ, ω)).

-The height of a proof tree T, written h(T), is defined as the maximal number of occurrences of the STEP rule on a branch.

Theorem 26 (Proof system is correct and complete).

We have ∀(E, Ω), ∃σ, σ |= (E, Ω) ⇐⇒ (E, Ω). More precisely, for any (E, Ω) and n ∈ N, (A) For any proof tree T of (E, Ω) with h(T) = n, there exists a substitution σ such that σ |= (E, Ω) and h(σ, Ω) = n.

(B) For any substitution σ such that σ |= (E, Ω) and h(σ, Ω) = n, there exists a proof tree T of (E, Ω) such that h(T) = n.

The proof can be found in Appendix A.

Corollary 27 (Smallest counter-example). By theorem 26, a breadth-first exploration of proof trees for a given typing problem (E, Ω) admitting a solution yields a solution of minimal height, that is, a substitution σ that has the minimal value h(σ, Ω).

Proof search procedure

The search of a proof or the certainty of the absence of proof is implemented as a breadth-first exploration of the above-defined proof trees. This problem is undecidable in general [START_REF] Shimoda | Symbolic automatic relations and their applications to SMT and CHC solving[END_REF], thus this procedure either finds a solution to the typing problem (i.e. a counter-example to M |= ϕ) or tries every possibility and finds no counter-example (meaning that M |= ϕ), or diverges. We present two sound optimizations which significantly improve the proving and disproving power of the proof search procedure. Using those optimizations makes this procedure usable and efficient in practice (see experiments in Section 9).

The first optimisation consists in splitting independent typing obligations when they do not depend on each other.

Definition 28 (Independence). Let (E, Ω) be a typing problem with E coherent. Ω a ⊆ Ω and

Ω b ⊆ Ω are said independent w.r.t. E, written Ω a E Ω b , when ∀σ a , σ b , [σ E ; σ a |= Ω a ∧ σ E ; σ b |= Ω b ] ⇒ [∀x ∈ Vars(σ E (Ω a )) ∩ Vars(σ E (Ω b )), σ a (x) = σ b (x)]
Therefore, any two solutions σ a of (E, Ω a ) and σ b of (E, Ω b ) with Ω a E Ω can first be factorized by σ E by letting σ a and σ b such that σ a = σ E ; σ a and σ b = σ E ; σ b and then joined into σ ab = σ a ∪ σ b , and we have σ E ; σ ab |= (E, Ω a ∪ Ω b ). Finding a most precise partitioning of (E, Ω) into independent sub-problems is hard, as it may require to examine the shape of automata. We define below a safe and easy-to-compute approximation of these independence classes that splits typing obligations whose variables cannot be related even using the equalities of E.

Definition 29 (Splitting). Let E be a set of constraints. Let V E ([ x : (A, q)]) . = Vars(σ E ( x)).

The set V E ([ x : (A, q)]) is the set of variables remaining in a typing obligation after application of the most general unifier σ E of E. Note how (A, q) has not been used. We define

D E ⊆ Ω × Ω as D E (ω 1 , ω 2 ) . = (V E (ω 1 ) ∩ V E (ω 2 ) = ∅).
Since D E is symmetric, its reflexive and transitive closure D * E is an equivalence relation. We define the function Split(E, Ω) to return the equivalence classes of D * E defined on Ω.

Lemma 30. ∀Ω 1 , Ω 2 ∈ Split(E, Ω), Ω 1 E Ω 2 .

3:13

Proof. For any

Ω 1 , Ω 2 ∈ Split(E, Ω), Vars(σ E (Ω 1 )) ∩ Vars(σ E (Ω 2 )) = ∅. Therefore Ω 1 E Ω 2 .
This separation into independent problems makes the search less combinatorial and give rise to a new rule for our typing system:

SPLIT (E, Ω 1 ) . . . (E, Ω n ) (E, Ω) with {Ω 1 , . . . , Ω n } = Split(E, Ω)
Example 31 (Splitting (E 1 , Ω 1 )). In example 24, we had

E 1 = {l = Cons(l 1 , l 2 ), n = S(n 1 ), n = S(m)} and Ω 1 = {ω 1 , ω 2 , ω 3 } with ω 1 = [ l 1 , : (A Len , q n )], with ω 2 = [ l 2 , n 1 : (A Len , q f )],
and

ω 3 = [ m : (A Odd , q e )]. We have σ E 1 = {l → Cons(l 1 , l 2 ), n → S(n ), n 1 → n , m → n }, V E 1 (ω 1 ) = {l 1 }, V E 1 (ω 2 ) = {l 2 , n }, and V E 1 (ω 3 ) = {n }. Therefore Split(E 1 , Ω 1 ) = {ω 1 }, {ω 2 , ω 3 } .
Solving ω 1 have no impact on the solving of ω 2 and ω 3 because the values that l 1 can take do not influence the values that l 2 , n 1 , or m 2 can take. On the other hand, because of E 1 , m and n 1 must take the same value, and therefore typing obligations ω 2 and ω 3 cannot be separated. Note that applying this SPLIT rule before the second STEP (of example 24) would have separated (E 1 , Ω 1 ) into two independent problems.

The second optimisation consists in pruning the search tree. The search space is, for almost all typing problems, infinite. Without pruning, it would be impossible to cover the whole search space, and therefore negative instances would (almost) all never terminate. Pruning the search tree allows, in some cases, to finitely ensure that no typing proof exists.

Definition 32 (Pruning). Let T be a proof tree. A node (E b , Ω b ) that appears in the sub-tree of T whose root is some other node (E a , Ω a ) is prunable when both (i) At least one STEP rule is used on the path between (E a , Ω a ) and (E b , Ω b ) ;

(ii) ∃σ, σ(σ E a (Ω a )) ⊆ σ E b (Ω b ).
Theorem 33 (Safety of pruning). For any proof tree that contains a prunable node, there exist a strictly smaller (w.r.t the total number of times the STEP rule is used) proof tree with the same root.

The idea of pruning a proof T is to replace the orange proof sub-tree of (E a , Ω a ) with the purple proof tree of (E b , Ω b ) (with minor modifications).

Step Proof. Let T be a prunable tree, that is such that there exists nodes (E a , Ω a Therefore, the proof tree T whose sub-tree T a has been replaced by T a is valid and smaller.

Besides, we know that the sub-tree T a is strictly smaller than T a because T a contains at least F S C D 2 0 2 3

3:14

Automata-based verification of relational properties of functions over data structures one application of the STEP rule between its root and T b . Therefore, this transformation strictly decreases the size of the proof tree.

Corollary 34. By induction, if there exists a proof tree T of some initial typing problem, then there exists one without any prunable node along the proof tree, and therefore abandoning the search of prunable branches is safe.

Example 35 (Pruning of the search tree). During the second STEP application of example 24, the typing problem (E 2 , Ω 2 ) is also in un f olds(Ω 1 ). This was no problem, as the algorithm found a solution and stopped. Now, if (for example) automaton A Len did not have rule (D), then there would be no solution to the initial typing problem (E 0 , Ω 0 ). The search would never stop, as, after a bit of unification and renaming, (E 0 , Ω 0 ) can be included in

(E 1 ∪ E 2 , Ω 2 ).
Without pruning, the typing algorithm could therefore loop forever instead of returning None. Fortunately, (E 1 ∪ E 2 , Ω 2 ) can be pruned by taking σ = {l → l 22 , n → n 11 }, as σ(σ 0 (Ω 0 )) ⊆ σ 2 (Ω 2 ) (with σ 0 and σ 2 being most general unifiers of E 0 and

E 0 ∪ E 1 ∪ E 2 ,
respectively).

Regular structure inference

This section presents a procedure for inferring a regular model of a set of CHCs. The input set of CHCs we later use the procedure for is C = Γ ∪ Γ , with Γ defining a program and Γ the desired properties. The procedure follows the Implication Counter-Example (ICE) framework [START_REF] Garg | Ice: A robust framework for learning invariants[END_REF]. In this framework, the task of inferring a correct model is divided between two entities (or procedures), a learner and a teacher, working iteratively. There are three possible outcomes for this procedure: either the learner finds a correct model (that the teacher validates), the learner finds a contradiction, or the procedure loops forever with more and more refined models. in a different state for each. That is, for any atom R( t) of any ϕ ∈ C, there exists a state q in W (R)

such that R(W (R), q) = { t}.
This working model construction is carried out by classical automaton algorithms [START_REF] Hubert Comon | Tree Automata Techniques and Applications[END_REF]. The model W can then be generalised by merging states and deciding which equivalence classes are to be considered as final states. Merging states leads to additional terms being recognized and makes regularity appear. We search for a merging that minimises the number of states of W while ensuring that the resulting model satisfies C.

T. Losekoot, T. Genet, T. Jensen

3:15

Definition 37 (State merging problem). The minimisation problem we define is on the first-order (functional) signature S = {c q | A ∈ dom(W ) ∧ q ∈ Q(A)} ∪ {Final} containing only constants, one for each state of every automaton in W, and one unary predicate Final. The constraints are C ok ∪ C f . The set C ok represents essential constraints: (i) merged states must belong to the same automaton ; (ii) merged states must be of the same type ; (iii) any final state must be of its automaton's type. The set C f forces states to be or not to be final, which also have an impact on which states to merge. It is defined from C by transforming every clause

ϕ = R 1 ( t 1 ) ∧ . . . ∧ R n ( t n ) ⇒ R 0 ( t 0 )
into ϕ q = Final(c q 1 ) ∧ . . . ∧ Final(c q n ) ⇒ Final(c q 0 ), with each q i being the state of W (R i ) that recognizes exactly t i . Recall that we use non-Horn clauses, so the head of ϕ could be empty or contain multiple predicates.

A minimal solution • to the state merging problem can be computed by a finite model finder. We write Final for the set of final states of the solution and c q for the equivalence class of constant c q .

Definition 38 (Generalisation of working model). Given a solution • to the state merging problem, we generalise the working model

W by M with M(R) = (Q, Q f , ∆) with Q = { c q | q ∈ Q(W (R))}, Q f = Q ∩ Final and ∆ = { f ( c q 1 , . . . , c q n ) → c q 0 | f (q 1 , . . . , q n ) → q 0 ∈ ∆(W (R))}.
Example 39 (Learner: Model generation). We observe the ICE procedure after learner and teacher already had two exchanges to learn the Len relation defined in Section 2. The learner has accumulated the constraints {Len(Nil, Z), Len(Nil, Z) ⇒ Len(Cons(Z, Nil), S(Z))}.

The generated working model is

W = {Len → A} with A = (Q, Q f , ∆), Q = {q l 0 , q l 1 , q n }, Q f = ∅, and ∆ = { Nil, Z () → q l 0 ; Cons, S (q n , q l 0 ) → q l 1 ; Z, () → q n }. We have R(A, q l 0 ) = {(Nil, Z)}, R(A, q n ) = {(Z, )}, and R(A, q l 1 ) = {(Cons(Z, Nil), S(Z))}.
Note that state q n recognizes the term Z, which does not appear in C but is necessary to recognize (Cons(Z, Nil), S(Z)).

The minimisation problem is therefore on the signature with unary predicate Final and constant symbols c q l 0 , c q l 1 , and c q n . The constraints C ok are stating that q n cannot be merged with q l 0 nor q l 1 because they are not of the same type, and that only q l 0 and q l 1 can be final, as they are the only states of the automaton's type, natlist × nat. The constraints C f , generated from C, are {Final(c q l 0 ), Final(c q l 0 ) ⇒ Final(c q l 1 )}. The smallest model is a two-elements set {q l , q z }, with Final = {q l }, q l 0 = q l 1 = q l , and q n = q z . The generalized model is M = {Len → A } with automaton A having states {q l , q z }, final states {q l }, and transitions { Nil, Z () → q l , Cons, S (q z , q l ) → q l , Z, () → q z }.

This automaton recognizes an almost-correct relation: the set of pairs (l, n) of a list of zeros together with its size. The only missing rule is S, (q z ) → q z , which will be added by the learner in the ICE step that follows.

Approximation

As we suppose programs to be deterministic and terminating, the CHC representation of a functional program has only one possible model. For many programs, this model is not regular and cannot be represented using convoluted tree automata. As a result, trying to verify a property using an exact model of the relation will fail on such programs. We circumvent this problem by approximating relations.

Our verification goals are CHCs of the form ψ(

x) ∧ R 1 ( x 1 ) ∧ . . . ∧ R n ( x n ) ⇒ R 0 ( x 0 ).
Given a relation R we denote by R + (resp. R -) an over-approximation (resp. underapproximation) of R which can also be R itself. A safe way to prove the above implication F S C D 2 0 2 3

3:16

Automata-based verification of relational properties of functions over data structures using approximations is to over-approximate R 1 , . . . , R n and under-approximate R 0 . If

ψ( x) ∧ R + 1 ( x 1 ) ∧ . . . ∧ R + n ( x n ) ⇒ R - 0 ( x 0 )
is true then so is the original CHC. Applying such a reasoning on the CHCs of the verification goal, we can infer which relations can be over or under-approximated. For instance, the functional program computing the sum of two natural numbers is represented by the relation Plus(n, m, u) associating any two natural numbers n and m with their sum u. This relation is not regular when using unary encoding of numbers. The argument for seeing this is very similar to that of {a n • b n | n ∈ N} not being a regular string language. For the string automaton, it would require an unbounded counter for as in order to later exactly match their number with bs. For a convoluted tree automaton to recognize Plus(n, m, u), the counting is of the depth at which n and m root symbol stop being both S, which later needs to match the number of Ss left on u.

However, to prove a property of the form Plus(n, m, u) ⇒ n ≤ u, we only need a regular over-approximation of the relation Plus, say Plus + , and an under-approximation of ≤, say ≤ -, such that Plus + (n, m, u) ⇒ n ≤ -u.

In practice, we focus on over-approximation and do not under-approximate. We thus prove the stronger goal Plus + (n, m, u) ⇒ n ≤ u. Here are the clauses defining the Plus relation:

Plus(n, Z, n). Plus(n, m, u) ⇒ Plus(n, S(m), S(u)). Plus(v, w, x) ∧ Plus(v, w, y) ⇒ x = y.

These clauses form a system where the first clause invalidates under-approximations, the second clause can invalidate both over and under approximations, whereas the third only invalidates over-approximations. We can therefore obtain a safe approximation Plus + from Plus by simply removing the third clause. In our example, this suffices to prove Plus + (n, m, u) ⇒ n ≤ u because the approximation Plus + we built relates any n, m with all u greater than or equal to n (See the solver result for isaplanner_prop21.smt2 in http:// people.irisa.fr/Thomas.Genet/AutoForestation/results_right/benchmarks.html).

Finally, some relations cannot be approximated. If a relation appears on both sides of the verification goal then it cannot be approximated. E.g., to prove Z < m ∧ Plus(n, m, u) ⇒ n < u, we can safely use Plus + . Since < occurs (positively) on the left and right-hand side of the implication, we could use < + on the left-hand side and < -on the right-hand side.

We could use different approximations for relations appearing at different positions in the formula. However, in our analyser, we choose to use a common approximation for any relation. In our example, we use the intersection between < + and < -, which is exactly <.

Implementation and Experiments

We implemented the verification algorithm in Ocaml. It can be found on https://gitlab. inria.fr/tlosekoo/auto-forestation. This provides an implementation of terms, tree automata, model checking, model-inference procedure, as well as left, right, and complete convolution.

The teacher closely follows the depth-first search of the proof system described in section 5. There is a lot of redundancy in the proof search, so we used canonization and memoisation of typing problems. Memoisation avoids re-computing the unfolding of a typing problem if the search already did. However, memoisation alone is not very useful, as even equivalent typing problems are often different because of variable names. This is the reason for using canonization, which ensures that equivalent typing problems have the same internal representation. The learner delegates the merging of states to Clingo [START_REF] Gebser | Answer Set Solving in Practice[END_REF], a finite-model finder.

The solver presented in this paper builds regular relations, as opposed to [11, [START_REF] Kostyukov | Beyond the elementary representations of program invariants over algebraic data types[END_REF][START_REF] Matsumoto | Automata-based abstraction for automated verification of higher-order tree-processing programs[END_REF] which only build regular sets of terms. Since regular sets are a particular case of regular [START_REF] Claessen | Tip and isaplanner benchmarks[END_REF][START_REF] Dixon | Isaplanner: A prototype proof planner in isabelle[END_REF] and built relational problems inspired by TIP [START_REF] Claessen | Tip and isaplanner benchmarks[END_REF][START_REF] Claessen | Tip: tons of inductive problems[END_REF]. As shown in Section 2, a typical property which can be automatically proved by those non-relational solvers [11, [START_REF] Kostyukov | Beyond the elementary representations of program invariants over algebraic data types[END_REF][START_REF] Matsumoto | Automata-based abstraction for automated verification of higher-order tree-processing programs[END_REF] is of the form ∀x l. less Z (len (Cons(x, l))) where l is any list of natural numbers.

Non-relational solvers can also handle a restricted form of relations: the finite union of languages L 1 × . . . × L n where ∀i ∈ 1, n , L i is a regular language. This allows to prove properties with a limited form of relation. For instance, using a non-relational regular solver, it is possible to prove the property ∀l 1 l 2 . less Z (len l 1 ) ⇒ less Z (len (append l 1 l 2 )) where append is the function concatenating lists and l 1 and l 2 are lists of a. For the tuple of variables (l 1 , l 2 ) to cover all the possible cases, it is enough to consider the two languages L nil × L lists and L Cons+ × L lists where L nil = {Nil} and L Cons+ = L lists \ L nil . With the first language, the property is true because the left-hand side of the implication is false. With the second language L Cons+ × L list , both the left and right-hand side of the implication are true.

One of the simplest problem which cannot be proved using a non-relational "regular" solver is ∀x y. Cons(x, y) = y. Proving such a property cannot be done using a finite union of products of regular languages. However, this property can automatically be proven using our relational solver. Additionally to the above examples, we highlight some relational properties which are automatically proven using our solver.

-∀(l : ablist). (len l) = (len (reverse l)) length_reverse_eq.smt2

-∀(l 1 : ablist) (l 2 : ablist). (pre f ix l 1 (append l 1 l 2 )) prefix_append.smt2 -∀(l : ablist). (len l) = (len (sort l)) sort_length_eq.smt2 -∀(i : nat)(t 1 : natbintree)(t 2 : natbintree). t 1 = (node i t 1 t 2 ) tree_add_not_eq.smt2
On the following properties our solver is able to find a counter-example.

-∀(n : nat). n < (double n) nat_double_is_le.smt2

-∀(x : ab) (l : ablist). (delete_one x l) = (delete_all x l) list_delete_all_count.smt2

⇒ (count x l) = 1
On the following properties, our solver does not terminate due to trying to represent a non-regular relation (ICE loops).

-∀(x : ab) (l : ablist). (delete_one x l) = (delete_all x l) list_delete_all_count.smt2

⇒ (count x l) ≤ 1 -∀(n : nat) (m : nat). n + m = m + n plus_commutative.smt2

Related work

Other approaches for automatically proving algebraic and relational properties also rely on a CHC representation. The approach of [START_REF] Unno | Automating induction for solving horn clauses[END_REF] and [START_REF] Tsukada | Software model-checking as cyclic-proof search[END_REF] aims to solve the satisfiability problem of Horn clauses over any underlying theory supported by an SMT solver. This approach first reduces this problem to validity checking of first-order formulas with inductively-defined predicates. It is then based on syntactic proof, together with calls to the underlying theory solver. They design an inductive proof system tailored to Horn constraint solving. Using the theory of inductive datatypes, their method can reason about, and automatically prove, relational and algebraic properties.

Another approach, which is closer to ours, is that of [START_REF] Shimoda | Symbolic automatic relations and their applications to SMT and CHC solving[END_REF]. This approach aims to check properties on recursive data-structure by using symbolic automatic relations, which are (almost) the languages defined by symbolic synchronous automata (ss-NFA), the combination of symbolic automata and automatic relations. They devise a sound but (necessarily) incomplete procedure for checking if a given formula admits an assignment of its free variables that makes it true in a given ss-NFA. This procedure corresponds to the teacher procedure, but for ss-NFAs. They plan to implement an ICE-based CHC solver, but have left the model discovery (learner section) to future work.

By manually writing ss-NFAs, authors of [START_REF] Shimoda | Symbolic automatic relations and their applications to SMT and CHC solving[END_REF] are able to benchmark their verification procedure. Our approach and theirs seems to be complementary as they succeed on different sets of examples. This can be observed on the IsaPlanner benchmark where our technique fails on most of examples that [START_REF] Shimoda | Symbolic automatic relations and their applications to SMT and CHC solving[END_REF] In [START_REF] Boichut | Towards more precise rewriting approximations[END_REF], the authors present an expressive formalism for representing relations between trees called synchronized context-free programs. This formalism is more expressive than convoluted tree automata presented here. In particular, it can represent languages of the form {(g n (a), g n (b)) | n ∈ N} (like convoluted tree automata) and also languages of the form { f (g n (a), g n (b)) | n ∈ N} and {g n (h(g n (a))) | n ∈ N} (out of the scope of convoluted tree automata). This formalism is used to precisely approximate the set of outputs of a term rewriting system. However, [START_REF] Boichut | Towards more precise rewriting approximations[END_REF] does not show how to automatically infer such a representation from the term rewriting system.

Conclusion and future work

This paper demonstrates that it is possible to use tree automata as a basis for analysing the input-output behaviour of a first-order functional program. This shows that existing automata-based techniques for approximating the set of reachable states of a function can be extended to also compute relations between input and output of a function. Such relational analysis is key to scaling static analyses to larger programs, because it enables a modular, function-by-function analysis technique. The extension to relational analysis is based on the notion of tree automata convolution. We argue that the standard left-convolution can be complemented by other convolution techniques in order to verify more properties of T. Losekoot, T. Genet, T. Jensen

3:19

programs. Another technical contribution of the paper is the proof tree pruning used for verifying models of constrained Horn clauses. An efficient implementation of this proof search has been an essential part of the counter-example guided learner-teacher algorithm for inferring models from the CHC representation of the program to be analysed. This is confirmed by the benchmark used to evaluate our implementation of the verifier.

We believe our ICE procedure to be relatively refutationally complete and relatively complete on regular structures. Relative means that we suppose the termination of the model-checking procedure to be able to study the ICE cycle. Refutationally complete means that if the set of clauses C given to the ICE procedure is contradictory, then the procedure eventually finds a contradiction and stops. Complete on regular structures means that if the set of clauses C

given to the ICE procedure admits a regular model, then the procedure eventually finds a model of C. This has to be investigated further.

Fixing the convolution to be the either left or right convolution is however insufficient for proving non-trivial properties that would need a different overlay of terms, for example the height function on trees. Complete convolution can theoretically overcome this restriction but, as confirmed by our benchmarks, the size explosion of convoluted term makes it unusable in practice. We believe the convolution can and should be non-static, that is, being inferred together with the model.

Moreover, unlike the convolutions presented in this paper, we think that convolution could be lossy. For instance, if a subterm in a relation is not useful to prove a property, we think that we can forget about it in the convolution. Later on, if a new ground counterexample comes to the learner showing that the subterm was, in fact, necessary to prove the property then the convolution needs to be extended for that purpose.

F

  using only feedback from the teacher. The teacher's goal is to verify if the clauses from C satisfy M (the model proposed by the learner) and to give feedback in the form of logical implications which are counter-examples. Initially, M associates to each relation symbol an empty relation recognized by an empty automaton, denoted by A ∅ . The relation recognized by A ∅ , denoted by R(A ∅ ), is the empty relation. On our example, the initial value for M is thus M = {Len → A ∅ , Less → A ∅ }. verification of relational properties of functions over data structures

  be a typed alphabet for natural numbers and lists of natural numbers. Following are two examples of left convolution of terms.

  the < relation on Peano numbers and τ(A < ) = nat × nat. For example, the convolution of S(Z) and S(S(S(Z))) is recognized by this automaton, as shown below.

F

  verification of relational properties of functions over data structures depending on the constructor argument's order and being able to duplicate terms, but the drawback of generating big convoluted terms. Both convolution are extended to terms in the same way ⊕ L was.Example 12.

F S C D 2 0 2 3 3: 10 Automata-based verification of relational properties of functions over data structures Theorem 17 (Example 18 (

 3101718 Model checking as type checking).For each model M and CHC property ϕ, M |= ϕ ⇐⇒ ∃σ, ∃(E, Ω) ∈ tp(M, ϕ), σ |= (E, Ω). Model checking a property). Let ϕ be Len(l, n) ⇒ Even(n), a formula stating that all lists are of even length. Let M = {Len → A Len , Even → A Even } where A Len and A Even respectively define the length relation on integer lists and the even predicate of integers. A Len has states {q f , q}, final states {q f }, and rules {(A) : Z, () →

  ) and (E b , Ω b ) with respective proof trees T a and T b , with T b a sub-tree of T a with a STEP rule between (E a , Ω a ) and (E b , Ω b ), and σ a substitution such that σ(σE a (Ω a )) ⊆ σ E b (Ω b ).By theorem 26(A) there exists a substitution σ b with σ b |= (E b , Ω b ) and h(σ b , Ω b ) = h(T b ). Because σ E b is the most general unifier of E b and σ b |= E b , there exists σ such that σ b = σ E b ; σ . Therefore the substitution σ a = σ E a ; σ; σ is such that σ a (Ω a ) ⊆ σ b (Ω b ). Because σ b |= Ω b , we also have σ a |= Ω a . Because σ a first applies σ E a , we have σ a |= E a . Therefore σ a |= (E a , Ω a ).

Finally, again because

  σ a (Ω a ) ⊆ σ b (Ω b ), we have h(σ a , Ω a ) ≤ h(σ b , Ω b ). By applying theorem 26(B) there exists a proof T a of (E a , Ω a ) with h(T a ) = h(σ a , Ω a ) ≤ h(σ b , Ω b ) = h(T b ).

  The teacher's procedure takes as input a model M and a CHC system C, and returns an optional ground Horn clause. It returns None if M |= C, and Some(σ(ϕ)) if M |= ϕ with counter-example σ for some ϕ ∈ C. With the model checking procedure already defined, a teacher's implementation is only a matter of selecting an order in which to check the formulas. For example, taking as input the problem of example 18, the output would be Len(Cons(Z, Nil), S(Z)) ⇒ Even(S(Z)). The learner's procedure is responsible for inferring a model from examples or finding a contradiction. It takes as input a finite set C of ground CHCs and returns None if C is contradictory and Some(M) otherwise, with M being a smallest model (in the number of states) satisfying C. This procedure is divided into two steps, which are the main subject of this section, the working model generation and the working model generalisation. Definition 36 (Working model generation). The working model W of a given finite set of ground CHCs C is the smallest model (up to state renaming) recognizing exactly the terms mentioned in C

T. Losekoot, T. Genet, T. Jensen 3:17 relations

  , our solver should be able to handle the examples covered by those techniques, plus some relational problems. As a result, for the experiments, we choose some examples coming from benchmarks of Timbuk [11], add relational examples taken from the Isaplanner benchmark

0 2 3 3:18 Automata-based verification of relational properties of functions over data structures technique

  All of our experimental results for all convolution types are available at http://people. irisa.fr/Thomas.Genet/AutoForestation/. Because the properties of our database were mostly either on same-type relations or on lists and natural numbers, the right-convolution was the most efficient of convolution type. Left-convolution is not adapted for most of the list-based examples and complete-convolution revealed to be too costly in practice though it should help to prove properties on functions manipulating trees. On a total of 120 examples, is flexible enough to find such a model, with an efficiency comparable with non-relational solvers. For instance, on 11 examples coming from the Timbuk benchmarks, we proved 6 of them (with execution times around 2 seconds), disproved 3, and have a timeout on the 2 last.

	our solver (using right-convolution) proves 66, disproves 23, and timeouts on 31 after 60s.
	Our solver succeeds on 20 out of the 79 first-order Isaplanner examples in less than 60s (and
	18 in less than 5s). Our solver reveals to be more efficient on examples where a single level
	of structure have to be compared, i.e., natural numbers, lists of arbitrary elements, etc. It is
	generally unsuccessful on examples mixing several layers of structure, e.g., lists of natural

numbers, or on examples where a precise counting is required to prove the property. Finally, on examples where using a non-relational model suffices to prove the property, our solving F S C D 2

  handles (i.e.[START_REF] Claessen | Tip and isaplanner benchmarks[END_REF][START_REF] Claessen | Tip: tons of inductive problems[END_REF][START_REF] Khoussainov | Automatic Presentations of Structures[END_REF][START_REF] Kostyukov | Beyond the elementary representations of program invariants over algebraic data types[END_REF] 29, 30, 39, 42, 50, 62, 67, 71, 86) and succeeds on examples on which they do not report any success (i.e.[START_REF] Matsumoto | Automata-based abstraction for automated verification of higher-order tree-processing programs[END_REF][START_REF] Shimoda | Symbolic automatic relations and their applications to SMT and CHC solving[END_REF] 21, 22, 23, 24, 25, 26, 31, 32, 33, 34, 45, 46, 65, 69).

A Appendix

Proof of theorem 26

Proof of A. Let suppose that T proves (E, Ω) and h(T) = n. Let us proceed by induction on the last rule used in T.

-case CONCLUDE:

By hypothesis, we have that T is of the form (E, ∅) with Coherent(E), and therefore n = 0. Take σ = σ E a most general unifier of E, which is well-defined, as E is coherent. We have:

as Ω is empty.

-case STEP:

By hypothesis, we have that T is of the form STEP T (E, Ω) with T of the form . . .

and (E , Ω ) ∈ un f olds(Ω). By induction, we have that there exists σ with σ |= (E ∪ E , Ω ) and h(Ω , σ ) = h(T ). We also know that h(T ) = n -1. Take σ = σ . Then:

+ σ |= E : Immediate by σ |= E ∪ E and monotonicity of first-order logic.

+ σ |= Ω : Let ω = [ x : (A, q)] ∈ Ω. We must prove that σ( x) ∈ R(A, q). For this, it is sufficient (and necessary) to show that there exists a rule r = f ( q) → q of A such that

T. Losekoot, T. Genet, T. Jensen

3:21

Since (E , Ω ) ∈ un f olds(Ω), we know that there exists such a rule r with (E r , Ω r ) ∈ un f old(ω). The first property is immediate from σ |= E and E r ⊆ E while the second is immediate from σ |= Ω and Ω r ⊆ Ω .

+ h(Ω, σ) = n: Because (E , Ω ) ∈ un f olds(Ω), every variable y in Ω is such that there exists a variable x in Ω with σ(x) = f (. . . , σ(y), . . .) for some function f , that is,

Proof of B.

Let us build a proof tree by induction on h(Ω, σ).

In any case, let suppose that there exists σ such that σ |= (E, Ω) and h(Ω, σ) = n. We then construct a proof tree T of (E, Ω) such that h(T) = n.

-case h(Ω, σ) = 0: This is only possible when Ω = ∅. Take T = CONCLUDE (E, Ω) . This proof tree T is correct, as Ω = ∅ and E is coherent (because σ |= E). Also h(T) = 0.

-case h(Ω, σ) > 0:

Because σ |= Ω, we have, for each ω = [ x 1 , . . . , x n : (A, q)] ∈ Ω, that there exists an associated rule r ω = f 1 , . . . , f n (q 1 , . . . , q k ) → q such that

Therefore we can build three functions, F c , F t , F s , which assign to each such typing obligation and rule the following:

and Ω = ω∈Ω F t (ω). Note that (E , Ω ) ∈ un f olds(Ω).

Let σ = σ ∪ ω∈Ω F s (ω). We have:

+ σ is well-defined: Any binding of σ which is not in σ is of the form x j i = σ(t j i ) for some fresh variable x j i . Therefore, as σ is well-defined, so is σ .

+ σ |= E ∪ E : We have σ ⊆ σ , therefore σ |= E. Any constraint of E is of the form

) with x i a variable appearing in a node ω ∈ Ω, for which we therefore have

) by definition of F s (ω).

+ σ |= Ω : For any typing obligation ω ∈ Ω , we have ω ∈ F t (ω) for some ω ∈ Ω, so ω = [ x 1 , . . . , x n : (A, q j )] for some x 1 , . . . , x n such that σ (x 1 ), . . . , σ (x n ) ∈ R(A, q j ), by definition of F t (ω) and F s (ω).

. By definition of F t (ω) and F s (ω), we have both h(σ , Ω ) ≥ h(σ, ω) -1 and h(σ , Ω ) ≤ h(σ, ω) -1.

By induction on σ |= (E ∪ E , Ω ), we have that there exists a proof tree T of (E ∪ E , Ω ) such that h(T ) = h(σ , Ω ).

Therefore, take T = STEP T (E, Ω)

We have that T is a valid proof tree and that h(T) = h(T ) + 1 = h(Ω, σ).

F S C D 2 0 2 3