Automatic Termination Verification for Higher-Order
Functional Programs⋆
Takuya Kuwahara1, Tachio Terauchi2 , Hiroshi Unno3 , and Naoki Kobayashi41

University of Tokyo, kuwahara@is.s.u-tokyo.ac.jp
Nagoya University, terauchi@is.nagoya-u.ac.jp
3
University of Tsukuba, uhiro@cs.tsukuba.ac.jp
4
University of Tokyo, koba@is.s.u-tokyo.ac.jp

2

Abstract. We present an automated approach to verifying termination of higherorder functional programs. Our approach adopts the idea from the recent work on
termination verification via transition invariants (a.k.a. binary reachability analysis), and is fully automated. Our approach is able to soundly handle the subtle
aspects of higher-order programs, including partial applications, indirect calls,
and ranking functions over function closure values. In contrast to the previous
approaches to automated termination verification for functional programs, ourapproach is sound and complete, relative to the soundness and completeness of
the underlying reachability analysis and ranking function inference. We have implemented a prototype of our approach for a subset of the OCaml language, andwe have confirmed that it is able to automatically verify termination of some
non-trivial higher-order programs.

1 Introduction
Recent years have witnessed a dramatic progress in automated verification of higherorder functional programs [27, 31, 24, 11, 16, 33, 37]. The line of work takes the ideas
from the recent advances in the verification of non-functional programs, such as predicate abstraction, counterexample-guided abstraction refinement, and interpolation [1,9, 21, 10], to the verification of higher-order functional programs by way of refinement(dependent) types [36] and higher-order model checking [23, 14].
However, except for the case when the base-type data is of a finite domain [15,20], the above line of work (to the extent of software model checking techniques forhigher-order programs) has been limited to the verification of safety (i.e., reachability)
properties. In particular, it is unable to verify liveness properties, such as termination.
For automated termination verification of higher-order programs, popular methods
have been based on size-change termination [12, 29, 28] or TRS (term rewriting systems) techniques [6]. (Besides them, Xi [35] has proposed termination analysis basedon dependent types, but his technique is not fully automated in the sense that users
have to provide dependent types of recursive functions as witness of termination.) The
current methods based on those approaches are not completely satisfactory, especiallyin terms of precision. Roughly, these techniques first construct a finite graph (called a⋆This work was supported by MEXT Kakenhi 23220001, 23700026, 25280023, and 25730035.

let rec app f x () =if x>0 then app f (x-1) () else f x () in
let id () = () in
let rec g x = if x=0 then id else app g x inlet t = * in g t ()Fig. 1. A non-terminating higher-order program.

static call graph [12, 29, 28] or a termination graph [6]) that over-approximates certain
dependencies on termination, and then use techniques for first-order programs [19, 7] toshow that there is no cyclic dependency. In these two-phase approaches to termination,
information is often lost in the first phase; see Section 5 for more details.
In the present paper, we follow an approach based on transition invariants [26, 4, 5],
and extend it to deal with higher-order functional programs. The transition-invariantbased approach has emerged as a powerful technique for verifying termination of firstorder imperative programs [26, 4, 5]. The technique iteratively reduces the termination
verification problem to the problem of checking the binary reachability of programtransition relations. It then delegates the binary reachability checking to a reachability
checker by encoding the problem as a plain reachability problem via a program transformation. Advantages of this approach are that termination arguments can be flexibly
adjusted for each program by choosing an appropriate binary reachability relation, andthat precise flow information can be taken into account in the plain reachability verification phase. The latter advantage is particularly important since the termination property
often depends on safety properties. For example, consider the program:let f x = if p(x) then () else loop_forever()Then, a call of f terminates if and only if p(x) is true, and the latter condition can
be checked during the reachability verification. In the higher-order case, termination
verification would be even more complicated since the condition can be passed as aparameter of f. This shows the advantage of reducing termination verification to reachability verification, where all the relevant information (such as value-dependent control
flow and size change) is put together and precisely analyzed by taking advantage of therecent advance of reachability verification tools for higher-order programs.
The extension of the transition invariant-based technique for higher-order programs
is non-trivial. To see why, let us consider the OCaml program P0 shown in Figure 1.
(Here, * denotes a non-deterministic integer.) The program is non-terminating for any
non-deterministic choice of t such that t < 0. For example, for t = −1, the program
exhibits the following infinite reduction sequence.
g (-1) () →∗ app g (-1) () →∗ g (-1) () →∗ app g (-1) () →∗ · · ·Note here that g is passed to and indirectly called by app, and there is no direct callto g in the definition of g. Moreover, g itself does not (totally) call app but returns apartially applied closure of the form app g n. Therefore, a termination verifier mustsoundly handle indirect calls and function closures to avoid incorrectly reporting thatthe program is terminating.

For a terminating example, let us consider a variation P1 of the above program,obtained by replacing the branching condition x = 0 in g with x ≤ 0. To prove that
P1 is terminating for any non-deterministically chosen t (and any non-deterministic
choice of the integers chosen inside g), we need to know that the sequence of the thirdarguments passed to the recursive calls to app is strictly decreasing and is bounded
below by 0.
Our technique consists of: (i) a method to find an appropriate (disjunctively) wellfounded relation, including those over function closure values, that over-approximates
the binary reachability relation (the relation between two recursive function calls), (ii) a
program transformation that reduces the binary reachability problem to the plain reachability problem, and (iii) a plain reachability analysis for higher-order programs. For (iii),
we employ off-the-shelf reachability verification tools for higher-order programs [27,31, 11, 16, 33, 37]. For (i), we adopt the previous technique [33] for automatically inserting implicit integer parameters that represent information about function closures.
We can then adopt the existing techniques to find ranking functions (on integer arguments) from counterexamples [25, 3, 5]. The most subtle part is (ii): how to reduce thebinary reachability analysis to plain reachability analysis. Actually, Ledesma-Garza andRybalchenko [18] has recently tackled this problem, but (as admitted in [18], Section 8),
their solution does not work quite well in the presence of partial applications and indirect function calls. In fact, their method cannot properly deal with the programs P0 and
P1 above (cf. Section 5 of this paper for more details). By contrast, the reduction frombinary reachability to plain reachability presented in this paper is sound and complete.
Our contributions are: (i) The first sound approach to the termination verificationof higher-order functional programs that is based on the transition invariant / binary
reachability technique. The approach is also complete relative to the completeness ofthe backend reachability checker and the ranking function inference process. A notableaspect of our approach is an inference of ranking functions over closure values via theautomatic inference of implicit parameter instantiations. (ii) A prototype implementation to show the effectiveness of the proposed approach.
The rest of the paper is organized as follows. We define the target functional language of termination verification in Section 2. Section 3 formalizes our termination
verification method. Section 4 reports on a preliminary implementation and experimentresults. We compare our method with related work in Section 5 and conclude the paper
in Section 6. Appendix contains extra materials and proofs of the theorems.

2 Preliminaries
In this section, we introduce a higher-order functional language L, which is the target of
our termination verification. Figure 2 shows the syntax of L. Here, xe is an abbreviation
for a (non-empty) variable sequence x1 x2 . . . xk . The meta-variables f , x, c andop range over the sets of function symbols, variables, constants, and binary operators
respectively. We write |ex| for the length of xe. The arity of function fi , written arity(fi ),is the number of formal parameters, i.e., |xei | in the function definition fi xei = ei . We
assume that the set of constants includes (), true, false and (unbounded) integers,
and that the set of binary operators includes comparators: >, <, ≥, ≤, = and boolean

Programs P ::= {f1 xe1 = e1 , . . . , fn x
en = en }Expressions e ::= v | x | let x = e1 in e2 | e1 op e2 | e1 e2 | if e1 then e2 else e3 | ∗int
Values v ::= c | f | f ev (where |ev | < arity (f ))Fig. 2. Syntax of L

Eval. contexts E ::= [ ] | E op e | v op E | E e | v E | let x = E in e
| if E then e1 else e2
E [c1 op c2 ] →P E [[[op]](c1 , c2 )]E [let x = v in e] →P E [[v/x] e]n∈Z
E [∗int ] →P E [n]E [if true then e1 else e2 ] →P E [e1 ]

fx
e=e∈P

E [if false then e1 else e2 ] →P E [e2 ]E [f ev ] →P E [[e
v /e
x] e]

|e
x| = |ev|

Fig. 3. Operational semantics of L.

operators: ∧, ∨, ⇒. We also assume that a program has a special one-arity function
named main that does not occur in the body of a function definition.
A program is a set of top-level function definitions; note that this does not lose
generality because any functional program can be transformed to this form via λ-lifting.
In the definition of the expression, ∗int evaluates to some integer in a non-deterministicmanner. Note that the non-deterministic boolean, ∗bool , can be defined as ∗int = 0.
The set of evaluation contexts and the reduction relation are given in Figure 3. Here,[[op]] denotes the binary operation on constants denoted by op. Note that the evaluation
is call-by-value and non-deterministic (because of ∗int ). We write →∗P for the reflexive
and transitive closure of →P , and →+P for the transitive closure of →P . When it is clear
from the context, we omit the subscript P from the relations.
Example 1. The following program fib chooses an integer n non-deterministically andcomputes the n-th Fibonacci number.

fib n = if n < 2 then 1 else fib(n − 1) + fib(n − 2),main () = fib ∗int
The following is a possible reduction sequence of the program:main () →fib fib ∗int →fib fib(2) →∗fib fib(1) + fib(0)→∗fib 1 + fib(0) →∗fib 1 + 1 →∗fib 2
For readability, we often write a program in the OCaml-like syntax as shown below:
let rec fib n = if n < 2 then 1 else fib (n-1) + fib (n-2)
let main () = fib ∗int

Example 2. The following program indirect is a simplified variant of the program P1
in Section 1, obtained by removing the then branch of app and moving the decrement
operation (i.e., x − 1) to inside g.

app f x u = f x u






id u = ug x = if x ≤ 0 then id else app g (x − 1) 





main () = g ∗int ()The following is a possible reduction sequence of the program.

main () →∗ g 2 () →∗ app g 1 () →∗ g 1 ()→∗ app g 0 () →∗ g 0 () →∗ id () →∗ ()Note that, although g is applied to two arguments in the reduction above, arity(g) = 1
in our definition (because x is the only formal parameter in the definition of g).
We define termination as follows.
Definition 1. A program P is terminating, if there is no infinite reduction sequencemain () →P e1 →P e2 →P · · · .
Remark 1. The language L is untyped and therefore, a program evaluation may getstuck. We consider a reduction sequence that ends with a stuck expression as terminating. Our approach is sound and complete even for untyped languages. But, our implementation currently supports only the typed subset because it delegates the reachability
checking to a higher-order program model checker for a typed language.

3 Termination Verification via Binary Reachability
This section describes our termination verification method. We give an informal overview
of the whole process in Subsection 3.1, and discuss each step in a more detail in the later
subsections.
main ()

3.1 Overview
We use indirect from Example 2 as arunning example in this subsection. Our
termination verification method is basedon the observation that a functional program is terminating if and only if eachof its call tree,5 which expresses how thefunctions are called in an execution of
the program, is finite. Figure 4 shows acall tree for indirect. Each node expresses a fully applied function call (a5gn

app g (n − 1) ()g (n − 1) app g (n − 2) ()g (n − 2)..
.
app g 0 ()g 0 id ()Fig. 4. A call tree of program indirect.

The call tree in this paper roughly corresponds to the dynamic call graph of [29].

Input Program P

Step 1: Program
Translation(Subsection 3.3)

Candidate Df and σ⌈P ⌉σ,f,Df
Step 2: Reachability
Analysis [16, 31]

Counterexample

Step 3: Ranking
Function & Implicit
Parameter Inference(Subsection 3.4) [25, 3, 5, 33]

Safe
Rec(f ) is disjunctively well-foundedFail
P may not terminate

Fig. 5. Overview of the termination verification process.

call of the form f ve with arity(f ) = |ev |),and an edge represents that the function call represented by the target node is made fromthe function call of the source node. For example, the edge from “app g (n − 1) ()”to “g (n − 1)” means that g (n − 1) is called during evaluation of app g (n − 1) ()(i.e., app g (n − 1) () →+ E[g (n − 1)] for some evaluation context E). For every(possibly infinite) reduction sequence, the corresponding call tree is finitely branching.
Therefore, by König’s lemma, to show that every call tree of the program is finite andtherefore the program is terminating, it is sufficient to show that no call tree has an infinite path from the root. The latter is equivalent to showing that for every function f ,there is no infinite path f e
v1 ⊲ f ve2 ⊲ f ve3 ⊲ · · · where f ev ⊲ gwe means that f ve is anancestor of g w
e in the call tree. In the running example, the only non-trivial sequenceis app g n1 () ⊲ app g n2 () ⊲ app g n3 () ⊲ · · · and this sequence must be finite sinceni is decreasing and bounded below by 0. Thus, we may conclude that indirect isterminating. We refer to Subsection 3.2 for the formal exposition of the above argument.
By the above argument, to show that the program terminates, it suffices to show
that, for every function f , the relation Rec(f ) = {(ev, ev ′ ) | f ve ⊲ f ve′ } is well-founded,
6
or disjunctively well-founded [26] because RecP (f ) is transitive. Thus, as mentioned
in Section 1, our termination verification method proceeds as follows.
(i) For each function f , guess a disjunctively well-founded relation Df that overapproximates Rec(f ), and reduce the termination verification problem to the socalled the binary reachability analysis problem of showing Rec(f ) ⊆ Df .
6

A binary relation is disjunctively well-founded if it is a finite union of well-founded sets [26].

(ii) Use a program transformation to reduce the binary reachability problem to a plain
reachability problem; and(iii) Solve the plain reachability problem by using an off-the-shelf software model
checker.
We express the disjunctively well-founded relation Df by using a set of ranking functions, and gradually refine the set by using the technique of counterexample-guided
abstraction refinement [25, 3, 5, 33].
Figure 5 shows the overall flow of the process. We start with an empty set of ranking
functions (i.e., with Df = ∅), and apply a program transformation to reduce the binary
reachability analysis problem of deciding Rec(f ) ⊆ Df to the plain reachability analysis problem of deciding if an assertion failure is reachable in the translated program⌈P ⌉σ,f,Df (Step 1 in Figure 5). Here, σ is a candidate implicit parameter instantiationand is used for ranking functions over higher-order values (i.e., function closures). For
the purpose of the exposition, we focus on the case where the ranking functions are only
over the first-order values in Subsections 3.2 and 3.3, and defer implicit parameters andranking functions over higher-order values to Subsection 3.4. For simplicity, we write⌈P ⌉f,Df for ⌈P ⌉σ,f,Df when implicit parameters are irrelevant to the discussion.
Informally, the idea of the program transformation is to pass around the argumentpf
v of an ancestor call as an extra argument, and assert in the body of f that pf
v and thecurrent argument e
v are related by Df . For the running example, the definition of app
would be transformed as follows.
app s1 f s2 x s3 u = assert((s3,(f,x,u))∈ Dapp ); ...

Here, s1, s2, and s3 are the extra arguments that carry the arguments of ancestor calls
to app. Because a function body does not evaluate until the function is fully applied,
only s3 is relevant and is checked with the current arguments (f, x, u) for the candidate
disjunctively well-founded relation Dapp . We use non-determinism to ensure that theextra parameter can be bound to the argument of an arbitrary ancestor call, so that thetransformed program is assertion safe if and only if Rec(f )⊆Df . Because a function
can be called indirectly in a higher-order program, we pass extra arguments at all callsites, including indirect calls, to account for all possible ancestor relations. Therefore,
for the running example, we also transform the functions g and id to take extra parameters (but only track and check the arguments of app). This makes our approachsound and complete even in the presence of higher-order functions.7 In this manner,
the binary reachability problem is reduced to a plain reachability problem. We refer to
Subsection 3.3 for a more formal exposition.
We proceed to the plain reachability analysis (Step 2 in Figure 5), to check if the inserted assertion may fail. If the assertion cannot fail, then we conclude that Rec(f )⊆Df
holds (and if that is the case for every function f in the program, we conclude that the
program is terminating). Even if the program is terminating, however, an assertion failure may occur, because of a wrongly guessed Df . For our running example, in the initial
7

This is a crucial difference with the previous approaches to automated termination verification
for higher-order programs [30, 28, 29, 6, 12] that handle higher-order functions by approximating the call graph up front (e.g., via a control flow analysis), which can lose precision when
the calls depend on non-trivial safety conditions.

iteration, we set Dapp = ∅, and when the transformed program is given to a reachability
verifier (e.g., MoCHi [16]), the verifier would return a concrete counterexample to theassertion safety. Suppose the following counterexample is returned.
main () →∗ app s1 g s2 0 (g, 1, ()) () →∗ failwhich corresponds to the following reduction sequence in the original program:main () →∗ g 2 () →∗ app g 1 () →∗ app g 0 ()We analyze the counterexample, and infer a new ranking function to refine Df(Step 3 in Figure 5). For the running example, we look for a ranking function r suchthat r(g, 1, ()) > r(g, 0, ()) ≥ 0 and update Dapp to Dapp ∪ {((pf, px, pu), (f, x, u)) |r(pf, px, pu) > r(f, x, u) ≥ 0}. To find a ranking function, we adopt the existing
techniques for inferring ranking functions from counterexamples of first-order programs [25, 5].8 If no ranking function can be found, then we report that the program
may not be terminating. This may happen either because the program is indeed nonterminating, or the method used for the ranking function synthesis is incomplete. We
refer to Subsection 3.4 for a more formal exposition on this step.
Upon refining Df , we go back to Step 1 and repeat the process. If the program is
terminating, and if the underlying reachability analysis tool and the ranking function
synthesis were complete, the loop eventually terminates and we conclude that the program is terminating.
3.2 Termination and Binary Reachability
We discuss how termination verification is reduced to binary reachability analysis (toshow Rec(f ) ⊆ Df ) more formally. First, we define the relations ⊲ and Rec(f ).
Definition 2. The call relation ⊲P is the binary relation defined by:⊲P := {(f ve, g w)
e | (main () →∗P E1 [f ve]) ∧ (f ve →+e
P E2 [g w])∧arity(f ) = |ev | ∧ arity(g) = |w|}e

We often use the infix notation f ev ⊲P g w
e for (f ev , g w)e ∈ ⊲P .

Definition 3. RecP (f ), the recursion relation of f in P , is the binary relation definedby:
RecP (f ) := (hve1 i, hve2 i) |f e
v1 ⊲P f ve2

When it is clear from contexts, we omit the subscript P . Note that the relations ⊲P and
RecP (f ) are transitive.
Example 3. Recall program fib in Example 1. Rec(fib) is:+({(n, n − 1)|n > 1} ∪ {(n, n − 2) | n > 2}) = {(m, n) | m > n ≥ 0}
8

To infer a ranking relation over function closure values, we use implicit parameters and infer sufficient instantiations for them to represent the closures. This is done by adopting thecounterexample-guided technique from the previous work [33] (cf. Subsection 3.4).

As shown in the example below, Rec(f ) may be non-empty even if f is not recursively defined, and Rec(f ) may be empty even if f is recursively defined.
Example 4. Recall the program in Example 2. The recursion relations are:Rec(app) = {(hg, m, ()i, hg, n, ()i) | m > n ≥ 0}
Rec(id) = Rec(g) = ∅Note that g is defined recursively but does not cause a recursive call to g. Therefore,
the relation Rec(g) is empty. On the other hand, app is not recursively defined but
Rec(app) 6= ∅. This shows that we must check the disjunctive well-foundedness ofRec(f ) for each function f , regardless of whether f is recursively defined or not.
Next, we show the termination verification problem can be reduced soundly andcompletely to the problem of showing that Rec(f ) is disjunctively well-founded forevery f .
We state the soundness and the completeness of the reduction.
Theorem 1 (Soundness). A program P is terminating if RecP (f ) is disjunctively wellfounded for every f defined in P .
Theorem 2 (Completeness). If a program P is terminating, then RecP (f ) is disjunctively well-founded for every f defined in P .
3.3 From Binary Reachability to Plain Reachability
This subsection presents the reduction from the binary reachability problem of deciding
RecP (f ) ⊆ Df to a plain reachability problem. As remarked in Subsection 3.1, wetransform P to the program ⌈P ⌉f,Df that simulates the program P and asserts theproperty (ve′ , ev ) ∈ Df whenever a recursive call relation f ve′ ⊲P f ve is detected. Then,
RecP (f ) ⊆ Df holds if and only if an assertion in ⌈P ⌉f,Df may fail.
The target language of the program transformation is an extension of L with tuples he1 , . . . , ek i, assertions assert(e1 ); e2 , and a special value ⊥. The semantics ofassertions is defined by:E[assert(true); e] →P E[e]E[assert(false); e] →P failwhere the evaluation contexts are extended accordingly: E ::= · · · | assert(E); e.
The special value ⊥ is used in place of the argument of an ancestor call, when there isno tracked ancestor call; see examples below.
Before we give the formal definition of the transformation, ⌈·⌉f,Df , we informallydescribe the idea. The program ⌈P ⌉f,Df is obtained by adding extra function argumentsthat represent the arguments of past calls to f .
First we consider the simple case where the program only contains first-order functions. For example, let P be the Fibonacci program from Example 1. Let Dfib ={(pn, n) | pn > n ≥ 0}. Then, ⌈P ⌉fib,Dfib would be as follows.

1: let rec fib pn n =2: assert(pn>n && n≥0);
3: let pn’ = if ∗bool then pn else n in
4: if n < 2 then 1 else fib pn’ (n-1) + fib pn’ (n-2)
5: let main () = fib ⊥ ∗int
We have added the formal argument pn that represents the argument of an ancestor call(i.e., a call that corresponds to an ancestor node in the call tree) for fib, and inserted theassertion that checks (pn, n) ∈ Dfib (lines 1-2). Accordingly, we have also inserted an
extra parameter to each function call (calls in line 4). In line 3, we non-deterministically“update” the tracked argument to the current argument in order to compare the argumentof the current call with a future call of fib. The extra parameter is initially set to ⊥,to indicate that there is no ancestor call (line 5). We assume that > is extended so that⊥ > n holds for every n. For the two recursive calls to fib in the definition of fib,pn or n is passed in a non-deterministic manner. Below is a possible reduction of thetransformed program.
main () →∗ fib ⊥ 2 →∗ assert(⊥ > 2&&2 ≥ 0); · · ·→∗ fib 2 1 + fib 2 0→∗ (assert(2 > 1&&1 ≥ 0); · · · ) + fib 2 0→∗ 1 + fib 2 0→∗ 1 + (assert(2 > 0&&0 ≥ 0); · · · )→∗ 1 + 1 →∗ 2
The subexpressions fib 2 1 and fib 2 0 capture the fact that fib 1 and fib 0 are
called from fib 2 in the original program. It is easy to see that RecP (fib) ⊆ Dfib if
and only if ⌈P ⌉fib,Dfib does not cause an assertion failure.
The transformation is more subtle for higher-order programs with partial applications and indirect calls. For example, let P be the program indirect from Example 2 and 4. Suppose that we wish to show RecP (app) ⊆ Dapp where Dapp ={((ph, pv, pu), (h, v, u)) | pv > v ≥ 0}. Then, ⌈P ⌉app,Dapp would be as follows.
1: let apphv (ph,pv,pu) u =2:
assert(pv>v && v≥0);3:
let (ph,pv,pu) = if ∗bool then (ph,pv,pu) else (h,v,u)4:in5:h (ph,pv,pu) v (ph,pv,pu) u
6: let id (ph,pv,pu) u = u
7: let rec g (ph,pv,pu) x =8:
if x≤0 then id
9:else app (ph,pv,pu) g (ph,pv,pu) (x-1)
e ()e ∗int ⊥10: let main () = g ⊥e denotes (⊥, ⊥, ⊥). As before, the extra parameter (ph,pv,pu) is inserted
Here, ⊥
to represent the arguments of an ancestor call to app (line 1). Note that the extra parameter for this program takes a tuple of values, so that all three arguments of app
can be tracked (i.e., h, v, and u). As before, the assertion is inserted at the beginningof the body of app to check ((ph, pv, pu), (h, v, u)) ∈ Dfib (line 2), and we update
the tracked past arguments with the current arguments non-deterministically, in order
to compare the arguments of the current call with a future call of the function (line 3).
To soundly and completely track the extra parameters through partial applications
and indirect calls, we pass the extra parameter at every function application site (lines
5, 9, and 10). To be able to do this, note that we have also transformed the definitionsof id and g to take the extra parameters and pass them at the applications that occur
in their body (lines 6 and 7), and also transformed the definition of app to take anextra parameter argument just before h and v as well as just before u, even though
app only checks the well-foundedness against the one passed just before u. (Note thatin the definition of app is an unused argument.) This is needed, because, in general,
we cannot statically decide which (indirect) function call is a fully applied function
call, nor which is a call to the target function (i.e., app in the example). We note that
it is possible to soundly eliminate some of the redundancy via a static analysis (seeExample 5 below), but it is in general impossible to completely decide a priori whichfunction is called in what context. In effect, the idea of our transformation is to delegate
such tasks to the backend reachability checker.
Example 5. By using useless code elimination [34, 13], we can simplify the above program to:let app h v (ph,pv,pu) u =assert(pv>v && v≥0);let (ph,pv,pu) = if ∗bool then (ph,pv,pu) else (h,v,u) inh v (ph,pv,pu) u
let id (ph,pv,pu) u = u
let rec g x = if x≤0 then id else app g (x-1)
e ()let main () = g ∗int ⊥Below is a possible reduction of ⌈P ⌉app,Dapp . (For simplicity, we use a reduction
sequence from the optimized version in Example 5.)
e () −→∗ app g 1 ⊥e ()main () −→∗ g 2 ⊥∗∗−→ g 1 (g, 1, ()) () −→ app g 0 (g, 1, ()) ()Note that the reached state app g 0 (g, 1, ()) () captures the recursion relation app g 1 ()⊲P
app g 0 () of the original program P .

The Formal Definition of ⌈·⌉f,D
We now define the transformation formally. ⌈P ⌉f,D is obtained by transforming eachfunction definition:⌈P ⌉f,D = {⌈g x
e = e⌉f,D | g x
e = e ∈ P}

where the function definition transformation is defined as follows.
⌈g x1 · · · xk = e⌉f,D =
g s1 x1 · · · sk xk =

let s = check&upd(D, sk , hx1 , . . . , xk i) in ⌈e⌉s
if g = f
g s1 x1 · · · sk xk = ⌈e⌉sk
if g 6= f

Note that an extra parameter si is added before every original parameter xi of a function.
Therefore, as opposed to the informal examples given above, the main function in thetarget program now takes two arguments, the first of which is always instantiated to ⊥.
The code that checks the candidate well-foundedness and non-deterministically updates
the arguments is inserted at the beginning of the body of the target function f . Here,check&upd(D, sk , hx1 , . . . , xk i) denotes the expression
assert(D# (sk , hx1 , . . . , xk i); if ∗bool then sk else hx1 , . . . , xk i.
where the relation D# is the extension of D defined by:e hv1 , . . . , vk i) | v1 , . . . , vk are values}∪
D# = {(⊥,{(hv1′ , . . . , vk′ i, hv1 , . . . , vk i) | (h⌊v1′ ⌋, . . . , ⌊vk′ ⌋i, h⌊v1 ⌋, . . . , ⌊vk ⌋i) ∈ D}
Here, ⌊v⌋ is the value obtained by removing all the extra arguments from partial applications; see below for the definition. We assume that D# is represented by a formula ofsome logic. (In the implementation, we use the first-order logic with linear arithmetic.)
Note that the body e of each function definition is transformed by ⌈e⌉s where s is theextra parameter passed just before the last argument (non-deterministically updated tothe current arguments in the case of the target function). The expression transformation⌈e⌉s passes s at each application site in e, and is formally defined as follows.
⌈c⌉s = c⌈∗int ⌉s = ∗int
⌈f ⌉s = f⌈x⌉s = x⌈let x = e1 in e2 ⌉s = let x = ⌈e1 ⌉s in ⌈e2 ⌉s⌈e1 op e2 ⌉s = ⌈e1 ⌉s op ⌈e2 ⌉s⌈if e1 then e2 else e3 ⌉s = if ⌈e1 ⌉s then ⌈e2 ⌉s else ⌈e3 ⌉s⌈e1 e2 ⌉s = ⌈e1 ⌉s s ⌈e2 ⌉s
The operation ⌊e⌋ for removing extra arguments (used in the definition of D# ) isdefined as follows.
⌊c⌋ = c⌊∗int ⌋ = ∗int⌊f ⌋ = f⌊x⌋ = x⌊let x = e1 in e2 ⌋ = let x = ⌊e1 ⌋ in ⌊e2 ⌋⌊e1 op e2 ⌋ = ⌊e1 ⌋ op ⌊e2 ⌋⌊e1 s e2 ⌋ = ⌊e1 ⌋ ⌊e2 ⌋⌊if e1 then e2 else e3 ⌋ = if ⌊e1 ⌋then ⌊e2 ⌋else ⌊e3 ⌋Note that ⌊⌈e⌉s ⌋ = e.
We prove the soundness and the completeness of the transformation. The following theorem states the soundness of the transformation. It says that the target program
reaches an assertion failure when the recursion relation is not a subset of D.

Theorem 3 (Soundness of ⌈·⌉f,Df ).
Suppose that main () →∗P E1 [f v1 · · · vk ], f v1 · · · vk →+P E2 [f w1 · · · wk ], and(hv1 , . . . , vk i, hw1 , . . . , wk i) 6∈ D. Then, main ⊥ () →∗⌈P ⌉f,D fail.
The theorem below states the completeness. It says that the target program reaches
an assertion failure only when the recursion relation is not a subset of D.
Theorem 4 (Completeness of ⌈·⌉f,Df ).
If main ⊥ () →∗⌈P ⌉f,D fail, then main () →∗P E1 [f ve] and f ve →+e andP E2 [f w],(hev i, hwi)
e 6∈ D for some E1 , E2 , ve, w.
e
3.4 Ranking Function InferenceThis subsection details how we refine the candidate disjunctively well-founded relation
Df . As remarked in Subsection 3.1, we actually infer both Df and the implicit parameter instantiation σ. The implicit parameters are used to assert and check well-founded
relation over function closure values.
We first describe the case where only Df is inferred. (This happens, for example,
when f is first-order and does not take function closures as arguments.) Recall that theinference is invoked when Rec(f ) 6⊆ Df (cf. Step 3 of Figure 5), and in such a case,the reachability checker returns a counterexample of the form:
main () →∗ E[f s1 v1 s2 v2 · · · (v1′ , . . . , vn′ ) vn ]→ assert((v1′ , . . . , vn′ ), (v1 , . . . , vn )) ∈ Df ); . . . → failAs remarked in Subsection 3.3, this implies that f v1′ · · · vn′ ⊲ f v1 · · · vn , and we havethat ((v1′ , . . . , vn′ ), (v1 , . . . , vn )) ∈ Rec(f ) and ((v1′ , . . . , vn′ ), (v1 , . . . , vn )) 6∈ Df .
The goal of ranking function inference is to obtain a refined disjunctively wellfounded relation Df′ such thatDf ∪ {((v1′ , . . . , vn′ ), (v1 , . . . , vn ))} ⊆ Df′ .
To this end, we infer a new ranking function r(x1 , . . . , xn ) such that r(v1′ , . . . , vn′ ) >r(v1 , . . . , vn ) ≥ 0 and let Df′ = Df ∪ {(ex′ , xe) | r(ex′ ) > r(ex) ≥ 0}. We adopt theconstraint-based technique [25, 5] to infer r(ex).
We overview the inference process. We prepare a ranking function template c0 +c1 x1 + · · · + cn xn . Here, ci ’s are fresh variables, serving as unknowns. Then, we solve
for the assignments to ci ’s that satisfy the constraint∀ex.[[π]] ⇒ c0 + c1 v1′ + · · · + cn vn′ > c0 + c1 v1 + · · · + cn vn ≥ 0
where xe are the free variables in [[π]] and v1 , . . . , vn , v1′ , . . . , vn′ . Here, [[π]] is the strongest
postcondition of the given counterexample π.9 Finally, we set r(x1 , . . . , xn ) = α0 +α1 x1 + · · · + αn xn where each αi is the assignment obtained for ci .
Next, we extend the above process with implicit parameters to infer ranking functions over higher-order values. We illustrate the need for ranking functions over higherorder values with the following program indirectHO.
9

More precisely, we construct a corresponding straightline program from the counterexample,
and take its strongest postcondition (cf. [16, 33] and Appendix E).

let app h v = h () v
let id x = x
let rec g x u =if x <= 0 then id else app (g (x-1))
let main () = g ∗int () ()The program is similar to indirect from Example 2 and 4, except that app no longer
takes an integer argument and instead has the “decreasing” integer value captured inside
the function closure passed as h. To show that this program is terminating, we needto show that the recursion relation for app is disjunctively well-founded. However,
because app only takes function-type arguments (besides unit), ranking functions overfirst-order values are insufficient for this.
To this end, we adopt the idea from the previous work [33] and systematically
add an integer-type implicit parameter just before each function-type parameter.10 For
indirectHO, we add an implicit parameter h IMPARAM before h so that the program
is now the following. (The added parts are underlined.)
let app h IMPARAM h () = h () ()let id x = x
let rec g x () =if x <= 0 then id else app σ(ℓ) (g (x-1))
let main () = g ∗int () ()Here, σ is the candidate implicit parameter instantiation that maps each instantiationsite ℓ to an arithmetic expression over the variables bound in the context of ℓ. Formally,an instantiation site is at an application of a function-type argument, and is syntacticallydetermined (i.e., between e1 e2 where e2 is function-type). Clearly, the addition of
implicit parameters and their instantiations do not affect the termination of the program,and so we may check the termination of the program with the implicit parameters added
to check the termination of the original. The verification process starts by initializing
the candidate instantiations to some arithmetic expression (e.g., 0), and refine them
iteratively via a counterexample analysis (cf. Figure 5).
As remarked above, in the presence of implicit parameters, we infer both σ andDf when given a counterexample. To this end, the above inference process is extended
as follows. We prepare templates for the instantiation expressions in addition to thetemplates for the ranking functions. Then, when generating the constraints, we use thetemplate instantiation expressions in the strongest postcondition of the counterexample,
and solve for both the unknowns in the ranking function templates and the instantiation
expression templates.
More formally, let Π = {π1 , . . . , πm } be the set of counterexamples we have seen
so far for f . We prepare a template instantiation map ∆ that maps each ℓ to an expression of the form c0 + c1 x1 + · · · + cn xn where ci ’s are fresh unknowns and xi ’s are
the integer-type variables that are bound in the context of ℓ (which may include implicit
10

Implicit parameters are called “extra parameters” in [33]. We call them implicit parameters
here to avoid confusion with the extra parameters in this paper which are used for a different
purpose.

program
ord time
Ackermann 1 5.85
Fibonacci 1 0.15
McCarthy91 1 4.95
loop2
1 0.61append
1 0.14zip
1 0.15binomial
1 0.70programord time
alias partial 1
0.32
quicksort2
timeout
indirectIntro 2
4.76
indirect2
1.36
indirectHO2
7.75
CE-0CFA2
0.14
CE-1CFA2
0.24

programord timechurchNum
4 3.13
CE-Jones Bohr 4 0.71
up down
2 0.65map
2 1.59toChurch
2 0.69x plus 2ˆn
2 2.02foldr
2 1.19

Table 1. Experiment results.

parameters). Then, we form the following constraint^′′∀ex.[[π∆]] ⇒ cπ,0 +cπ,1 vπ,1+· · ·+cπ,nvπ,n> cπ,0 +cπ,1vπ,1 +· · ·+cπ,n vπ,n ≥ 0π∈Πwhere cπ,i ’s are fresh unknowns, and x
e are the free non-unknown variables in [[π∆]]and v1 , . . . , vn , v1′ , . . . , vn′ . (Here, we assume that the counterexamples π explicitly
use the instantiation sites ℓ as expressions.) We solve for the unknowns that satisfy
the constraint to obtain implicit parameter instantiations and ranking functions that
refute the counterexample. We obtain theSnew candidate disjunctive well-founded rex′ , xe) | rπ (ex′ ) > rπ (ex) ≥ 0} wherelation from the ranking functions: D = π∈Π {(erπ (ex) = απ,0 + απ,1 x1 + · · · + απ,n xn and each απ,i is the obtained assignment
for cπ,i . And, we substitute the assignments to the unknowns in ∆ to obtain the new
candidate implicit parameter instantiation. Appendix E contains details of the inference
process applied to indirectHO.

4 Implementation and Experiments
We have implemented a prototype of the termination verifier for a subset of OCaml.
We use MoCHi [16] as the backend reachability checker, and Z3 [22] as a constraint
solver for ranking function inference. As an optimization, we have extended the ranking
function inference described in Section 3.4 to also infer lexicographic linear ranking
functions [5] whenever possible. Appendix F contains details of the lexicographic linear
ranking function inference process.
We have tested our tool on various termination verification benchmark programs inliterature, taken mostly from the previous work on termination verification of higherorder programs, as well as some synthetic but non-trivial examples. We ran the experiment on a machine with 3.20GHz CPU and 16GB of memory, with timeout of 600
seconds. The web interface of the verification tool and the programs used in the experiments are available online [17].
Table 1 summarizes the experiment results. The column “program” shows the namesof programs, and the column “ord” shows the order of the program (where order-1 functions take only base type values, order-2 functions may take order-1 functions as arguments, etc., and the order of a program is the maximum order of the functions in the
program). The column “time” shows the running time in seconds.

We briefly describe the benchmark programs. The seven programs in the left column
and alias partial are first-order (i.e., order-1) programs. The programs append,zip, and binomial are from [2]. Ackermann is the Ackermann’s function, and isalso used as examples in [2, 35]. McCarthy91 is the McCarthy’s 91 function (used asa benchmark program in, e.g., [18]11). Fibonacci is the Fibonacci number function
from Example 1. The program alias partial is from Section 8 of [18] and is given
as an example on which their approach fails.
The program quicksort is from [35],12 and is a second-order program where
the list sorting function is parametrized by the “compare” function. We check the termination of a program that passes the sorting function a terminating compare function
and an arbitrary list. (Our tool currently does not directly support lists, and so a list
is represented by the integer denoting its length.) Our tool fails to verify the program
within the time limit due to the underlying reachability checker MoCHi failing to verify
the necessary assertion safety. This is not a fundamental limitation with our termination verification approach, and we expect further advances in reachability verification
to allow our approach to verify instances like quicksort.
The rest of the programs are higher-order programs whose termination depends
non-trivially on the functions passed as the arguments, and precise reasoning about
the function arguments is required for proving termination. They are mostly from theexamples and benchmarks in [12, 28, 29]. Many of these are difficult examples that theprevious approaches cannot verify. (We have selected the ones given as examples where
their approaches fail). We refer to Appendix G for further description of these programs.
As seen in Table 1, the benchmark results are promising and show that our tool is able toautomatically verify the difficult instances quickly, except quicksort whose reason
for the failure is elaborated above.

5 Related Work
There have been three major approaches to automated termination verification for firstorder programs: transition invariants [26, 3, 4], size-change termination [19], and term
rewriting [7] (see also [32, 8] for relationships between those approaches). The approaches have recently been extended to the termination verification of higher-orderprograms [18, 30, 28, 29, 6, 12]. Below, we compare them with our approach.
5.1 Transition Invariants
Closest to our work is the work by Ledesma-Garza and Rybalchenko [18]. Similar
to our work, they propose a program transformation to reduce the transition invariant
verification problem (i.e., binary reachability analysis) to a plain reachability problem
via a program transformation. Unfortunately, as also admitted in their paper (Section
8 of [18]), their approach has a limited applicability to the verification of higher-order
11[18] is not fully automated and requires the user to provide the sufficient ranking functions aswell as the predicates to be used for reachability checking.
12[35] is not automated.

programs because it does not correctly handle indirect calls and is actually unsound.
For example, their approach would incorrectly report the program P0 from Section 1
to be terminating. Moreover, their approach is not fully automated and requires a sufficient well-foundedness relation to be provided manually, and it also cannot handle
well-foundedness relations over function closure values.
By contrast, we have proposed the first sound and (relatively) complete approachto termination verification of higher-order programs via binary reachability analysis.
A key idea of our approach is the novel program transformation that precisely tracks
the call-tree ancestor’s arguments values through the higher-order control flow withouta priori approximation. We have also presented a method to infer well-foundedness
relations (including those over function closure values) from counterexamples returned
by a higher-order program verifier, thus realizing a fully automated verification.
5.2 Size-Change Analysis
The size-change approach [19] to termination verification involves the following two
steps: (1) an analysis of the program to construct a size-change graph, and (2) an analysis of the obtained graph to decide if the program is terminating. For functional programs, the size-change graph is a graph comprising functions in the program where theedges express the changes in the values that may be passed as arguments. Step (1) constructs the graph by statically approximating the possible calls that the program would
make in its actual execution.
To apply size-change termination verification to higher-order programs, a control
flow analysis (CFA) is employed to statically approximate the possible call relations as
a call graph and construct a sound size-change graph from the call graph [30, 28, 29, 12].
Therefore, the approach involves a priori approximation of the program, and can leadto loss in a precision when a precise graph cannot be constructed by the static analysis.
For example, the approach may fail on cases where a non-terminating call depends ona safety property (recall the simple example from Section 1 where a non-terminating
function is called if and only if the condition p(x) is met). By contrast, our approach
suffers no a priori loss in precision and is sound and complete.
Like our approach, the size-change approach to higher-order programs [30, 28, 29,
12] can prove termination of programs that require well-foundedness relation over function closure values. For example, Jones and Bohr [12] and Sereni [28] order closure arguments by using the subtree relation on their tree representations. By contrast, we havepresented a generic approach that uses implicit parameters and counterexample analysis to infer the appropriate instantiations for the implicit parameters. Our approach ismore general in the sense that it is not fixed to one pattern of closure information to be
used for the well-foundedness relation. For example, the subtree relation used in [12,28] can be expressed by inferring instantiations that encode the depth of the closures,and our prototype implementation automatically verifies examples in their paper that
require such information (cf. Section 4 and Appendix G).
On the other hand, we employ counterexample analysis and constraint-based inference to automatically infer the instantiations, and so the approach of Jones, Bohr,
and Sereni that fixes the closure information to a pre-determined pattern may be more
efficient on instances that are known to be verifiable with such information.

5.3 Term Rewriting
Similar to the size-change approach, the application of termination verification techniques for term rewriting systems to higher-order programs is done in a two-step process [6]. There, in the first step, a static analysis is employed to construct a term rewriting system that soundly approximates the given program such that the program is terminating if the constructed rewriting system is terminating. Then, the second step applies
a termination verifier for term rewriting systems [7] to verify termination.
As with the size-change approach, this two-step approach can introduce a loss inprecision because of the approximation in the first step. For example, Giesl et al. [6]show a simple program on which their approach fails because of this limitation (Example 4.12 in [6]).

6 Conclusion
We have presented a new automated approach to termination verification of higherorder functional programs. In stark contrast to the previous approaches, our approach
is sound and complete relative to the soundness and completeness of the underlying
reachability analysis and ranking function inference. Our approach is the first soundbinary reachability analysis based approach to the termination verification of higherorder programs. The key features of our approach are the novel program transformationthat correctly tracks the call-tree ancestor’s arguments through the higher-order control flow, and the inference method for ranking functions over higher-order values via
implicit parameter instantiation inference.

References
1. Ball, T., Rajamani, S.K.: The SLAM project: debugging system software via static analysis.
In: POPL. pp. 1–3 (2002)
2. Chin, W.N., Khoo, S.C.: Calculating sized types. Higher-Order and Symbolic Computation
14(2-3), 261–300 (2001)
3. Cook, B., Podelski, A., Rybalchenko, A.: Abstraction refinement for termination. In: SAS.
Lecture Notes in Computer Science, vol. 3672, pp. 87–101. Springer (2005)
4. Cook, B., Podelski, A., Rybalchenko, A.: Termination proofs for systems code. In: PLDI.
pp. 415–426. ACM (2006)
5. Cook, B., See, A., Zuleger, F.: Ramsey vs. lexicographic termination proving. In: TACAS.
Lecture Notes in Computer Science, vol. 7795, pp. 47–61. Springer (2013)
6. Giesl, J., Raffelsieper, M., Schneider-Kamp, P., Swiderski, S., Thiemann, R.: Automatedtermination proofs for Haskell by term rewriting. ACM Transactions on Programming Languages and Systems 33(2), 7:1–7:39 (Feb 2011)
7. Giesl, J., Thiemann, R., Schneider-Kamp, P., Falke, S.: Automated termination proofs with
AProVE. In: RTA. LNCS, vol. 3091, pp. 210–220. Springer (2004)
8. Heizmann, M., Jones, N.D., Podelski, A.: Size-change termination and transition invariants.
In: SAS. LNCS, vol. 6337, pp. 22–50. Springer (2010)
9. Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: POPL. pp. 58–70(2002)
10. Jhala, R., Majumdar, R.: Software model checking. ACM Comput. Surv. 41(4) (2009)11. Jhala, R., Majumdar, R., Rybalchenko, A.: HMC: Verifying functional programs using abstract interpreters. In: CAV. Lecture Notes in Computer Science, vol. 6806, pp. 470–485.
Springer (2011)12. Jones, N.D., Bohr, N.: Call-by-value termination in the untyped lambda-calculus. Logical
Methods in Computer Science 4(1) (2008)
13. Kobayashi, N.: Type-based useless-variable elimination. Higher-Order and Symbolic Computation 14(2-3), 221–260 (2001)
14. Kobayashi, N.: Model checking higher-order programs. Journal of the ACM 60(3) (2013)
15. Kobayashi, N., Ong, C.H.L.: A type system equivalent to the modal mu-calculus model
checking of higher-order recursion schemes. In: LICS. pp. 179–188. IEEE Computer Society (2009)
16. Kobayashi, N., Sato, R., Unno, H.: Predicate abstraction and CEGAR for higher-order model
checking. In: PLDI. pp. 222–233. ACM (2011)
17. Kuwahara, T., Terauchi, T., Unno, H., Kobayashi, N.: Automatic termination verification forhigher-order functional programs (2013), http://www-kb.is.s.u-tokyo.ac.jp/
˜kuwahara/termination
18. Ledesma-Garza, R., Rybalchenko, A.: Binary reachability analysis of higher order functional
programs. In: SAS. LNCS, vol. 7460, pp. 388–404. Springer (2012)
19. Lee, C.S., Jones, N.D., Ben-Amram, A.M.: The size-change principle for program termination. In: POPL. pp. 81–92. ACM (2001)
20. Lester, M.M., Neatherway, R.P., Ong, C.H.L., Ramsay, S.J.: Model checking liveness properties of higher-order functional programs. In: Proceedings of ML Workshop 2011 (2011)
21. McMillan, K.L.: Lazy abstraction with interpolants. In: CAV. Lecture Notes in Computer
Science, vol. 4144, pp. 123–136. Springer (2006)
22. de Moura, L.M., Bjørner, N.: Z3: An efficient SMT solver. In: TACAS. Lecture Notes in
Computer Science, vol. 4963, pp. 337–340. Springer (2008)
23. Ong, C.H.L.: On model-checking trees generated by higher-order recursion schemes. In:
LICS. pp. 81–90. IEEE Computer Society (2006)
24. Ong, C.H.L., Ramsay, S.: Verifying higher-order programs with pattern-matching algebraic
data types. In: Proceedings of POPL 2011. pp. 587–598. ACM (2011)25. Podelski, A., Rybalchenko, A.: A complete method for the synthesis of linear ranking functions. In: VMCAI. Lecture Notes in Computer Science, vol. 2937, pp. 239–251. Springer(2004)
26. Podelski, A., Rybalchenko, A.: Transition invariants. In: LICS. pp. 32–41. IEEE Computer
Society (2004)
27. Rondon, P.M., Kawaguchi, M., Jhala, R.: Liquid types. In: PLDI. pp. 159–169. ACM (2008)
28. Sereni, D.: Termination analysis of higher-order functional programs. Ph.D. thesis, Magdalen
College (2006)
29. Sereni, D.: Termination analysis and call graph construction for higher-order functional programs. In: ICFP. pp. 71–84. ACM (2007)
30. Sereni, D., Jones, N.D.: Termination analysis of higher-order functional programs. In:
APLAS. Lecture Notes in Computer Science, vol. 3780, pp. 281–297. Springer (2005)
31. Terauchi, T.: Dependent types from counterexamples. In: POPL. pp. 119–130. ACM (2010)
32. Thiemann, R., Giesl, J.: The size-change principle and dependency pairs for termination ofterm rewriting. Appl. Algebra Eng. Commun. Comput. 16(4), 229–270 (2005)
33. Unno, H., Terauchi, T., Kobayashi, N.: Automating relatively complete verification of higherorder functional programs. In: POPL. pp. 75–86. ACM (2013)
34. Wand, M., Siveroni, I.: Constraint systems for useless variable elimination. In: Proceedingsof POPL ’99. pp. 291–302 (1999)
35. Xi, H.: Dependent types for program termination verification. In: LICS ’01. pp. 231–242.
IEEE (2001)

36. Xi, H., Pfenning, F.: Dependent types in practical programming. In: POPL. pp. 214–227(1999)
37. Zhu, H., Jagannathan, S.: Compositional and lightweight dependent type inference for ML.
In: VMCAI. LNCS, vol. 7737, pp. 295–314. Springer (2013)

Appendix
A

Proof of Theorem 1

We first prove the following lemma.
Lemma 1. If RecP (f ) is disjunctively well-founded for every function f defined in P ,then every sequence f1 ve1 ⊲P f2 ve2 ⊲P . . . ⊲P fn vf
n ⊲P . . . is finite.

Proof. Suppose that RecP (f ) is disjunctively well-founded for every f , but that there isan infinite sequence f1 ve1 ⊲P f2 ve2 ⊲P . . .⊲P fn vf
n ⊲P . . .. Because the number of function
symbols fi is finite, there must be f such that fi = f for infinitely many i’s. But, thiscontradicts with the assumption that RecP (f ) is disjunctively well-founded and thefact that RecP (f ) is transitive. (Recall that a transitive relation that is disjunctively
well-founded is also well-founded.)⊓⊔
We are now ready to prove the soundness of the reduction.
Proof. [Theorem 1] Suppose that RecP (f ) is disjunctively well-founded for every f ,but that there were an infinite reduction sequence π:main ()(= e0 ) →P e1 →P e2 →P · · ·We write (f ev , i)⊲πP (g w,
e j) if, for some E1 and E2 , ei = E1 [f ve] and ej = E1 [E2 [g w]]
e

with j > i ≥ 0, arity(f ) = |ev | and arity (g) = |w|e and if E1 is not reduced in the
sub-sequence ei →∗P ej of π. By definition, ⊲πP is a restriction of ⊲P in the sense that(f ve, i) ⊲πP (g w,
e j) implies f ve ⊲P g w.
e
Define Tπ as the tree consisting of the set Vπ of nodes and the set Eπ of edges givenby:Vπ = {(f ve, i) | arity(f ) = |ev | and ei = E [f ve]}Eπ = {((f ve, i), (g w,e j)) | (f ve, i) ⊲πP (g w,
e j)∧¬∃k, h, ze.((f ve, i) ⊲πP (h ze, k) ∧ k < j)}We note that this is the formal definition of the call tree mentioned in Subsection 3.1.
By the assumption that π is infinite, function definitions must be unfolded infinitely
many times; thus, the tree Tπ must be infinite. However, Tπ is finitely branching (toobserve this, notice that if ((f ve, i), (g w,e j)) ∈ Eπ , then (g w,
e j) must be called fromthe body of f obtained by reducing f ve), and every path from the root in Tπ must be
finite, by Lemma 1 and the fact that ⊲πP is a restriction of ⊲P . By König’s lemma, Tπ
must be finite, hence a contradiction.
⊓⊔

B Proof of Theorem 2
It suffices to show that RecP (f ) is well-founded if P is terminating. We prove thecontraposition. Suppose that RecP (f ) is not well-founded. Then there is an infinite
sequence f ev0 ⊲P f e
v1 ⊲P f ev2 ⊲P . . .. By the definition of ⊲P , we have f vei →+P
Ei [f vei+1 ] for every i ≥ 0, and main () →∗P E0 [f ve1 ]. Therefore, we have an infinite
reduction sequence:
main () →∗P E0 [f ve1 ] →+e2 ]] →+
e3 ]]] →+P E0 [E1 [f v
P E0 [E1 [E2 [f vP ···Thus, P is not terminating.

C

Proof of Theorem 3

We define the relation ∼s between the source expressions and the target expressions asfollows,
v is a value⌊v⌋ ∼s v
x ∼s x∗int ∼s ∗int
e1 ∼s e′1e2 ∼s e′2
let x = e1 in e2 ∼s let x = e′1 in e′2
e1 ∼s e′1e2 ∼s e′2
e1 op e2 ∼s e′1 op e′2
e1 ∼s e′1e2 ∼s e′2e3 ∼s e′3
if e1 then e2 else e3 ∼s if e′1 then e′2 else e′3
e1 ∼s e′1e2 ∼s e′2′
e1 e2 ∼s e1 s e′2
Let D0 be the relation that relates all the elements, that is, D0 (hev i, hev ′ i) for all′
values ve and ve .

Lemma 2. Let P be a program, e1 be a closed expression, and s be ⊥ or a tuple ofvalues hvi. If e1 →P e2 and e1 ∼s e′1 , then e′1 →∗⌈P ⌉f,D e′2 for some e′2 such that0e2 ∼s e′2 .
Proof. This follows by case analysis on the rule used for e →P e′ . The only non-trivial
case is whene1 ≡ E[f ve] →P E[[ev /ex]e0 ] ≡ e2

where f x
e = e0 . By the assumption e1 ∼s e′1 , e′1 is of the form E ′ [f s1 v1′ · · · sk vk′ ]with sk = s, E ∼s E ′ and ve ∼s v1′ · · · vk′ (where ∼s is extended to contexts in a naturalway). Thus, we have:e1 ≡ E ′ [f s1 v1′ · · · sk vk′ ]→∗ E ′ [let s0 = check&upd(D0# , s, hve′ i) in[v1′ /x1 , . . . , vk′ /xk ]⌈e0 ⌉s0 ]∗′→ E [let s0 = s in [v1′ /x1 , . . . , vk′ /xk ]⌈e0 ⌉s0 ]→∗ E ′ [[v1′ /x1 , . . . , vk′ /xk ]⌈e0 ⌉s ]and e2 ∼s E ′ [[v1′ /x1 , . . . , vk′ /xk ]⌈e0 ⌉s ] as required.

⊓⊔

The following lemma states that every element of the recursion relation may occur
in a reduction sequence of the target program.
Lemma 3. Suppose main () →∗P E1 [f v1 · · · vk ] and f v1 · · · vk →+P E2 [f w1 · · · wk ].
Then,main ⊥ () →∗⌈P ⌉f,D E[f s1 w1′ · · · sk wk′ ]0for some E,s1 , . . . , sk and w1′ , . . . , wk′ such that sk = hv1′ , . . . , vk′ i with ⌊vi′ ⌋ = vi and⌊wi′ ⌋ = wi for i ∈ {1, . . . , k}.
Proof. By the assumption main () →∗P E1 [f v1 · · · vk ] and Lemma 2, we havemain ⊥ () →∗⌈P ⌉f,D e10

for some e1 such that E1 [f v1 · · · vk ] ∼⊥ e1 . Thus, e1 must be of the form E1′ [f s1 v1′ · · · ⊥ vk′ ]where ⌊vi′ ⌋ = vi for every i ∈ {1, . . . , k}. By the assumption f v1 · · · vk →+P E2 [f w1 · · · wk ],we havef v1 · · · vk →P [v1 /x1 , . . . , vk /xk ]e0 →∗P E2 [f w1 · · · wk ]where f x1 · · · xk = e0 ∈ P . The expression f s1 v1′ · · · ⊥ vk′ is reduced as follows:
f s1 v1′ · · · ⊥ vk′→⌈P ⌉f,D0 let s = check&upd(D0# , ⊥, hv1′ , . . . , vk′ i) in[v1′ /x1 , . . . , vk′ /xk ]⌈e0 ⌉s∗→⌈P ⌉f,D [v1′ /x1 , . . . , vk′ /xk ]⌈e0 ⌉hv1′ ,...,vk′ i0Let ve′ = hv1′ , . . . , vk′ i. By[v1 /x1 , . . . , vk /xk ]e0 →∗P E2 [f w1 · · · wk ]and[v1 /x1 , . . . , vk /xk ]e0 ∼ve′ [v1′ /x1 , . . . , vk′ /xk ]⌈e0 ⌉ve′ ,we have:[v1′ /x1 , . . . , vk′ /xk ]⌈e0 ⌉ve′ →∗⌈P ⌉f,D e20

for some e2 such that E2 [f w1 · · · wk ] ∼ve′ e2 . Because arity(f ) = k, e2 must be of
the form E2′ [f s1 w1′ · · · ve′ wk′ ], and the required conditions are satisfied.
⊓⊔

Proof. [Theorem 3] By the assumption and Lemma 3, either we havemain ⊥ () →∗⌈P ⌉f,D E[f s1 w1′ · · · sk wk′ ] for some E,s1 , . . . , sk and w1′ , . . . , wk′ suchthat sk = hv1′ , . . . , vk′ i with ⌊vi′ ⌋ = vi and ⌊wi′ ⌋ = wi for i ∈ {1, . . . , k}, or main ⊥ () →∗⌈P ⌉f,D
fail (because →∗⌈P ⌉f,D is the same except that the assertions are stronger). In the former case, by the assumption(hv1 , . . . , vk i, hw1 , . . . , wk i) 6∈ D,
we have main ⊥ () →∗⌈P ⌉f,D fail as required.

⊓
⊔

D

Proof of Theorem 4

Lemma 4. Let P be a program, e1 be a closed expression, and s be ⊥ or a tuple
′′
′
′
′
∗
of values hvi. If e′1 →+⌈P ⌉f,D0 e2 , then ⌊e1 ⌋ →P e2 and either e2 →⌈P ⌉f,D0 e2 or
e′′2 →∗⌈P ⌉f,D e′2 for some e2 and e′′2 such that e2 = ⌊e′′2 ⌋.
0

Proof. This follows by straightforward induction on the case analysis on the rule used′
for the first reduction step of e′1 →+⌈P ⌉f,D e2 . The only non-trivial case is when0e′1 ≡ E ′ [f s1 v1′ · · · sk vk′ ] →⌈P ⌉f,D0
let s = check&upd(D0# , sk , hv1′ , . . . , vk′ i) in[v1′ /x1 , . . . , vk′ /xk ]⌈e0 ⌉s ≡ e′2
with f x1 · · · xk = e0 ∈ P . In this case, we have e1 ≡ E[f ve] with E = ⌊E ′ ⌋and ⌊ev ⌋ = ⌊ev ′ ⌋. The required result holds for e2 = [v1 /x1 , . . . , vk /xk ]e0 and e′′2 =′′⊓⊔E [[v1 /x1 , . . . , vk′ /xk ]⌈e0 ⌉s′ ] where s′ is sk or hv1′ , . . . , vk′ i.
Lemma 5. If main ⊥ () →∗⌈P ⌉f,D E[g s1 w1′ · · · sℓ wℓ′ ] with sℓ = hv1′ , . . . , vk′ i and0arity(g) = ℓ, then main () →∗P E1 [f v1 · · · vk ] and f v1 · · · vk →+P E2 [g w1 · · · wℓ ],for some E1 , E2 , ve, w
e such that ⌊vi′ ⌋ = vi for i ∈ {1, . . . , k}. and ⌊wi′ ⌋ = wi for
i ∈ {1, . . . , ℓ}.

Proof. Suppose main ⊥ () →∗⌈P ⌉f,D E[g s1 w1′ · · · sk wℓ′ ] and sℓ = hv1′ , . . . , vk′ i.
0Then, by the definition of the transformation, it must be the case that main ⊥ () →∗⌈P ⌉f,D
0
E1′ [f s′1 v1′ · · · s′k vk′ ] and f s′1 v1′ · · · s′k vk′ →∗⌈P ⌉f,D E2′ [g s1 w1′ · · · sℓ wℓ′ ] with E =0E1′ [E2′ ]. (Formally, this is proved by induction on the length of the reduction sequence.
) By Lemma 4, we obtain the required property.
⊓⊔
Proof. [Theorem 4] By the assumption main ⊥ () →∗⌈P ⌉f,D fail, we havemain ⊥ () →∗⌈P ⌉f,D E[f s1 w1′ · · · sk wk′ ]0with (sk , wk′ ) 6∈ D# . Thus, the statement follows from Lemma 5.

⊓⊔

E Implicit Parameter Instantiation Inference Example
Consider the program indirectHO from Section 3.4. As remarked there, an implicit
parameter is added to the program as follows.
let app h IMPARAM h v = h () v
let id x = x
let rec g x u =if x <= 0 then id else app σ(ℓ) (g (x-1))
let main () = g ∗int () ()We initialize σ(ℓ) = 0.
The transformed program ⌈indirectHO⌉σ,app,∅ is shown below.13
13Here, the program is simplified and only has the implicit parameter is tracked via the extra parameter for carrying call-tree ancestor’s arguments. That is, it only tracks the previous
h IMPARAM (in ph IMPARAM) and does not track the previous values of h and v.

let apph IMPARAMh ph IMPARAM v =assert (ph IMPARAM 6= ⊥);let s = if ∗bool then ph IMPARAM else h IMPARAM in
h s () s v
let id s x = x
let rec gx s u =
if x ≤ 0 then id
else app s 0 s (g s (x-1))
let main xs () = g xs ∗int xs ()The program causes an assertion failure, and we obtain the counterexample as an error path in ⌈indirectHO⌉app,∅ . Suppose we obtained the error path represented as thefollowing reduction sequence:
main ⊥ () →∗ g ⊥ 2 ⊥ ()→∗ app ⊥ σ(ℓ) ⊥ (g ⊥ 1) ⊥ ()→∗ g σ(ℓ) 1 σ(ℓ) ()→∗ app σ(ℓ) σ(ℓ) σ(ℓ) (g σ(ℓ) 0) σ(ℓ) ()→∗ assert(σ(ℓ)=⊥) → failTo build the strongest post condition of the counterexample, we build the straightline higher-order program (henceforth abbreviated to SHP) corresponding to the counterexample path. SHP is a recursion-free slice of the program obtained by copying functions and removing branches so that it contains no branches and every function occurrence is “linear” (i.e., each function is called at most once), such that the evaluating
the SHP results in the counterexample path as the reduction sequence. We refer to theprevious work [16, 33] for more details on SHP.
From the counterexample above, we obtain the following SHP π.14 (Here, the expression “assume(cond);e” evaluates e if cond is true and otherwise gets stucksafely.)let rec main xs () = g(1) xs ∗int xs ()and g(1)x s u =
assume (¬(x ≤ 0)); app(1) s ℓg(1) s (g(2) s (x-1))
and app(1)h IMPARAMh ph IMPARAM v =assume (¬(ph IMPARAM 6= ⊥));
let s = h IMPARAM in h s () s v
and g(2)x s u =
assume (¬(x ≤ 0)); app(2) s ℓg(2) s (g(3) s (x-1))
x s () = assume (false); u
and g(3)and app(2)h IMPARAMh ph IMPARAM () =assume (ph IMPARAM6= ⊥); fail14

Unlike in the main body of the paper, here we use π to denote the SHP instead of the counterexample path.

We prepare the template c1,0 + c1,1 xg(1) (resp. c2,0 + c2,1 xg(2) ) for the instantiationsite ℓg(1) (resp. ℓg(2) ) with fresh unknowns. (Generally, for an instantiation site ℓ, we
prepare the template c0 + c1 x1 +h· · · + cm xm where x1 ,i. h. . , xm are the variablesi boundin the context of ℓ.) We let ∆ = c1,0 + c1,1 xℓg(1) /ℓg(1) c2,0 + c2,1 xℓg(1) /ℓg(2) be thetemplate instantiation map.
Then, the following strongest postcondition [[π∆]] is computed by symbolicallyevaluating π∆. (The formula is slightly simplified.)[[π∆]] ≡ xg(1) > 0 ∧ h IMPARAMapp(1) = σ(ℓg(1) )∧ph IMPARAMapp(1) = ⊥ ∧ xg(2) = xg(1) − 1 ∧ xg(2) > 0∧h IMPARAMapp(2) = σ(ℓg(2) )∧ph IMPARAMapp(2) = h IMPARAMapp(1)∧ph IMPARAMapp(2) 6= ⊥Next, we prepare the ranking function template T (x) = c0 + c1 x with fresh unknowns and solve for the assignments to the unknowns satisfying the constraint below.
∀ex.[[π∆]] ⇒ T (ph IMPARAMapp(2) ) > T (h IMPARAMapp(2) ) ≥ 0
Suppose we obtain the following as the solution to the constraint.
c0 7→ 0, c1 7→ 1, c1,0 7→ 0, c1,1 7→ 1, c2,0 7→ 0, c2,1 7→ 1
This gives us the new ranking function r(x) = T (x) [0/c0 ] [1/c1 ] and the new implicit
parameter instantiation σ ′ = ∆ [0/c1,0 ] [1/c1,1 ] [0/c2,0 ] [1/c2,1 ]. We refine Dapp from∅ to {(x, x′ ) | r(x) > r(x′ ) ≥ 0}, and the implicit parameter instantiation to σ ′ .
With the refined candidate well-founded relation and implicit parameter instantiation, the reachability checker is able to verify that ⌈indirectHO⌉σ′ ,app,Dapp is assertion
safe. And, the program is verified to be terminating.

F

Lexicographic Linear Ranking Function

Cook et al. [5] have proposed a counterexample-guided method to infer a class of wellfounded relations called lexicographic linear ranking functions (LLRFs). LLRFs is asequence of ranking functions hr1 , . . . , rn i that represents the following well-founded
relation.
VWrj (ex′ ) ≤ rj (e
x)}
ri (e
x′ ) > ri (ex) ≥ 0 ∧{(ex′ , x
e) |
i≤n

j≤i−1

Inferring LLRFs can be done by a constraint-based method similar to the ranking function inference described in Section 3.4.
As observed in [5], one can often find LLRFs that refutes all the currently-seencounterexamples to form a sufficient termination argument, which, in turn, allows theverification process to check the termination argument against the call tree relation as
opposed to the transitive closure of the call tree relation. In an approach based on a
reduction to binary reachability, this means that we can use an optimized version of
the program transformation that avoids building the transitive closure. We informallydescribe the optimized transformation using an example.

Example 6. Consider the following program.
let rec f m n =let r = ∗int in
if r > 0 && m > 0 then f (m-1) ∗int
else if r <= 0 && n > 0 then f m (n-1)
else ()
let main () = f ∗int ∗int
Note that either m or n is decremented non-deterministically by a recursive call to f.
Note that we cannot verify the program’s termination via one linear ranking function,
because the recursion f m n⊲f (m-1) ∗int only depends on the argument m while
the recursion f m n⊲f m (n-1) is not strictly decreasing in m.
Nonetheless, we can verify the program’s termination by using hm, ni as LLRFs off. To do this, we transform the program as follows.
let rec f m (pm, pn) n =assert (( pm > m && m >= 0)|| ( pm >= m && pn > n && n >= 0))
let (pm, pn) = (m, n) in
let r = ∗int in
if r > 0 && m > 0 then f (m-1) (pm, pn) nelse if r <= 0 && n > 0 then f m (pm, pn) (n-1)
else ()
let main s () = f ∗int s ∗int
The underlines highlight the main differences from the transformation described in themain body of the paper. Firstly, the “not decreasing” condition pm >= m of the firstranking function m is added as the condition guarding the second ranking function (i.e.,pn > n && n >= 0). Secondly, the state (pm, pn) is deterministically updated
at the beginning the body of f. The reachability checker will find that the program isassertion safe, and we have verified the program’s termination.

G Further Description of Benchmark Programs– indirectIntro is P1 from Section 1. That is, it is indirect from Example 2
and 4 but without the simplification. We show the code below.
let rec app f x u =if x>0 then app f (x-1) u else f x u
let id u = ()let rec g x = if x <= 0 then id else app g x
let main () = g ∗int ()– indirect is from Example 2 and 4.
– indirectHO is from Section 3.4.
– CE-0CFA is the program below.

let id x = x
let rec omega x = omega x
let f x y z = y z
let main () = f (f id omega) id 1
The program is from [29], given as an example on which both 0CFA and treeautomata-based size-change analysis fails. CE-1CFA is its variant obtained bywrapping each function with an apply function so that 1-limited CFA [29] also
fails. See also the discussion in Section 5.
– up down is the program below.
let rec app f x = f x
and down x = if x = 0 then () else down (x-1)
and up x = if x = 0 then () else up (x+1)
let main () =let t1 = ∗int in let t2 = ∗int in
if t1 > 0 then app down t1
else if t2 < 0 then app up t2 else ()The program cannot be verified by 0CFA-based size-change analysis because up
and down are both passed to the first argument of f and the analysis cannot distinguish the two functions.
– churchNum is the program below, which is based on the example given in Section 7.1 of [12].
let succ m s z = m s (s z)
let id x = x
let two f z = f (f z)
let zero f z = z
let main () = two succ zero id 0
– CE-Jones Bohr is the following program.
let f1 u c d = d
let f2 u a b = a (f1 u)
let f3 u a = a (f2 u a)let f4 u v = v
let f5 u e = e (f4 u)
let main () = let zz = f3 u (f5 u) in ()The program is the λ-lifting of (λa.a(λb.a(λcd.d)))(λe.e(λf.f )), which is given
in Section 7.8 of [12] and is used to show a limitation of their approach.
– map is the program below, which is based on the example given in Section 3.1.1 of[28].
let rec map f xs =if xs = 0 then 0
else f ∗int + map f (xs - 1)

let compose f g x = f (g x)
let add x y = x + y
let main () =let l = ∗int in
if l >= 0 then map (compose (add 1) (add 2)) l else 0– toChurch is the program below.
let compose f g x = f (g x)
let id x = x
let succ x = x + 1
let rec toChurch n f =if n = 0 then id
else compose f (toChurch (n - 1) f)
let main () =let x = ∗int in
if x>=0 then let tos = toChurch x succ in ()else ()The program is given in Section 4.1 of [28] as an example whose dynamic callgraph includes closures of unbounded depth.
– x plus 2ˆn is the following program given in [12], Section 7.2.
let succ n = n + 1
let g r a = r (r a)let rec f n = if n=0 then succ else g (f (n-1))
let main () =let n = ∗int in
let x = ∗int in
if n>=0 && x>=0 then f n x else 0– foldr is the program below, which is based on the example given in Section 4.4.4of [28].
let rec foldr h e l =if l = 0 then eelse h ∗int (foldr h e (l-1))
let sum m n = m + n
let main () =let l = ∗int in
if l >= 0 then foldr sum ∗int l else 0