Automata-Based Abstraction for Automated
Verification of Higher-Order Tree-Processing
Programs
Yuma Matsumoto1 , Naoki Kobayashi1 , and Hiroshi Unno2
1
2

The University of Tokyo
University of Tsukuba

Abstract. Higher-order model checking has been recently applied toautomated verification of higher-order functional programs, but there
have been difficulties in dealing with algebraic data types such as lists
and trees. To remedy the problem, we propose an automata-based abstraction of tree data, and a counterexample-guided refinement of theabstraction. By combining them with higher-order model checking, we
can construct a fully-automated verification tool for higher-order, treeprocessing functional programs. We formalize the verification method,
prove its correctness, and report experimental results.

1

Introduction

Higher-order model checking [15, 9], or the model checking of higher-order recursion schemes (HORS), has been recently applied to automated verification offunctional programs [9, 19, 16, 11, 18]. Since a HORS is essentially a simply-typed
higher-order functional program with recursion and finite base types (such as
Booleans, not integers), the control structure of a (higher-order) functional program can be precisely modeled and verified. Thus, with a suitable abstraction ofdata, we can verify functional programs fully automatically by using higher-ordermodel checking. For example, Kobayashi et al. [11] used predicate abstraction
and CEGAR (counterexample-guided abstraction refinement) for abstracting integers to Booleans, and constructed a fully automated verification tool MoCHi
for simply-typed higher-order functional programs with recursion and integers.
There have, however, been limitations in the treatment of algebraic datatypes such as trees and lists. Sato et al. [18] extended MoCHi to deal with algebraic data types by encoding algebraic data into functions; for example, a list
may be encoded as a function that maps an index to the corresponding element.
That approach has not been so successful, because the encoding makes both programs and specifications complex. In another line of work, Kobayashi et al. [12]proposed a verification method for HMTT, a kind of higher-order tree transducers. The HMTT model is however much more restricted than the usual functional
programs: there is a distinction between input and output trees, and input trees
are read-only, and output trees are write-only. Unno et al. [19] later extended
HMTT to allow conversion between input and output trees so that the model isas expressive as an ordinary functional language, but annotations are required
for the conversion. Ong and Ramsay [16] introduced a verification method for an
extension of HORS called pattern-matching recursion schemes (PMRS). PMRS
supports pattern matching on tree-structured data, but the verification method,
however, uses pattern-based abstraction, which is not powerful enough.
To remedy the situation above, we propose a new approach to using higherorder model checking for automated verification of higher-order tree-processing
programs. As in [11], we apply abstraction to approximate a source programby a higher-order functional program over finite base types, so that the lattercan be verified by higher-order model checking. Instead of using predicates on
integers, however, we use an automaton for abstracting tree data: each tree isabstracted to a state of the automaton that accepts the tree. Using the automatabased abstraction, we can transform a higher-order tree-processing program toa higher-order functional program with finite data domains, so that the latteroverapproximates the behavior of the source program. Thus, verification problems for the former can be reduced to those for the latter, which can further be
reduced to higher-order model checking.
As an example, consider the following program.
double x = twice (add x) Z.
twice f x = f(f x).
add x y = match x with Z => y | S x’ => add x’ (S y).
Here, Z and S are tree constructors. The program consists of two functions double
and add . The main function double takes a natural number x (in the unary tree
representation) and returns x + x. Suppose that we wish to verify that theoutput of double is always even, i.e, a unary tree of the form (S)2n Z. We canuse a tree automaton that distinguishes (S)2n Z and (S)2n+1 Z, consisting of two
states q0 , from which trees of the form (S)2n Z is accepted, and q1 , from whichtrees of the form (S)2n+1 Z is accepted. Using the automaton, the program above
is abstracted to:main() = (double q0 )(double q1 ).
double x = twice (add x) Z.
twice f x = f(f x).
s x = match x with q0 => q1 | q1 => q0
add x y = match x with q0 => y(add q1 (s y)) | q1 => add q0 (s y).
Here,  represents a non-deterministic choice, and s is now a function on states.
The new main function main non-deterministically invokes double q0 or double
q1 ; here, the argument of double is now a state of the automaton, instead of atree. The call double q0 (double q1 , resp.) simulates the case where the input
is an even (odd, resp.) number. The case analysis on tree x in function add has
now been replaced by a case analysis on states. The case x = q0 models the casewhere x is of the form (S)2n z in the source program; since both of the branches
are possible in the source program, the abstract program non-deterministicallyevaluates (the abstract version of) them. On the other hand, the case x = q1
models the case where x is of the form (S)2n+1 Z; since only the second branchof the source program is possible, the abstract program evaluates add q0 (s y)deterministically. To check that the return value of the source program is alwaysprogram
newautomata

automata-based
abstraction
abstracted
programhigher-ordermodel checking

automata
splittingconstraints on
automata

No

error
path

infeasible
feasibility checkfeasibleYes
Yes

No (counterexample)

Fig. 1. Our method

even (given (S)n Z as an input), it suffices to check that the return value of theabstract program is always q0 .
Figure 1 illustrates our overall method. As mentioned above, we apply an
automata-based abstraction to reduce a given verification problem to that on afunctional program with finite data domains. The latter problem can be decided
by a reduction to higher-order model checking [9]. If the abstract program has
no error path then we can conclude that the answer to the original verification
problem is “yes”. Otherwise, we inspect an error path returned by a higherorder model checker. If a source program has a corresponding error path, we canconclude that the answer to the original verification problem is “no”. Otherwise,
the abstraction was not precise enough, so the automaton used for abstraction isrefined, and the cycle is repeated until the answer is found. (Since the verification
problem is undecidable, the cycle may be repeated forever.)A challenge arises on how to refine the automaton used for abstraction when aspurious error path is found. Unlike the case for predicate abstraction for integer
values [11], we cannot use an interpolant-based method for predicate discovery.
Given an initial automaton for abstraction, we split each state of the automaton
to obtain a new automaton with an unknown transition function. From spurious
error paths, we accumulate constraints on the transition function, which represent necessary conditions for eliminating spurious error paths. Then by using an
SMT solver, we obtain a transition function that satisfies the constraints. This
refinement procedure is relatively complete, in the sense that if there exists anautomaton with which the abstract program can be proved to be safe, the procedure can eventually find such an automaton and the verification succeeds. The
rest of this paper is organized as follows. Section 2 reviews the definitions of tree
automata. Section 3 introduces our verification problem. Section 4 formalizes
the automata-based abstraction. Section 5 describes an abstraction refinementmethod. Section 6 reports experimental results. Section 7 discusses related work,
and Section 8 concludes this paper.

2

Preliminaries

In this section, we recall the standard notion of tree automata [4], which will be
used for program specification and also for abstraction.
A ranked alphabet, written Σ, is a map from a finite set of symbols to theset of non-negative integers. An element C of dom(Σ) (the domain of Σ) may
be considered a tree constructor of arity Σ(C). The set TreesΣ of finite trees
is inductively defined by: T1 , . . . , TΣ(C) ∈ TreesΣ ⇒ C T1 · · · TΣ(C) ∈ TreesΣ .
Note that Σ(C) may be 0 above, so C ∈ TreesΣ if Σ(C) = 0.
Definition 1 (tree automata). A (bottom-up) tree automaton M is a quadruple(Σ, Q, ∆, F ) where (i) Σ is a ranked alphabet. (ii) Q is a set of states. (iii) ∆,called a transition function, is a subset of dom(Σ)×Q∗ ×Q such that (C, q1 · · · qn , q)
∈ ∆ implies n = Σ(C). (iv) F is a subset of Q. Elements of F are called final
states. We define the transition relation T −→M T 0 on TreesΣ∪{q7→0|q∈Q} by:
C q1 · · · qn −→M q

if (C, q1 · · · qn , q) ∈ ∆.

A tree T ∈ TreesΣ is accepted by M if T −→∗M q ∈ F for some q. The
language accepted by M, written L(M), is the set of trees accepted by M. We
often write ΣM , QM , ∆M , FM for the four components of M. We write L(M, q)
and L(M, Q) for L((ΣM , QM , ∆M , {q})) and L((ΣM , QM , ∆M , Q)) respectively. An automaton (Σ, Q, ∆, F ) is deterministic if for every C ∈ dom(Σ) and
q1 · · · qΣ(C) ∈ Q∗ , there exists at most one q such that (C, q1 · · · qΣ(C) , q) ∈ ∆. An
automaton (Σ, Q, ∆, F ) is total if for every C ∈ dom(Σ) and q1 · · · qΣ(C) ∈ Q∗ ,there exists at least one q such that (C, q1 · · · qΣ(C) , q) ∈ ∆. When an automaton
M is deterministic and total, we write ∆M (C, q1 · · · qΣM (C) ) for the state q suchthat (C, q1 · · · qΣM (C) , q) ∈ ∆M .
Example 1. Consider an automaton M = (Σ, {q1 , q2 , q3 }, ∆, {q1 , q2 }) where Σ ={E 7→ 0, A 7→ 1, B 7→ 1} and∆ = {(E, , q1 ), (A, q1 , q2 ), (A, q2 , q2 ), (A, q3 , q3 ), (B, q1 , q1 ), (B, q2 , q3 ), (B, q3 , q3 )}The automaton M is total and deterministic, and L(M) = A∗ B∗ E. Here, wehave identified unary trees with words, and used a regular expression for a setof unary trees. The regular expression A∗ B∗ E denotes{A(· · · (A(B(· · · (B E))))) | m ≥ 0, n ≥ 0}.
| {z } | {z }mnWe often use this kind of notation for a set of unary trees.
Henceforth, we consider only deterministic and total automata; this does not
lose generality, as we are considering bottom-up automata.

3

The Verification Problem

This section introduces the language of tree processing programs, which is usedas the target of our verification, and defines the verification problem. The targetof verification is a higher-order, tree-processing functional program. We fix aranked alphabet Σ. We sometimes write {ei }ni=1 for {e1 , . . . , en }, and also write{f (x)}x∈S for {f (x) | x ∈ S}.
Definition 2. The set of expressions, ranged over by e, is given by:e ::= C | x | fail | e1 e2 | case e of {Ci yei ⇒ ei }ni=1 .
Here, C ranges over dom(Σ), and x ranges over the set of variables and function
symbols. A program P is a set of function definitions {f1 x
f1 = e1 , . . . fm xf
m =em } where fi is a function symbol, and xei is a sequence of variables. The set offunction symbols {f1 , . . . , fm } must contain the main function symbol “main”.
We write arity(fi ) for the length of the sequence xei .
The expression fail aborts the execution. The expression case e of {Ci yei ⇒ei }ni=1 evaluates e to a tree, and then evaluates [Te/yei ]ei if the tree matches
Ci Te. We assume that the patterns of every case expression are exhaustive; if
not, we can insert a clause Ci yei ⇒ fail. We consider only programs that are
well-typed in the standard simple type system. The set of (simple) types, ranged
over by κ, is given by: κ ::= o | κ1 → κ2 . Here, o is the type of trees, andκ1 → κ2 is the type of functions from κ1 to κ2 . A type judgment is of the formK ` e : κ, where K is a map from a finite set of variables (which may include
function symbols) to the set of types. It is defined by the following rules.
K `C :o· · → o} → o| → ·{zΣ(C)K, x : κ ` x : κK ` e1 : κ1 → κ2
K ` e2 : κ1
K ` e1 e2 : κ2

K `e:oK, yei : eo ` ei : κ(for each i ∈ {1, . . . , n})K ` case e of {Ci yei ⇒ ei }ni=1 : κWe write ` P : K if: (i) P = {fi xi,1 · · · xi,ki = ei }ni=1 ; (ii) dom(K) = {f1 , . . . , fn };(iii) K(fi ) = κi,1 → · · · → κi,ki → o and K, xi,1 : κi,1 , . . . , xi,ki : κi,ki ` ei : o forevery i ∈ {1, . . . , n}; and (iv) K(main) = o → o. A program P is well-typed if` P : K for some K. Henceforth, we consider only well-typed programs.
The sets of evaluation contexts and values are defined respectively by:K ` fail : κE (evaluation contexts) ::= [ ] | E v | e E | case E of {Ci yei ⇒ ei }ni=1
v (values) ::= f v1 · · · vn (n < arity(f )) | C v1 · · · vn (n ≤ Σ(C))
The reduction relation e −→P e0 is defined by: (i) E[fail] −→P fail;(ii) E[f v1 · · · vn ] −→P E[[v1 · · · vn /x1 · · · xn ]e] if f x1 · · · xn = e ∈ P; and(iii) E[case ak ve of {Ci yei ⇒ ei }ni=1 ] −→P E[[ev /yek ]ek ]. We often omit the subscript P.

Example 2. The program in Section 1 is expressed as:
P1 = {main x = twice (add x) Z, twice f x = f (f x),
add x y = case x of Z ⇒ y | S x0 ⇒ add x0 (S y)}
The expression main (S(Z)) is evaluated as follows.
main (S(Z)) −→ twice (add (S(Z))) Z −→ add (S(Z))(add (S(Z)) Z) −→∗ S(S(Z)).
Definition 3 (verification problem). Let MI and MO be tree automata.
We write |= (P, MI , MO ) if, for every T ∈ L(MI ), main T −→6 ∗P fail and∗00main T −→P t ∈ TreesΣ implies t ∈ L(MO ). The verification problem(P, MI , MO ) is the problem of deciding whether |= (P, MI , MO ) holds.
Intuitively, |= (P, MI , MO ) means that given a tree accepted by MI as an
input, P does not fail, and if it returns a (finite) tree, it is accepted by MO .
Example 3. Consider the verification problem (P1 , M1 , M2 ) where P1 is the
program given in Example 2, and
M1 = (Σ, {q1 }, ∆1 , {q1 })∆1 = {(Z, , q1 ), (S, q1 , q1 )}M2 = (Σ, {q2 , q3 }, ∆2 , {q2 }) ∆2 = {(Z, , q2 ), (S, q2 , q3 ), (S, q3 , q2 )}The languages accepted by M1 and M2 are (S)∗ Z and (S S)∗ Z respectively. The
answer to the verification problem (P1 , M1 , M2 ) is “yes”.

4

Automata-Based Abstraction

This section formalizes our automata-based abstraction method.
4.1

Abstract Programs

The target language of the automata-based abstraction has a finite enumeration
type as the base type, instead of tree types. The enumeration type consists ofthe states of automata used for abstraction.
Definition 4 (abstract programs). The set of (abstract) expressions, ranged
over by t, is given by: t ::= q | x | t1 t2 | case t of {qi ⇒ ti }mi=1 | t1  t2 | fail.
Here, q ranges over the set {q1 , . . . , qm } of values of the finite enumeration typeand x ranges over a set of variables (including defined function symbols fi ’s). An
abstract program D is a set of function definitions {f1 x
f1 = t1 , . . . , fn x
fn = tn },where main ∈ {f1 , . . . , fn }.
The expression case t of {qi ⇒ ti }mi=1 is a case analysis on the finite enumeration type; it first evaluates t, and evaluates ti if the value is qi . The expression
t1  t2 evaluates t1 or t2 in a non-deterministic manner. As for source programs,
we require that abstract programs are simply-typed. The set of types is given
by: τ ::= d | τ1 → τ2 . Here, d is the finite enumeration type, consisting of values

q1 , . . . , qm . We show only the typing rules for q and case-expressions; the othertyping rules for expressions are essentially the same as those for source programs.
Θ `t:dΘ ` ti : τΘ `q:dΘ ` case t of {qi ⇒ ti }mi=1 : τWe write ` D : Θ if: (i) D = {fi xi,1 · · · xi,ki = ti }ni=1 ; (ii) dom(Θ) = {f1 , . . . , fn };(iii) Θ(fi ) = τi,1 → · · · → τi,ki → d and Θ, xi,1 : τi,1 , . . . , xi,ki : τi,ki ` ti : d forevery i ∈ {1, . . . , n}; and (iv) Θ(main) = d → d
We define the call-by-value, small-step reduction relation below. The sets ofevaluation contexts and values, ranged over by E and v, are defined by:
E ::= [ ] | E v | t E | case E of {qi ⇒ ti }mi=1

v ::= f v1 · · · vn (n < arity(f )) | q

The relation t1 −→D t2 is defined by: (i) E[f v1 · · · vn ] −→D E[[v1 · · · vn /x1 · · · xn ]t]
if f x1 · · · xn = t ∈ D; (ii) E[case qk of {qi ⇒ ti }mi=1 ] −→D E[tk ]; (iii) E[fail] −→D
fail; and (iv) E[t1  t2 ] −→D E[ti ] for i ∈ {1, 2}.
Definition 5 (safety problem). Let D be an abstracted program and FI and
FO be finite subsets of {q1 , . . . , qm }. We write |= (D, FI , FO ) if, for every q ∈ FI ,(i) main q −→6 ∗D fail; and (ii) main q −→∗D q 0 implies q 0 ∈ FO . The safety problem(D, FI , FO ) is the problem of deciding whether |= (D, FI , FO ) holds.
The safety problem above is decidable by a reduction to higher-order model
checking [9]. Furthermore, if |= (D, FI , FO ) does not hold, we can obtain an error
reduction sequence main q −→∗D fail or main q −→∗D q 0 6∈ FO by using a higherorder model checker [3, 8]. The knowledge of higher-order model checking andthe reduction method is not required for understanding the rest of this paper;an interested reader may wish to consult [9].
4.2

Abstraction Method

We now formalize the automata-based abstraction. In order to allow a different automaton to be used for abstracting each expression of tree type, we use
abstraction types, which specify how each expression should be abstracted.
The set of abstraction types is defined by: σ ::= oM | σ1 → σ2 . Here, M is a
(total, deterministic) automaton. Intuitively, oM describes trees that should be
abstracted by using the automaton M. The type σ1 → σ2 describes functions
whose argument should be abstracted according to σ1 , and return value shouldbe abstracted according to σ2 . For example, consider the automata M1 and M2
in Example 3. The type oM1 → oM2 describes a function whose input tree shouldbe abstracted using the automaton M1 , and output tree should be abstractedusing the automaton M2 . Using this type, the identity function λx.x would be
abstracted to λx. case x of q1 ⇒ (q2  q3 ); the argument is abstracted to q1 , andsince there is no information about whether the original value of x is even or
not, the function returns q2 (which is an abstraction of trees of the form s2n Z)
or q3 (which is an abstraction of trees of the form s2n+1 Z) non-deterministically.
If the abstraction type was oM2 → oM2 , then λx.x would be abstracted to λx.x.

The abstraction is formalized as a type-based program transformation relation Γ ` e : σ ; t, where Γ , called an abstraction type environment, is a
map from a finite set of variables to the set of abstraction types. Intuitively,Γ ` e : σ ; t means that assuming that each variable x has been abstracted
according to Γ (x), the expression e should be abstracted to t according to theabstraction type σ. How to obtain an appropriate abstraction type environment
is discussed in [13] The transformation relation is defined by the following rules.
Γ, x : σ ` x : σ ; xΓ ` a : oM → · · · → oM → oM ; fa,M
{z
}
|
Σ(a)

Γ ` e : oM ; tΓ, yei : og
M ` ei : σ ; ti (for each i ∈ {1, . . . , n})q /ye` ]t` }(C` ,eq,q)∈∆M }q∈QMΓ ` case e of {Ci yei ⇒ ei }ni=1 : σ ; case t of {q ⇒  {[eΓ ` e1 : σ1 → σ2 ; t 1
Γ ` e2 : σ1 ; t 2
Γ ` fail : σ ; fail
Γ ` e1 e2 : σ2 ; t1 t2Here,  {t1 , . . . , tn } is an abbreviation of t1  (t2  · · ·  (tn−1  tn )). In therule for case-expressions, yei : og
M abbreviates yi,1 : oM , . . . , yi,k : oM ; note thatthe type of yi,k is the same as that of e.)
A variable is abstracted to itself. A tree constructor is transformed to afunction fa,M defined below. A case expression is transformed to a case expression on the states of M. If the value of t matches q, then the value Tof the original expression e is accepted by M from state q. So, T must be of
the form a T1 · · · Tk such that (a, q1 · · · qk , q) ∈ ∆M with Ti ∈ L(M, qi ). Thus,
the body of the clause for q is a non-deterministic branch on such cases. For
example, consider the expression: case x of {Z ⇒ e1 , S y ⇒ e2 }, with the abstraction type x : oM2 (where M2 is that of Example 3). It is transformed to:case x of {q2 ⇒ (t1  [q3 /y]t2 ), q3 ⇒ [q2 /y]t2 }, where x : oM2 ` e1 : σ ; t1
and x : oM2 , y : oM2 ` e2 : σ ; t2 . The rule for applications transforms e1 and e2
in a compositional manner, but it ensures that the argument abstraction typeof e1 is equal to the abstraction type of e2 , so that the abstraction is consistent.
A program is transformed by the following rule.
P = {fi x
ei = ei }ni=1
D = {fi x
ei = ti }ni=1 ∪ D0n
Γ = {fi : σ
ei → oMi }i=1
Γ, xei : σei ` ei : oMi ; ti (for each i)D0 = {fC,M x1 · · · xΣ(C) = tC,M }C∈dom(Σ),M∈Automata(Γ )`P:Γ ;D(A-Prog)

Here, Automata(Γ ) is the set of automata occurring in Γ , and tC,M is:case (x1 , . . . , xΣ(C) ) of {(q1 , . . . , qΣ(C) ) ⇒ q}(C,q1 ···qΣ(C) ,q)∈∆ .
We have used a case expression on tuples for clarity; it can be easily flattened
to case expressions on each of x1 , . . . , xΣ(C) . In the rule A-Prog, σe → oM andxe:σe abbreviate σ1 → · · · → σk → oM and x1 : σ1 , . . . , xk : σk respectively.
The soundness of the abstraction is stated as follows; see [13] for a proof.

1: function verify(P, MI , MO )2:
Γ0 := infer abst tenv(P, MI , MO ); Split := 1; CnstSet := ∅; Γ := Γ0 ;
3:
loop
4:
let (D, FI , FO ) = abstract((P, MI , MO ), Γ )5:case check reachability(D, FI , FO ) of6:
| Yes → return Yes;
7:
| No(ep) →8:
let Cnst =gen cnst(ep, (P, MI , MO ))9:case solve cnst(Cnst) of
10:| Satisfiable(θ) → return No;
11:| Unsatisfiable →12:
CnstSet := CnstSet ∪ {Cnst};
13:
loop
14:
let cond =gensmt(CnstSet, Γ0 , Split)
15:
case smt solver(cond ) of
16:
| Satisfiable(sol ) → Γ := refine(Γ0 , Split, sol ); break;17:| Unsatisfiable → Split := Split + 1;}}

Fig. 2. Pseudo code of our method

Theorem 1 (soundness). Let (P, MI , MO ) be a verification problem. If `P : Γ ; D and Γ (main) = oM0I → oM0O with L(M0I , FI ) = L(MI ) andL(M0O , FO ) = L(MO ), then |= (D, FI , FO ) implies |= (P, MI , MO ).
Example 4. Consider the verification problem (P1 , M1 , M2 ) where P1 is definedin Example 2 and the automata M1 and M2 are given in Example 3. Let Γ1 be:{main : oM1 → oM2 , add : oM1 → oM2 → oM2 ,twice : (oM2 → oM2 ) → oM2 → oM2 }.
Then, ` P1 : Γ1 ; D1 , where D1 consists of:main x = twice (add x) q2
fS,M2 x = case x of q2 ⇒ q3 | q3 ⇒ q2
twice f x = f (f x)
add x y = case x of q1 ⇒ y  (add q1 (fS,M2 y)).
The verification problem has been reduced to the safety problem (D1 , {q1 }, {q2 }).
(|= (D1 , {q1 }, {q2 }) does not hold, however, as shown in Section 5.1; we need torefine the abstraction using the method described in Section 5.2.)tu

5Abstraction Refinement

This section discusses how to refine the automata used for abstraction when they
are not precise enough. The pseudo code of our verification method is shown in
Figure 2. Our method first infers the initial abstraction type environment, andperforms some initialization (line 2). The verification problem is reduced to asafety problem as explained in Section 4.2 (line 4). The safety problem is solved
by an existing higher-order model checker (line 5). If the answer to the problem is“no” (line 7), we inspect whether the abstract error path returned by the model
checker is feasible, i.e., the source program has a corresponding error path (lines
8–9). If the error path is feasible, the answer to the verification problem is “no”
(line 10). Otherwise, our method refines the abstraction by splitting each stateof the automaton for abstraction so that the spurious error path is eliminatedfrom the future abstraction (lines 12–17).
We explain below the feasibility checking (lines 8–9) and the abstraction
refinement (lines 12–17) in Sections 5.1 and 5.2 respectively. The inference of theinitial abstraction type environment (line 2) is explained in the full version [13].
5.1

Feasibility Check

If the answer to a safety problem is “no”, a higher-order model checker [3, 8]
outputs an error path of the abstract program. To check whether the source
program has a corresponding error execution path, we evaluate the source program symbolically along the error path, and generate constraints on variables(line 8). We then check the satisfiability of constraints (line 9).
For example, recall the safety problem (D1 , {q1 }, {q2 }) in Example 4. The
answer to this safety problem is “no”, and one of the error paths output by amodel checker is as follows.
main q1 −→D1 twice (add q1 ) q2 −→D1 add q1 (add q1 q2 )−→∗D1 add q1 (q2  (add q1 (fS,M2 q2 ))) −→D1 add q1 q2−→∗D1 q2  (add q1 (fS,M2 q2 )) −→D1 add q1 (fS,M2 q2 )−→∗D1 add q1 q3 −→∗D1 q3  (add q1 (fS,M2 q3 )) −→D1 q3
We first prepare a concise version of the error path (of the abstract program),
which is just a sequence TR of the transition rules used for abstracting thevalues inspected by each case expression. Here, we ignore the case-expressions
in the definition of fC,M , which have no corresponding case-expressions in thesource program. For the example above, TR = (Z, , q1 )(S, q1 , q1 )(Z, , q1 ). The ith element (i ∈ {1, 2, 3}) corresponds to the evaluation of the i-th case expression
evaluated in the error path above. For example, the first element corresponds tothe first case expression; since the expression being evaluated to q1 means thatthe corresponding value of the source program has been considered Z, and it was
abstracted to q1 by using the transition rule (Z, , q1 ).
Given a concise error sequence TR, we replace TR with a corresponding
concise transition sequence TR 0 for the initial abstraction, which is obtainedby replacing each transition rule (C, qe, q) with the corresponding transition rule(C, qe0 , q 0 ) of the automata occurring in the initial abstraction type environment
Γ0 . This is always possible by the construction of the refinement procedure described in Section 5.2; each state of an automaton in the current abstraction
type environment is of the form q (i) , and we just need to replace q (i) with q.
The symbolic evaluation of the original program is formalized as the relation (e, Cnst, TR) −→P (e0 , Cnst 0 , TR 0 ), where e is an expression of the original

program, Cnst is the set of constraints being accumulated, and TR is a concise
error sequence. The relation is defined by the following rules:
f x1 · · · x n = e ∈ P(E[f v1 · · · vn ], Cnst, TR) −→P (E[[v1 · · · vn /x1 · · · xn ]e], Cnst, TR)
TR = (Ck , qe, q) · TR 0
Cnst 0 = {(v = Ck xe), v : q, (ex : qe)} ∪ Cnst (ex fresh)0m(E[case v of {Ci yei ⇒ ek }i=1 ], Cnst, TR) −→P (E[[ex/yek ]ek ], Cnst , TR 0 )The first rule is for a function call, which is a deterministic evaluation that
does not require information about the error path. The second rule is for caseexpressions, where the first element of TR is looked up (and consumed) to decide
which branch should be taken. The premise TR = (Ck , qe, q) · TR 0 means that v
has been abstracted to q using the transition rule (Ck , qe, q). So, the constraints
v = Ck xe, v : q, and x
e : qe are added. Here, v is a tree expression consisting ofvariables and tree constructors; the latter constraint x
e : qe is an abbreviation of
x1 : q1 , . . . , xk : qk , which means that the value of xi should belong to L(M, qi ).
(Here, the states of automata in Automata(Γ ) are disjoint from each other;so M is uniquely identified by qi .) By applying the rules above, we obtain asymbolic execution sequence: (main x, ∅, TR 0 ) −→∗P (e, Cnst, ). We let Cnst
be the output of gen const on line 8 of Figure 2. By the rules, it should beclear that if we instantiate each variable in the symbolic evaluation sequence sothat Cnst is satisfied, then we get an actual error path of the source program.
Therefore, Cnst is satisfiable if and only if the source program has an error pathcorresponding to the abstract error path TR 0 . The satisfiability of Cnst can beeasily checked by first solving equality constraints using a standard unification
algorithm, and then checking the remaining condition v:q based on the transition
rules of the automaton.
Example 5. Recall the verification problem (D1 , {q1 }, {q2 }) and the (concise)abstract error path TR = (Z, , q1 )(S, q1 , q1 )(Z, , q1 ) considered above. We havethe following symbolic execution sequence.
(main x1 , ∅, (Z, , q1 )(S, q1 , q1 )(Z, , q1 ))−→∗ (add x1 (case x1 of Z ⇒ Z | S x0 ⇒ add x0 (S Z)), ∅, (Z, , q1 )(S, q1 , q1 )(Z, , q1 ))−→ (add x1 Z, {x1 : q1 , x1 = Z}, (S, q1 , q1 )(Z, , q1 ))−→ (case x1 of Z ⇒ Z | S x0 ⇒ add x0 (S Z)), {x1 : q1 , x1 = Z}, (S, q1 , q1 )(Z, , q1 ))−→ (add x2 (S Z), {x1 : q1 , x1 = Z, x1 = S x2 , x2 : q1 }, (Z, , q1 ))−→ (case x2 of Z ⇒ S Z | S x0 ⇒ add x0 (S (S Z)),{x1 : q1 , x1 = Z, x1 = S x2 , x2 : q1 }, (Z, , q1 ))−→ (S Z, {x1 : q1 , x1 = Z, x1 = S x2 , x2 : q1 , x2 = Z}, )We therefore get constraints {x1 : q1 , x1 = Z, x1 = S x2 , x2 : q1 , x2 = Z}. Because
the constraints are unsatisfiable (there are conflicting equalities x1 = Z andx1 = S x2 ), the error path is infeasible. Note that the infeasible error path has
been obtained because the variable x1 has been copied as add x1 (add x1 Z)
and instantiated differently (the first occurrence as S Z and the second as Z) due
to the imprecise abstraction, which abstracts both Z and S Z to the same state
q1 . The procedure described in the next subsection refines the abstraction by
splitting the state q1 in order to avoid this confusion between Z and S Z.
5.2

Abstraction Refinement

As mentioned above, when the error path of the abstracted program is infeasible, our method refines the abstraction by splitting each automaton state q
to q (1) , . . . , q (n) , where n, called the split number, is kept in variable Split in
Figure 2. It is set to 1 initially (line 2), and gradually increased.
We refine each automaton M ∈ Automata(Γ0 ) to M0 , so that: (i) ∀q ∈QM . L(M, q) = L(M0 , {q (1) , . . . , q (n) }); and (ii) the same error path (TR 0 in
Section 5.1) never occurs again.
To guarantee the first condition, it suffices to guarantee that for each rule(C, q1 · · · qk , q) ∈ ∆M ,
(i )

(i )

∀i1 , . . . , ik ∈ {1, . . . , n}.∃i ∈ {1, . . . , n}.(C, q1 1 · · · qk k , q (i) ) ∈ ∆M0
holds. Thus, M0 is determined by a function g(C,q1 ···qk ,q) ∈ {1, . . . , Split}k →{1, . . . , Split} for each (C, q1 · · · qk , q) ∈ ∆M . We prepare an uninterpreted function symbol g(C,q1 ···qk ,q) for representing the unknown function, and generate theconstraints on g(C,q1 ···qk ,q) ’s so that the second condition is guaranteed.
To guarantee the second condition, for each constraint Cnst in CnstSet(which accumulates the set of constraints generated from spurious error paths
found so far), we generate the following SMT formula FCnst .
W∀x1 , . . . , x` ∈ {1, . . . , Split}. v1 =v2 ∈Cnst (state(v1 ) 6= state(v2 )).
Here, state(v) is defined by: (i) state(x) = x; and (ii) state(C v1 · · · vk ) =g(C,q1 ··· qk ,q) (state(v1 ), . . . , state(vk )) if ∆0 (v1 ) = q1 , . . . , ∆0 (vk ) = qk , and∆0 (C v1 , . . . vk ) = q, where ∆0 (v) is defined by:(q(if v = x ∧ (x : q) ∈ Cnst)0∆ (v) =∆(C, ∆0 (v1 ) · · · ∆0 (vΣ(C) )) (if v = C v1 · · · vΣ(C) )S
with ∆ = {∆M | M ∈ Automata(Γ0 )} for the initial abstraction type environment
Γ0 . Then, gensmt outputs the conjunction of the above formulaV
Cnst∈CnstSet FCnst . If it is satisfiable, then we obtain a refined abstraction typeenvironment Γ . Otherwise, we increase Split until the SMT constraint becomes
satisfiable.
Example 6. Recall the verification problem in Example 5 and suppose Split = 2.
The generated SMT formula is:∀x1 , x2 ∈ {1, 2}.x1 6= g(Z,,q1 ) () ∨ x1 6= g(S,q1 ,q1 ) (x2 ) ∨ x2 6= g(Z,,q1 ) ()

One of the solutions is g(Z,,q1 ) = 1, g(S,q1 ,q1 ) (1) = 2, g(S,q1 ,q1 ) (2) = 1. The transi(1)

(1)

(2)

(2)

(1)

tion function of the refined automaton is: {(Z, , q1 ), (S, q1 , q1 ), (S, q1 , q1 )}.
Using this automaton, the verification succeeds.
The following theorem ensures that if there is an appropriate abstraction typeenvironment with which the verification succeeds, then the algorithm eventuallyfind such an abstraction type environment. See [13] for a proof.
Theorem 2 (relative completeness). Let (P, MI , MO ) be a verification problem. Suppose there exists Γ such that ` P : Γ ; D, |= (D, FI , FO ), andΓ (main) = oM0I → oM0O with L(MI ) = L(M0I , FI ) and L(MO ) = L(M0O , FO ).
Then the algorithm eventually terminates and outputs “Yes”.
We say that check reachability in Figure 2 is fair if every concise error
path is eventually generated; it is guaranteed if check reachability always
returns a shortest concise error path, for example. We can also guarantee:
Theorem 3 (completeness of refutation). Let (P, MI , MO ) be a verification problem such that 6|= (P, MI , MO ). If check reachability is fair, thenthe algorithm eventually terminates and outputs “No”.

6

Implementation and Experiments

We have implemented a verification tool based on our method, and evaluatedit through experiments. The experiments were conducted on a machine withIntel(R) Xeon(R) CPU E5620 2.40GHz and 3.73GB memory. We used HorSat[3] as the higher-order model checker (except for the program “homrep-rev” forwhich we used [8] due to a problem of HorSat) and Z3 [5] as the SMT solver.
Table 1 shows the result of the experiments. The column “S” represents
the size of the programs. The size of a program is the number of occurrences of
constants and variables on the right side of the rules in the program. The column“O” represents the order of the programs. The order of a program is the largest
order of the types of functions. Here, the order order (κ) of the type κ is definedby: order (o) = 0, order (κ1 → κ2 ) = max{order (κ1 ) + 1, order (κ2 )}. The column“R” represents the number of refinements in the verification. The column “T”
shows the running time (measured in seconds). We ran each program 3 times
and show the average running time. “TO” in the column “T” means a time-out,
where we set the time-out to 1000 seconds. For comparison, we have also run
the verification tools for HMTT [12] and EHMTT [19] and show their runningtimes in the columns “TH ” and “TE ” respectively. The “N/A” means that thetool is inapplicable; that is the case for the HMTT verification tool, when trees
are repeatedly constructed and deconstructed inside the program. The EHMTT
verification tool is inapplicable when there is no appropriate annotation; see
the discussion below. We have also tried to compare our tool with the PMRS
verification tool [16], but unfortunately we could not obtain its source code.
The benchmark programs consist of three categories (separated by lines in thetable). The first category (the programs from “reverse” to “mincaml-k”) has been

taken from the benchmark set for the EHMTT verification tool [19]. The original
programs contain annotations required for EHMTT, and they have been removed
for the experiments on our new tool. The second category has been taken fromthe benchmark set for the PMRS verification tool [16], available at http://mjolnir.cs.ox.ac.uk/cgi-bin/horsc/recheck-horsc/input. The third category contains a new benchmark set. The program “double” is the verification
problem given in Example 3. The program “isort2” sorts a given list consistingof “A” and “B” by the insertion sort algorithm. The specification asserts thatthe result is a sorted list. The program “issorted” sorts a given list consisting of“A” and “B” by the insertion sort, and then (inside the program) checks thatthe result is a sorted list; if not, the program fails. The specification is that the
program does not fail. The program “mergesort2” is the same as “insertionsort”
except that the merge sort algorithm is used. The program “mapswsort” sorts
a given list and maps a function that swaps “A” and “B” on the list. In the
programs above, lists are encoded as trees constructed from cons, nil, A, and
B. The program “remove0” takes a list of integers (in the unary representation)and removes 0 from the list.
Our tool could verify the benchmark programs, except “xmarkq1” and “gapid”.
For the program “xmarkq1”, the tool failed to construct the initial abstraction.
This is because the automata given as the specification of the program is large,
and the current tool naively applies a product construction to make the automaton used for abstraction. For the program “gapid”, the abstraction refinement
loop did not terminate within the given time limit. This is because the automaton
required for abstracting intermediate trees is quite different from the automata
given as the input/output specification.
As for the comparison with the HMTT/EHMTT verification tools, the HMTT
tool is applicable to only a few of the benchmark programs. That is because
HMTT [12] classifies trees into input trees and output trees, and pattern matching can be applied only to input trees, and tree constructors can be applied only
to output trees. Most of the programs in the benchmark set repeatedly constructand deconstruct trees.
The EHMTT tool works for the first benchmark set, but it relies on user
annotations. Like HMTT, EHMTT also distinguishes between input and output
trees, but allows an explicit coercion of output trees to input trees. Each coercion
must be annotated with an invariant on the shape of trees that are coerced, andthat invariant is used for abstraction. Thus, since an appropriate abstraction
is given by hand, EHMTT is faster than our tool when it is applicable. For
the second and third categories, we have also added annotations for EHMTT,
when applicable. For many of the benchmark programs in the second and third
categories, however, there are no appropriate annotations that make the EHMTT
verification succeed. There are two main reasons for this. One reason, which issomehow specific to the current implementation, is that the EHMTT tool allows
only deterministic top-down automata as output specifications. Since the classof deterministic top-down tree automata is a strict subclass of deterministicbottom-up tree automata, some of the specifications cannot be handled by the

EHMTT tool. The other reason is more fundamental. Consider the following
function “iszero”.
iszero x t f = case x of Z ⇒ t | S y ⇒ f.
If the first argument of the function “iszero” is an output tree, the argument
requires an annotation as follows.
iszero (coerceL e) et ef
Here, coerceL e converts an output tree constructed by e to an input tree, sothat pattern matching can be applied again. The annotation L is an invariant
on the value of e; in this case, L would be typically S∗ Z (unless the value of ecan be statically determined). Given the annotation, the EHMTT converts the
body of iszero to a non-deterministic choice between t and f , ignoring the actual
value. Thus, if the property to be verified requires a case analysis on whether x
is Z or not, the EHMTT verification fails.
To summarize, compared with the HMTT/EHMTT verification tools, ournew tool works for a larger set of programs, requiring no special annotations,although it may be slower when the previous tools are applicable. For the programs such as xmarkq1 and gapid, a compromise would be to allow users toprovide abstraction types as annotations. Such annotations do not suffer fromthe problem of EHMTT annotations discussed above.

programS O R T TH TE program
S O R T
TH TE
reverse46 1 16 4.215 N/A 0.032 mkground 46 1 4 0.892 N/A 0.043
isort
29 1 0 0.103 N/A 0.022 filter-nz
31 2 1 0.472 N/A N/Amergesort 173 2 0 1.711 N/A 0.303 safe-tail100 2 9 11.48 N/A N/Ahomrep-rev 97 4 14 2.338 N/A 0.043 maphead
53 2 5 2.489 N/A N/Asplit2108 2 53 589.3 N/A 0.089 risers
78 1 3 2.006 N/A 0.079
bib2html 103 2 1 3.568 N/A 0.376 safe-init
113 2 13 22.76 N/A N/A
xmarkq1
89 2 - TO N/A 0.767 checknz
8 1 0 0.018 0.011 0.009
xmarkq2 157 1 0 100.8 N/A 1.531 checkpairs 35 1 0 0.082 N/A N/A
gapid
393 3 14 TO N/A 0.148 double
12 1 0 0.041 0.040 N/A
jwig-cal96 1 0 143.5 N/A 0.570 isort2
40 1 1 1.058 N/A N/Ajwig-guess 99 2 6 65.8 N/A 1.411 issorted
127 1 6 12.45 N/A N/A
mincaml-k 683 2 0 532.3 N/A 1.830 mapswsort 61 2 20 22.63 N/A N/A
last
20 1 1 0.129 N/A 0.027 mergesort2 96 1 0 3.178 N/A N/Asafe-head67 2 1 0.888 N/A N/A remove0
32 1 1 0.409 0.015 0.012
Table 1. Experimental results

7

Related WorkAs mentioned in Section 1, several approaches have been proposed for automated verification of functional programs based on higher-order model checking.
Kobayashi et al. [11] proposed predicate abstraction and CEGAR (counterexampleguided abstraction refinement) for higher-order model checking, but they used
only predicates on integers for abstraction. They later supported some algebraic
data structures by encoding them into functions on integers. That encoding approach, however, complicates both programs and specifications. For example,
since a list is encoded into a pair consisting of its length and a function thatmaps an index to the corresponding element, the property of a list: “1 occurs in
the list” would be converted to a refinement type specification:n : int × {f : int → int | ∃x.(0 ≤ x < n ∧ f (x) = 1)},
which would be simply represented by ∗ 1 ∗ with a regular language (or automaton) specification. The above specification involves function variables andexistential quantifiers, which cannot be handled even by the recent extension of
MoCHi [1]. Even if the encoding works, the resulting program and specification
tends to become too complex and large, making automated verification difficult;in fact, the current implementation of MoCHi does not work for the benchmark
programs in Section 6. That said, a limitation of our new approach is that wecannot verify some co-relation between arguments and return values, like “Function f takes a list of length n, and returns a list of length 2 × n.” This is because
we use automata for abstracting information about each tree, which loses therelationship between multiple trees. A possible remedy to this problem would be
to use tree automatic relations [2] for abstraction. Another approach would be
to integrate our new approach with that of MoCHi.
We have already discussed HMTT [12] and EHMTT [19] in Section 6. Although HMTT also abstracts trees by using an automaton, the automaton used
for the abstraction is fixed to the one specified as the input automaton. EHMTT
decompose the verification problem to multiple HMTT verification problems, byusing annotations. Again, the abstraction relies on the automata given as specifications or annotations. There was no abstraction refinement loop mechanism in
the above work on HMTT/EHMTT verification. We have recently extended the
HMTT verification with abstraction refinement loops [14], but it was restricted
to HMTT (where there is a distinction between input/output trees), and therelative completeness (cf. Theorem 2) was not guaranteed. In short, our new
method requires no annotations unlike EHMTT verification, and works (at leastin theory) for a strictly larger set of verification problems than our previous workon HMTT/EHMTT verification.
Ong and Ramsay [16] introduced a verification method fortree-processing programs called PMRS. Their method abstracts trees based on
finite patterns, so it cannot deal with general regular properties like “a tree contains an even number of S”. For example, for the program P1 in Example 2:
they abstract the argument x of add based on the information about whether

x matches Z or S x0 . If the verification fails, they expand patterns by unfolding
functions; in the case of the above example, the new set of patterns would be{Z, S Z, S (S x)}. Thus, their abstraction never captures properties like “x is aneven number” (i.e., x is of the form S2n Z). For the benchmark programs usedin our experiments, PMRS works for the second category (because it has beentaken from the benchmark of the PMRS tool), but it would not work for mostof the benchmarks in the first and third categories.
Automata-based abstraction has also been recently used for µHORS model
checking [10]. The µHORS model checking is an extension of higher-order model
checking, where HORS has been extended with recursive types. They abstract
the whole program configuration (which can be represented as applicative terms)
by using a tree automaton, and gradually refines the abstraction using a similar technique utilizing an SMT solver. Since µHORS is Turing complete, theirapproach can in theory be applied to the verification problems considered in
the present paper, but our approach would scale much better for tree-processing
programs. They abstract both control and data structures using automata in amonolithic way, whereas we abstract only tree data using automata, and precisely analyze control structures thanks to the decidability of higher-order model
checking.
Besides approaches based on higher-order model checking, there have been a
few other approaches to (semi-)automated verification of higher-order functional
programs that support algebraic data types. Liquid types [17, 7, 20] is a notableapproach based on refinement types, but it requires a user’s hints on the predicates used in refinement types. Genet [6] applies a tree automata completion
technique for term rewriting systems to static analysis of functional programs.
His approach uses tree automata for modeling the whole program state (likein the µHORS model checking mentioned above), while our approach uses tree
automata only for abstracting tree data. His method does not guarantee therelative completeness in the sense of ours.

8

Conclusion

In this paper, we have introduced a new method for fully automated verification of tree-processing, higher-order functional programs. We have introduced
automata-based abstraction, and combined it with higher-order model checking.
The automata-based abstraction is formalized as a type-based program transformation, and the abstraction is gradually refined based on counterexamples.
Compared with the previous methods based on higher-order model checking, the
new method is more automated (requires no annotations), and can deal with alarger class of programs. Future work includes improvement of the scalability ofthe verification method, and an integration of the proposed technique with thepredicate abstraction approach of MoCHi [11, 18, 1].
Acknowledgments We thank anonymous reviewers for useful comments. This
work was partially supported by JSPS Kakenhi 15H05706, 23220001, and 25730035.

References
1. Asada, K., Sato, R., Kobayashi, N.: Verifying relational properties of functional
programs by first-order refinement. In: Proceedings of PEPM 2015. pp. 61–72(2015)
2. Blumensath, A., Grädel, E.: Automatic structures. In: Proceedings of LICS 2000.
pp. 51–62 (2000)
3. Broadbent, C.H., Kobayashi, N.: Saturation-based model checking of higher-orderrecursion schemes. In: Proceedings of CSL 2013. LIPIcs, vol. 23, pp. 129–148 (2013)
4. Comon, H., et al.: Tree automata techniques and applications. Available on: http://www.grappa.univ-lille3.fr/tata (2007)
5. De Moura, L., Bjørner, N.: Z3: An efficient SMT solver. In: Proceedings of TACAS
2008. Lecture Notes in Computer Science, vol. 4963, pp. 337–340. Springer-Verlag(2008)
6. Genet, T.: Towards static analysis of functional programs using tree automata
completion. In: Rewriting Logic and Its Applications - 10th International Workshop, WRLA 2014. Lecture Notes in Computer Science, vol. 8663, pp. 147–161.
Springer (2014)
7. Kawaguchi, M., Rondon, P., Jhala, R.: Type-based data structure verification. In:
Proceedings of PLDI ’09. pp. 304–315. ACM (2009)
8. Kobayashi, N.: Model-checking higher-order functions. In: Proceedings of PPDP2009. pp. 25–36 (2009)
9. Kobayashi, N.: Model checking higher-order programs. J. ACM 60(3), 20:1–20:62(Jun 2013)
10. Kobayashi, N., Li, X.: Automata-based abstraction refinement for µhors model
checking. In: Proceedings of LICS 2015 (2015)
11. Kobayashi, N., Sato, R., Unno, H.: Predicate abstraction and cegar for higher-ordermodel checking. In: Proceedings of PLDI 2011. pp. 222–233 (2011)
12. Kobayashi, N., Tabuchi, N., Unno, H.: Higher-order multi-parameter tree transducers and recursion schemes for program verification. In: Proceedings of POPL
2010. pp. 495–508. ACM (2010)
13. Matsumoto, Y., Kobayashi, N., Unno, H.: Automata-based abstraction for automated verification of higher-order tree-processing programs (2015), an extended
version, available from the second author’s web page
14. Matsumoto, Y., Kobayashi, N., Unno, H.: Counterexample finding and abstraction refinement for automated verification of higher-order transducers. Computer
Software 31(1), 161–178 (2015), (in Japanese)
15. Ong, C.H.L.: On model-checking trees generated by higher-order recursion
schemes. In: Proceedings of LICS 2006. pp. 81–90. IEEE Computer Society (2006)
16. Ong, C.H.L., Ramsay, S.J.: Verifying higher-order functional programs withpattern-matching algebraic data types. In: Proceedings of POPL 2011. pp. 587–
598. ACM (2011)
17. Rondon, P.M., Kawaguchi, M., Jhala, R.: Liquid types. In: PLDI ’08. pp. 159–169(2008)
18. Sato, R., Unno, H., Kobayashi, N.: Towards a scalable software model checker for
higher-order programs. In: Proceedings of PEPM 2013. pp. 53–62. ACM (2013)
19. Unno, H., Tabuchi, N., Kobayashi, N.: Verification of tree-processing programs via
higher-order model checking. In: Proceedings of APLAS 2010. Lecture Notes in
Computer Science, vol. 6461, pp. 312–327. Springer-Verlag (2010)
20. Vazou, N., Rondon, P.M., Jhala, R.: Abstract refinement types. In: ESOP ’13.
Lecture Notes in Computer Science, vol. 7792, pp. 209–228. Springer-Verlag (2013)