Inference of Tree Data Structure Invariant basedon Language Identification from Samples
Naoshi Tabuchi, Naoki Kobayashi, and Hiroshi Unno
Tohoku University

Abstract. We propose a method to infer invariants of tree data structures for higher-order functional programs. The method uses a machinelearning technique for identifying a regular tree language from samples.
The proposed method is combined with a recent technique for program verification based on higher-order model checking, yielding a fullyautomated verification method for higher-order, tree-processing functional programs. We have implemented the prototype verifier and conducted preliminary experiments.

1

Introduction

Finding good data invariants is often a key to the success of program verification.
For example, in Hoare logic, loop invariants allow us to reduce the problem ofproving a Hoare triple to that of proving the verification conditions. In typesystems, types express certain data invariants, and type checking, (i.e., checking
whether a program annotated with types is well-typed) is often much easier thantype inference.
In this paper, we are interested in the problem of finding invariants of tree
data structures, for a higher-order, tree-processing functional program. By theinvariant, we mean a regular tree language that overapproximates the set oftree data that an expression may evaluate to. An immediate application of thetree invariant inference is Unno et al.’s recent work on verification of higherorder tree processing programs [21]. They developed a semi-automated method
for proving that a given higher-order functional program satisfies given input
and output specifications, provided that the program is annotated with certain
invariants on tree data. For example, consider the following program, where `1and `2 are labels to identify subterms:
case x of e ⇒ e| a x ⇒ Append ((Reverse x)`1 ) (a e)| b x ⇒ Append ((Reverse x)`2 ) (b e)Append x y = case x of e ⇒ y| a x ⇒ a (Append x y)
| b x ⇒ b (Append x y)

Reverse x =The program manipulates tree data constructed from a tree constant e and unary
constructors a and b. The function Reverse takes a tree and returns the tree obtained by reversing the sequence of a and b. For example, Reverse(a(a(b(e))))returns b(a(a(e))). Suppose that we wish to verify that, given an element ofa∗ b∗ e1 , Reverse returns an element of b∗ a∗ e. By using Unno et al.’s method, it
suffices to declare invariants that the expression labeled by `1 evaluates to anelement of b∗ a∗ e, and the expression labeled by `2 evaluates to an element ofb∗ e. Thus, the combination of an algorithm to find such invariants with Unno
et al.’s method provides a fully-automated verification method for higher-ordertree-processing programs. Similar applications would be possible also to otherverification methods for functional programs that require certain invariant annotations, such as refinement type checking [4] and a combination of verification
condition generation and decision procedures for data structures [19].
The standard approach to finding invariants is to use static analyses. For
tree data structure invariants, Jones and Andersen [8] developed a kind of flow
analysis to approximate the value of each variable by a regular tree grammar.
Kochems and Ong [14] extended it to obtain more precise approximations byusing indexed grammars. Minamide [16] developed a method to infer the output
of a string-processing program as a context-free grammar. A limitation of thestatic analysis approaches is that they are often not precise enough for the verification methods mentioned above. For example, even for the simple program
above, we need context-sensitivity, to infer that Reverse x labeled with `1 returns an element of b∗ a∗ e while the same expression labeled with `2 returns anelement of b∗ e. If a context-insensitive analysis is used for invariant inference
and is combined with Unno et al.’s method, which is based on a kind of higherorder model checking [13], then the advantage of the preciseness of higher-ordermodel checking is lost. Another limitation, related to the above point, is thatthe static analysis approaches mentioned above are a kind of forward inference,
which propagates the input specification but does not take into account the output specification. Thus, it is difficult to adjust the precision and efficiency of
the analysis based on the final verification goal. For example, for the program
above, if the output specification is replaced with (a|b)∗ e, then the simple invariant (a|b)∗ e would suffice for `1 and `2 , but the static analyses may spend
much time in vain for finding more precise invariants.
In the present paper, we propose an alternative approach to invariant inference, based on a technique for learning regular tree languages from samples.
We use Besombes and Marion’s algorithm [2] that, given a finite set of (positive) samples and an oracle to answer a membership query, infers a regular tree
language. We assume that the overall verification goal is, given a program e
and regular tree languages LI and LO as the input and output specifications,to prove that e conforms to the input and output specifications, i.e., for any
tree t that belongs to LI , the value of e t belongs to LO . The goal of invariant
inference is then to find an invariant L for the subterm of M labeled by ` thatis sound in the sense that the subterm can only evaluate to an element of L,
and strong enough to prove that the value of e t belongs to LO . (This is analogous to the problem of, given a Hoare triple, finding loop invariants so that the1

We often identify linear trees with sequences, and use a regular expression for a setof linear trees.

Hoare triple can be reduced to verification conditions.) Our method proceeds
as follows. We first pick a finite set of elements of LI randomly, and run the
program, and check whether the outputs belong to LO . If so, we collect a set ofpairs (ti , Ei )(i ∈ {1, . . . , n}) such that the program evaluates to Ei [t`i ]. We thenuse t1 , . . . , tn as positive samples, and, as a membership oracle, the function thattakes a tree t0 and returns whether the value of Ei [t0 ] belongs to LO for everyi ∈ {1, . . . , n}. If the inferred language is not a valid invariant, we expand theset of inputs and repeat the procedure, until either a counterexample against the
input/output specifications is found, or a valid invariant is found. Our proceduredoes not terminate in general, but with certain assumptions, the procedure caneventually find a valid invariant.
Advantages of our invariant inference method include: (i) it is a combinationof forward and backward analyses, taking both the input and output specifications into account, and (ii) it is largely independent of the target language; itdoes not matter whether the target is higher-order/first-order, or pure/impure,
as long as we have a sound procedure to check the correctness of inferred invariants.
We have implemented the invariant inference algorithm and combined it with
Unno et al.’s verification method. According to preliminary experiments, thealgorithm works reasonably well, especially for linear trees (i.e., list-like data
structures).
The rest of the paper is organized as follows: Section 2 presents preliminary
definitions and notational conventions. Section 3 introduces a minimal functional calculus as a target language. Section 4 reviews language identification
techniques, the back-end of our method. Section 5 formalizes the procedure ofinvariant inference. Section 6 reports implementation and experiments. Section 7
compares our method with related work and Section 8 concludes.

2

Preliminaries

This section introduces (bottom-up) tree automata, which are used for expressing the specifications and invariants of programs.
We write dom(f ) for the domain of a mapping f . If X is a set, X ∗ denotes
the set of finite sequences of elements of X. We sometimes use the standard
regular expressions to denote a set of sequences, e.g., (a | b) for {a, b}, and(a | b)∗ for {a, b}∗ . We write  for the empty sequence. We write s1 · s2 for the
concatenation of sequences s1 and s2 . A (possibly empty) sequence v1 . . . vn isoften abbreviated to ve and |ev | denotes the length of ve.
A ranked alphabet Σ is a mapping from a finite set of symbols, called terminal
symbols, to non-negative integers. For each symbol a ∈ dom(Σ), Σ(a) denotes
the arity of a. The set TΣ of (finite) Σ-labeled ranked trees is inductively definedby: a t1 · · · tn ∈ TΣ if t1 , . . . , tn ∈ TΣ ∧ Σ(a) = n. In particular, a ∈ TΣ if
Σ(a) = 0. We let metavariable t range over TΣ . A tree context C is a term
obtained by replacing a subterm of a tree with a hole [ ]. When C is a treecontext and t is a tree, we write C[t] for the tree obtained by replacing [ ] witht. We write CΣ for the set of tree contexts.
A (bottom-up) finite tree automaton over Σ is a quadruple M = (Q, Σ, Qf , ∆)where Q is a finite set of states, Qf ⊆ Q is a set of final states and ∆ is a set oftransition rules. A transition rule is a rewrite rule of the form a q1 · · · qn → q
where q, q1 , . . . , qn ∈ Q and Σ(a) = n. We define the binary relation −→M on
TΣ∪{q7→0|q∈Q} by: C[a q1 · · · qn ] −→M C[q] ⇐⇒ a q1 · · · qn → q ∈ ∆ and
C is a tree context. A tree t is accepted by M iff t −→∗M qf for some qf ∈ Qf .
We write L(M) for the set of Σ-labeled ranked trees accepted by M and callit the language of M. An automaton is deterministic if for every a, q1 , . . . , qn ,there is at most one transition rule of the form a q1 · · · qn → q. This paper only
concerns deterministic bottom-up tree automata.

3

Target Language and Invariant Inference Problem

Our target language is an untyped, call-by-value λ-calculus with recursion andtree constructors/destructors; as mentioned in Section 1, our invariant inferencetechnique is largely independent of the choice of the language. We fix a ranked
alphabet Σ, and use its elements as tree constructors.

Definition 1 (Expressions). The set of expressions, ranged over by e, is givenby:e (expressions) ::= x | (fix f, x, e) | e1 e2| a | case e of {ai yei ⇒ ei }ki=1 | e`Here, e` denotes a labeled expression, for which we wish to infer invariants. We
assume that the whole expression (called a program) contains only one label `,just for the sake of simplicity; the actual implementation discussed in Section 6
handles a program with multiple labels.
The first line of the definition shows the standard constructs of λ-calculus:(fix f, x, e) denotes a (possibly) recursive function. We write λx.e when f is notfree in e. We sometimes use the letrec-binding of the form letrec f x ye = e1 in e2
as a syntax sugar for (λf.e2 )(fixf, x, λey .e1 ). The expression a(∈ dom(Σ)) denotes a tree constructor. The expression case e of {ai yei ⇒ ei } evaluates to[et/yei ]ei if the value of e is of the form ai et, and gets stuck otherwise. The operational semantics is shown in Figure 1. The evaluation gets stuck when there is
no applicable rule, e.g. because of type errors.

v (values)::= a v1 · · · vk | (fix f, x, e)E (evaluation contexts) ::= [ ] | E[[ ]` ] | E e | v E | case E of {ai yei ⇒ ei }ki=1
E[(fix f, x, e) v] −→ E[[(fix f, x, e)/f, v/x]e]E[t` ] −→ E[t]|et| = |yei |ee ei ]ei ]E[case ai t of {ai yei ⇒ ei }ni=1 ] −→ E[[t/yFig. 1. Operational Semantics

Example 1. We use the following program erev , discussed in Section 1, as a running example:
letrec append x y = case x of e ⇒ y| a x ⇒ a (append x y)
| b x ⇒ b (append x y)
inletrec reverse x = case x of e ⇒ e| a x ⇒ append (reverse x)` (a e)| b x ⇒ append (reverse x) (b e)in reverse
As mentioned in Section 1, given (i) a program e that takes a tree as an input
and returns a tree, and that has a labeled subexpression e0 , and (ii) regulartree languages LI and LO as the input and output specifications, the goal of
our invariant inference is to infer an invariant L such that (1) L is a soundapproximation of the value of e0 and (2) L is small enough to prove that thevalue of e t belongs to LO whenever t belongs to LI .
To formalize the two conditions above, we introduce the extended reduction
relation −→L shown in Figure 2. Rule Swap allows the value of a labeled expression to be replaced by an arbitrary element of the invariant L. Given a programe and input/output specifications LI and LO , we say that a tree language L isa forward invariant if L ⊇ {t | ∃tI ∈ LI .(e tI −→∗L E[t` ])} holds. Here, we use−→∗L instead of −→∗ to ensure that, when the label ` occurs inside a recursion(or a loop), the forward invariant is general enough for inductively showing that
it is indeed an invariant. For example, consider the following function:2
letrec f x y = (if y = 0 then x else (f x (y − 1)) + (f x (y − 1)))`
If x ranges over the set {0, 1}, then the set of values of the body of f is{0, 1, 2, 4, 8, . . .}, but it is not large enough to prove inductively that the return
value of f belongs to {0, 1, 2, 4, 8, . . .}. In our definition, the set of all non-negative
integers is a forward invariant but {0, 1, 2, 4, 8, . . .} is not.
2

We use integers for the sake of simplicity.

e −→ e0Base
e −→L e0t0 ∈ LSwap
E[t ] −→L E[t0 ]`Fig. 2. Extended Operational Semantics

T
We write Lfe,LI ,LO for the least foward invariant, i.e., {L | L ⊇ {t | ∃tI ∈LI .(e tI −→∗ E[t` ])}}. We just write Lf for the least foward invariant if e, LI , LO
are clear from the context. We say that a tree language L is a backward invariant
if∀t ∈ L.∀tI ∈ LI .∀E, t0 , t00 .(e tI −→∗Lf E[t0 ] ∧ E[t] −→∗ t00 =⇒ t00 ∈ LO )holds, and write Lbe,LI ,LO for the largest backward invariant.
Definition 2 (Invariant Inference Problem). Let e be a program and LI , LOregular tree languages. We say that L is a valid invariant and write |= (M, LI , LO , L)if Lfe,LI ,LO ⊆ L ⊆ Lbe,LI ,LO . An invariant inference problem Inf (e, LI , LO ) is the
problem of checking whether there exists a regular tree language L such that|= (e, LI , LO , L) holds, and if so, returns L.
Note that the problem above is undecidable in general. In Section 5, we
assume the existence of a sound (but not necessarily complete) procedure tocheck the condition |= (e, LI , LO , L), and give an (incomplete) procedure for theabove problem.
Remark 1. In the above formalization, a valid invariant L may not be a forward
invariant. Depending on the verification method, we may need to require that L
is also a forward invariant.
Example 2. Recall the program erev in Example 1. The invariant inference problem discussed in Section 1 is formalized as Inf (erev , a∗ b∗ e, b∗ a∗ e), and a solutionis b∗ a∗ e. Unno et al.’s method [21] serves as an oracle to check the condition|= (erev , a∗ b∗ e, b∗ a∗ e, L).34

Algorithm for Identifying Regular Tree Languages
from Samples

This section reviews Besombes and Marion’s algorithm [2], called Altex, forlearning regular tree languages from positive samples and membership queries.
We adopt this algorithm as a core machinery of our invariant inference procedure.
The algorithm Altex (∈ 2TΣ → (TΣ → {0, 1}) → TreeAutomata) takes a finite
set E of positive sample trees and an oracle o to answer membership queries,
3

Actually, to use Unno et al.’s method, we also need an invariant for the other occurences of reverse x in the body of reverse. It is easy to extend our invariant
inference algorithm to infer invariants for multiple labels.

and returns a (bottom-up) tree automaton whose language includes the given
samples. The oracle o should output 1 if the given tree is a member of thelanguage to be learned, and 0 otherwise. In our settings, (continuations of) the
program itself acts as the oracle, as we shall see later. In the sequel, we write
S(E) for the set of subtrees of trees in E.
We briefly sketch how Altex works. The algorithm is mostly treated as a
blackbox in this paper, so the reader may safely skip this paragraph for the
first reading. Given a set E of samples and a membership oracle o, Altex constructs an observation table, where each row is indexed by a subtree of an element of E and each column by a tree context. A cell T(t, C) of the table T
is filled by o(C[t]). Let row(t) be the sequence of 0, 1 in the row t. Then, Altex outputs the following automaton MT = (Q, Σ, Qf , ∆) induced by T as theresult of learning: Q = {qrow(t) | t ∈ S(E)}, Qf = {qrow(t) | o(t) = 1}, ∆ ={a qrow(t1 ) · · · qrow(tn ) → qrow(a t1 ··· tn ) | a t1 · · · tn ∈ S(E)}. At the initial
phase of the learning, the set of tree contexts {C | ∃t ∈ E.t = C[t0 ] for some t0 }generated from the sample set is used as the column set of the observation table.
During the learning, new tree contexts are added to the table until MT becomesa deterministic automaton.
We now review the property of Altex. The following is a sufficient condition
for the sample set.
Definition 3 (Representative Sample). Let L be a regular tree language,E ⊆ L and M the minimal automaton for L. A finite set E (⊆ L) is called a
representative sample of L if for each transition a q1 · · · qn → q of M, there
exists a tree a t1 · · · tn ∈ S(E) such that ti −→∗M qi (∀1 ≤ i ≤ n).
Intuitively, E is a representative sample if all the transition rules of M are used
for accepting trees in E.
The following is the key property of Altex, which states that learning of aregular language always succeeds if the sample set E is large enough, i.e., if it isa representative sample.
Theorem 1 (Besombes and Marion [2]). Let E be a finite subset of a regulartree language L and o the oracle for L. Then Altex(E, o) terminates and returns
a deterministic (bottom-up) tree automaton M. Further, if E is a representative
sample of L, M is the minimal (deterministic) automaton for L.
Example 3. Let L = b∗ a∗ e, and E = {b(b(a(e)))}. Altex constructs the following observation table.
ea(e)b(a(e))b(b(a(e)))

[]
1
1
1
1

b([ ]) b(b([ ])) b(b(a([ ])))
1
1
1
1
1
1
1
1
0
1
1
0

The automaton constructed from the table is M = (Q, {a, b, e}, Q, ∆) where Q ={q1110 , q1111 } and ∆ = {e → q1111 , a q1111 → q1111 , b q1111 → q1110 , b q1110 →q1110 }. Note that L(M) = b∗ a∗ e.

5Invariant Inference

We now present our procedure for invariant inference, using Altex as a backend.
The procedure roughly proceeds as follows. We first run a given program for some
inputs (chosen randomly but in a fair manner) and collect the sets U of values andthe set K of continuations of the labeled expression. We then use U as a sample
set for the invariant, and the function λx.“for every k ∈ K, k x returns a valid output”
as (an approximation of) the membership oracle for the invariant, and invoke
Altex. We then check whether the language output by Altex is a valid invariant by using an outside procedure. If the output is not a valid invariant,then we run the program for more inputs, to collect more samples and refine theapproximation of the membership oracle.
Below we first extend the operational semantics to collect values and continuations of the labeled expression in Section 5.1. We then describe the procedureand discuss its properties in Sections 5.2 and 5.3.
5.1

Extended Operational Semantics

In order to collect values and continuations, we extend the reduction relatione −→ e0 to (U, K, e) −→ (U 0 , K0 , e0 ). It is defined by the following rules.
e −→ e0Red(U, K, e) −→ (U, K, e0 )E ∈ K, t ∈ U
Switch(U, K, e) −→ (U, K, E[t])(U, K, E[t` ]) −→ (U ∪ {t}, K ∪ {E}, E[t])Memorize

Note that the reduction relation (U, K, e) −→ (U 0 , K0 , e0 ) is non-deterministic.
In a state (U, K, e), e can be reduced normally by using Red, or a pair of anevaluation context E and a tree t is picked up from K and U respectively, andE[t] is evaluated. When a labeled expression is evaluated to a tree value t, thetree t and its context E are memorized by rule Memorize.
5.2

Invariant Inference Procedure

Figure 3 shows our procedure for invariant inference. The procedure takes a
program e, an input specification LI and an output specification LO , and returns
an invariant L satisfying Verify(e, LI , LO , L) = true if such an L is found. Online 4, a sample input is chosen from LI . Here, we assume that Enum LI (i) isa surjective mapping from the set of positive integers to LI , so that every tree
in LI is eventually chosen. On line 5, Eval is a (non-deterministic) procedurethat returns a triple (Ui , Ki , t0 ) such that (Ui−1 , Ki−1 , e ti ) −→∗ (Ui , Ki , t0 ). If
the tree t0 does not conform to the output specification, the procedure is aborted
on line 6. Otherwise, an (approximation of) membership oracle is constructed
on line 7. It returns 1 (i.e., true) if it is provable (in some decidable logic) that
E[t] evaluates to a valid tree for every E ∈ Ki . On line 8, Altex is used to infer

an invariant candidate. On line 9, we assume that Verify is a sound procedure
to check whether |= (e, LI , LO , L) holds. If Verify returns L, then the inference
succeeds and L is returned as a witness. Otherwise, the procedure goes back toline 3 and iterates for next i.

1 : InferInvariants(e, LI , LO ) =2 : let (U0 , K0 ) = (∅, ∅) in
3 : for i ∈ {1, 2, . . .} do begin
4:
ti := Enum LI (i);5:let (Ui , Ki , t0 ) = Eval (Ui−1 , Ki−1 , e ti ) in // Evaluate the program with ti
6:
if t0 ∈
/ LO then (output “There is no valid invariant”; abort);7:
let oKi = λt.if ` ∀E ∈ Ki .∀t0 .(E[t] −→∗ t0 =⇒ t0 ∈ LO ) then 1 else 0 in
8:
let L = L(Altex(Ui , oKi )) in
9:
if Verify(e, LI , LO , L) = true then return L
10 : end
Fig. 3. The Procedure of Invariant Inference

Example 4. Recall the program in Example 1. Let LI = a∗ b∗ e and LO = b∗ a∗ e.
By choosing an input t1 = a(a(b(b(e)))), we get:(∅, ∅, erev t1 ) −→∗ (∅, ∅, E1 [(reverse (a(b(b(e)))))` ])−→∗ (∅, ∅, E2 [(reverse (b(b(e))))` ])−→∗ (∅, ∅, E2 [(b(b(e)))` ])−→∗ ({b(b(e))}, {E2 }, E2 [b(b(e))])−→∗ ({b(b(e))}, {E2 }, E1 [(b(b(a(e))))` ])−→∗ ({b(b(a(e))), b(b(e))}, {E1 , E2 }, b(b(a(a(e)))))
where E1 = append [ ] (a e) and E2 = E1 [E1 ]. Thus, we get U1 = {b(b(a(e))), b(b(e))}
and K1 = {E1 , E2 }. The membership oracle oK1 (x) returns 1 if and only if x is
an element of b∗ a∗ e. Altex constructs a table similar to the one in Example 3,
and returns the minimal automaton accepting b∗ a∗ e. This is a valid invariant,so that the procedure terminates and returns b∗ a∗ e.
If the output specification LO is replaced with (a | b)∗ e, then oK1 returns 1 forevery element of Ta,b,e . Thus, Altex returns an automaton accepting (a | b)∗ e,which is again a valid invariant.
2
5.3

Properties of the Procedure

This section discusses properties of our invariant inference procedure.
We make several
S assumptions. Let (U∞ , K∞ ) be the least fixedoint of thefunction λ(U, K). {(U 0 , K0 ) | (U, K, e tI ) −→∗ (U 0 , K0 , e0 ), tI ∈ LI }. First, we
assume that Eval is fair in the sense that (i) every pair (E, t) in (U∞ , K∞ ) is eventually put into Ui , Ki for some i, and (ii) for every t such that (U∞ , K∞ , e tI ) −→∗(U 0 , K0 , t) for some tI ∈ LI , Eval eventually returns t. Note that U∞ is the least
forward invariant (recall Section 3) and the set LB defined by:
LB := {t | ∀E ∈ K∞ , t0 .E[t] −→∗ t0 =⇒ t0 ∈ LO }is a backward invariant under this assumption. Secondly, we assume that Verify
is a complete procedure. Thirdly, ` ∀E ∈ Ki .∀t0 .(E[t] −→∗ t0 =⇒ t0 ∈ LO ) is
decidable, so that the oracle oKi is complete for the language defined by Ki .
The following properties follow immediately from the definition of the procedure and the above assumptions.
Fact 2 Let e be a program, and LI and LO are regular tree languages.
1. If there exist trees tI , tO such that e tI −→∗ tO with tI ∈ LI and tO 6∈ LO ,then the procedure eventually reports that there is no valid invariant.
2. If the procedure returns L, then |= (e, LI , LO , L) holds.
The algorithm does not terminate in general, however, even under the assumptions above. The main problems are:
1. The function oKi is only an approximation of the membership oracle for the?

backward invariant LB . Although oKi approaches the ideal oracle λx.x ∈ LB
in the limit, oKi may return a wrong answer for some input, for any finite i.
2. The (least) forward invariant U∞ may not contain a representative sample for
LB . Thus, the assumption for the correctness of Altex (recall Theorem 1)
is not met.
The first point can be remedied by slightly changing the algorithm: On line
8, instead of calling Altex for the pair (Ui , oKi ), call it for every pair (Ui , oKj )such that i ≤ j. Then, we have:
Theorem 3. Suppose that LB is a regular tree language and U∞ contains a
representative sample of LB , and that U∞ ⊆ LB . Then, the refined algorithm
eventually terminates and returns LB .
Proof. Let E be the representative sample contained in U∞ . Then, by the assumption on the fairness of Eval , E ⊆ Ui holds for some i. (Here, note that E
is a finite set by the definition of representative samples.) For Ui , Altex issues
only a finite set S of membership queries. Therefore, there exists j such that oKj
outputs the same answers for all the membership queries in S. Thus, by Theorem 1, Altex(Ui , oKj ) outputs LB . By the assumption on the completeness of
Verify, the procedure returns LB .
2
The above assumptions that LB is regular and that U∞ contains a representative sample of LB may be too strong in general. See Appendix for the discussion
on how to relax it.

6Experimental Results

We have implemented the algorithm presented in Section 5, and combined itwith Unno et al.’s EHMTT verifier, which is used as Verify in Figure 3. As
a result, we have obtained a fully-automated verifier for higher-order, treeprocessing functional programs. In the prototype, the reduction rule Switch
is suppressed, so that the evaluation for sample inputs is deterministic. A Web
interface to test the prototype and bechmark programs are available at http://www.kb.ecei.tohoku.ac.jp/∼tabee/atva/exp/.
Table 1 shows the experimental results. The columns “P” shows the numberof labeled expressions for which invariants are inferred. “R” and “S” show thenumber of functions and the size of the program respectively. The size of aprogram is measured by the number of symbols occurring in the program. The
column “I” shows how sample inputs are supplied: an integer k indicates thattrees of height up to k are automatically generated, while “m(n,k)” means thatn trees whose heights are up to k are manually given: for example, “m(2,12)”
indicates that two trees whose heights are ≤ 12 are manually given as test cases.
QI and QO respectively show the number of the states of tree automata for input
and output specifications, while ΣQA shows the sum of the number of the statesof tree automata for inferred invariants. Finally, “Y/N” indicates whether theinference was successful (“Y”) or not (“N”) and “T” shows the time taken for
the inference measured in seconds. “time-out” indicates that the inference did
not terminate. “fail” indicates that the inference did not succeed, but no more
sample inputs were available (on line 4 of the algorithm).

Program
P R S
I QI QO ΣQA Y/NTreverse2 2 24
4 2 2
3
Y
0.058
rev-rmsp
1 4 27
3 2 2
2
Y
0.139
inssort1 3 21
4 1 2
2
Y
0.053
mergesort
4 7 123
5 1 2
6
Y 11.669
lc-ucfirst 1 3 32
2 1 2
1
Y
0.019
rtrim
2 5 46
3 2 1
3
Y
0.145
ltrim-rtrim 3 6 39
4 3 1
7
Y
5.501
homrep-rev 1 11 78
3 4 2
2
Y
0.067
flatten1 2 16
5 3 2
2
Y
0.250
foldr
1 4 27
3 4 2
2
Y
0.014
map-foldr
2 6 46
4 4 2
5Y 22.860
addexp1 2 17
4 3 2
2
Y
0.013
addexp-add1 2 4 33
4 3 2
5
Y
0.088
split
4 5 86
12 7 9 56
N time-out
split
4 5 86 m(2,12) 7 9 56
Y 362.929
split’
1 5 75 m(2,12) 7 9 17Y 51.387
id-fail
1 2 6
2 2 3
1
N
fail
Table 1. Experimental Results

The programs from reverse to homrep-rev manipulate strings (represented
in the form of linear trees). reverse is the same as the program shown in Example 1: it takes an element of a∗ b∗ e and reverses it. rev-rmsp takes an elementof (a | s)∗ (b | s)∗ e, where s stands for the whitespace character, reverses the
input and removes all whitespace. inssort performs insertion sort on strings
over (a | b)∗ e, while mergesort performs the merge sort on strings of the sameform. lc-ucfirst takes a string over (a | b | A | B)∗ e, first lowers all As andBs and finally capitalizes the initial character (if any). rtrim takes a string over(a | b)∗ s∗ e and removes all the trailing whitespace. Similarly, ltrim-rtrim takes
a string over s∗ (a | b)∗ s∗ e and removes all the heading and trailing whitespace.
Finally, homrep-rev takes a word homomorphism h, a natural number n anda string w ∈ (a | b)∗ e and produces the reverse of the image hn (w). We let
h = {a 7→ bb, b 7→ a} and verified that if n is an even number and w ∈ a∗ b∗ e,then the reversed image is in b∗ a∗ e.
The programs from flatten to map-foldr manipulate lists. flatten takes alist of lists and returns the flattened list. foldr takes a list l of natural numbers
and a natural number x and performs foldr ∗ l x where ∗ is the multiplicative
operator. It is verified that the program returns an even number if x is even.
map-foldr also takes a natural-number list l and a natural x and performs
foldr ∗ (map (λx.2 ∗ x + 1) l) x. It is verified that it returns an odd number if
x is odd.
The program addexp is an evaluator of arithmetic expressions over natural numbers where the additive is the only operator. The verified property isthat an expression over even numbers evaluates to an even number. Similarly,
addexp-add1 takes an additive expression. It first adds one to each leaf of theexpression and evaluates it. It is verified that an expression over odd numbers
evaluates to an even number, respectively.
The program split is taken from a sample program of Cduce [1], a higherorder XML-centric functional language. It takes an arbitrarily nested lists ofpersons representing parent-child relationship and splits the children of each
person into a list of men (sons) and of women (daughters). The program split’is semantically equivalent to split, while the number of labeled expressions is
reduced to 1 by fusioning some functions and redundant expressions.
Finally, id-fail is the following identity function: let id x = x in id(id x)` , where the input and output specifications are respectively given by
LI = {e, a(e)} and LO = {e, a(e), a(a(e))}. It is an artificial example constructed to show a limitation of our invariant inference.
As shown in the table, our algorithm could successfully infer appropriate
invariants for all programs, except split and id-fail. As for programs fromreverse to addexp-add1, the total numbers of the states of the inferred regulartree languages range from 1 to 7 and the program size varies from 16 to 123.
Compared with them, the time taken for inference to terminate ranges widelyfrom 14 milliseconds to more than 22 seconds. This suggests that the effectivenessof our algorithm heavily depends on the choice of the sample input series, notonly on the complexity of the program and invariants.

For the program split, the naı̈ve enumeration of input samples resulted in
combinatorial explosion and did not terminate. Thus, sample input trees had tobe supplied manually, A smarter strategy of choosing samples would be required
for fully automated inference. The manual enumeration of inputs was also necessary for split’, but the inference was much faster. This indicates that the
programming style is also relevant to the efficiency of the inference.
For id-fail, the inference fails because of a limitation of Altex. The sample?

set Ui and the oracle oKi passed to Altex are {e, a(e)} and λt.(t ∈ {e, a(e), a(a(e))}
respectively, so that the assumption of Theorem 1 fails, i.e., Ui is not a representative sample of the language {e, a(e), a(a(e))}. Altex(Ui , oKi ) returns a∗ e,and there is no way to refine it as there are no further inputs.

7

Related WorkAs mentioned in Section 1, several static analysis methods have been proposed
for inferring invariants of tree- or string-processing programs [8, 14, 16]. A main
limitation of these approaches is context-insensitiveness. For example, consider
the following program let id x = x in let f y z = ... in f (id a) (idb). Jones and Andereson’s analysis [8] would infer {a, b} as the values of y and z,
rather than {a} and {b} for y and z. Kochems and Ong [14] refined their analysis
by introducing a restricted form of context-sensitivity by using index grammars,
but it still suffers from similar problems. In contrast, our learning-based approachis context-sensitive, as we actually evaluate the program (for sample inputs) andcollect the values of each expression. There are also limitations of our approach,that the procedure may not terminate in general, and (even it terminates) that
there is no theoretical bound for the complexity of invariant inference. Thus, wethink the standard static analysis approach and our approach should be used ascomplementary methods.
In Section 6, we have combined our invariant inference technique with Unno
et al.’s method for verification of tree-processing programs [21]. Their method
is based on higher-order model checking [11, 13, 17], but requires invariant annotations for certain program points. By the combination with the invariant inference technique, we have enabled fully automated verification of higher-ordertree-processing programs. We expect that a similar combination with other verification methods is possible; for example, our invariant inference can be used for
replacing the binding analysis part of Ong and Ramsay’s verification method [18].
As their method is also based on higher-order model checking, the contextsensitivity of the binding analysis is important for fully exploiting the precisionof higher-order model checking.
There are other pieces of work to infer invariants based on test execution
or machine learning techniques [3, 5, 6, 10]. For example, Jung et al. [9, 10] presented a method for inferring loop invariants for a simple while-language. Our
combination of forward and backward information for invariant inference has
also some similarity to interpolant-based techniques for invariant or predicate
discovery [7, 15, 20]. To our knowledge, however these techniques are mainly forthe inference of numeric or non-recursive symbolic constraints, and it is not clear
how to lift them to infer invariants in the form of regular tree languages.

8

Conclusion and Future Work

We have proposed a method for inferring regular tree language invariants of tree
processing programs. The proposed approach is based on test execution anda technique of language identification from positive samples and membership
queries. We have combined it with a previous verification method requiring invariant annotations, and implemented a fully automated verifier for higher-ordertree processing programs. The preliminary experiments indicate that our invariant inference works reasonably well for small programs. Future work includes
optimizations of the invariant inference procedure to achieve more scalability.
For example, a more elaborated strategy for test-case generation would enable
faster convergence of invariant inference.

References
1. V. Benzaken, G. Castagna, and A. Frisch. Cduce: an xml-centric general-purpose
language. SIGPLAN Not., 38:51–63, August 2003.
2. J. Besombes and J.-Y. Marion. Learning tree languages from positive examples
and membership queries. Theor. Comput. Sci., 382:183–197, September 2007.
3. C. Csallner, N. Tillmann, and Y. Smaragdakis. DySy: dynamic symbolic execution
for invariant inference. In International Conference on Software Engineering 2008,
volume 2008, pages 0–18. Association for Computing Machinery, One Astor Plaza
1515 Broadway, 17 th Floor New York NY 10036-5701 USA, 2008.
4. R. Davies. Practical refinement-type checking. PhD thesis, Pittsburgh, PA, USA,2005.
5. M. Ernst, J. Cockrell, W. Griswold, and D. Notkin. Dynamically discovering likely
program invariants to support program evolution. Software Engineering, IEEE
Transactions on, 27(2):99–123, 2002.
6. S. Hangal and M. S. Lam. Tracking down software bugs using automatic anomaly
detection. In Proceedings of the 24th International Conference on Software Engineering, ICSE ’02, pages 291–301, New York, NY, USA, 2002. ACM.
7. T. A. Henzinger, R. Jhala, R. Majumdar, and K. L. McMillan. Abstractions fromproofs. In Proceedings of POPL 2004, pages 232–244. ACM Press, 2004.
8. N. D. Jones and N. Andersen. Flow analysis of lazy higher-order functional programs. Theor. Comput. Sci., 375(1-3):120–136, 2007.
9. Y. Jung, S. Kong, B. Wang, and K. Yi. Deriving invariants by algorithmic learning,decision procedures, and predicate abstraction. In Verification, Model Checking,and Abstract Interpretation, pages 180–196. Springer, 2010.
10. Y. Jung, W. Lee, B. Wang, and K. Yi. Predicate Generation for Learning-Based
Quantifier-Free Loop Invariant Inference. Tools and Algorithms for the Construction and Analysis of Systems, pages 205–219, 2011.
11. N. Kobayashi. Model-checking higher-order functions. In Proceedings of the 11th
ACM SIGPLAN conference on Principles and practice of declarative programming,
PPDP ’09, pages 25–36, New York, NY, USA, 2009. ACM Press.

12. N. Kobayashi. TRecS. http://www.kb.ecei.tohoku.ac.jp/∼koba/trecs/, 2009.
13. N. Kobayashi, N. Tabuchi, and H. Unno. Higher-order multi-parameter tree transducers and recursion schemes for program verification. In Proc. of POPL, pages
495–507. ACM Press, 2010.
14. J. Kochems and C.-H. L. Ong. Improved functional flow and reachability analyses
using indexed linear tree grammars. In Proceedings of RTA 2011, 2011.
15. K. McMillan. Quantified invariant generation using an interpolating saturation
prover. Tools and Algorithms for the Construction and Analysis of Systems, pages
413–427, 2008.
16. Y. Minamide. Static approximation of dynamically generated web pages. In Proceedings of the 14th international conference on World Wide Web (WWW 2005),
pages 432–441. acm, 2005.
17. C.-H. L. Ong. On model-checking trees generated by higher-order recursion
schemes. In LICS 2006, pages 81–90. IEEE Computer Society Press, 2006.
18. C.-H. L. Ong and S. J. Ramsay. Verifying higher-order functional programs withpattern-matching algebraic data types. In Proceedings of the 38th annual ACM
SIGPLAN-SIGACT symposium on Principles of programming languages, POPL
’11, pages 587–598, New York, NY, USA, 2011. ACM.
19. P. Suter, M. Dotta, and V. Kuncak. Decision procedures for algebraic data types
with abstractions. In Proc. of POPL, pages 199–210, 2010.
20. H. Unno and N. Kobayashi. Dependent type inference with interpolants. In
Proceedings of the 11th ACM SIGPLAN conference on Principles and practiceof declarative programming, PPDP ’09, pages 277–288, New York, NY, USA, 2009.
ACM.
21. H. Unno, N. Tabuchi, and N. Kobayashi. Verification of tree-processing programs
via higher-order model checking. In Proceedings of APLAS 2010, volume 6461 of
LNCS, pages 312–327. Springer-Verlag, 2010.

A

Further Discussion on Termination of Invariant
Inference

Theorem 3 makes a rather strong assumption that U∞ is a representative sample
of LB . Without this assumption, the algorithm may not terminate. In fact, as
discussed in Section 6, for the following input:e ≡ let id x = x in id (id x)`
LI = {e, a(e)}LO = {e, a(e), a(a(e))}?

Altex is called with the sample set {e, a(e)} and the oracle λx.(x ∈ LO ). With
these inputs, Altex constructs the following observation table:[]e1a(e) 1a([ ])
1
1

The language of the automaton M = ({q11 }, {a, e}, {q11 }, {e → q11 , a q11 →q11 }) induced by the table is thus a∗ (e), which is larger than LB = LO , so thatthe verification of |= (e, LI , LO , a∗ (e)) fails.
A possible way to overcome the above limitation is to extend Altex. In
addition to positive samples E and the membership oracle o, let us assume that
another oracle f to test the inclusion relation is available: The new oracle fshould take a regular tree language X as input, check whether X ⊆ L (where L
is the language to be learned), and if X 6⊆ L, return an element of X \ L as acounterexample. We can then modify Altex so that, given E, o and f , it returns
a subautomaton of the minimal automaton for accepting L, no matter whether
E is a representative sample.
In the example above, if we get a(a(a(e))) as a counterexample of a∗ e ⊆{e, a(e), a(a(e))}, then we can add the context a(a([ ])) to the table, and obtainthe new observation table:[]e1a(e) 1a([ ]) a(a([ ]))11
10The inferred automaton is then M1 = ({q110 , q111 }, {a, e}, {q111 , q110 }, {e →q111 , a q111 → q110 }) and L(M1 ) = {e, a(e)}.
By using the extended version of Altex, we expect that the terminationof the invariant inference is guaranteed without the assumption that U∞ is a
representative sample of LB . The technical details are rather complex, and left
for future work.