Predicate Abstraction and CEGAR for
Disproving Termination of Higher-order
Functional Programs
Takuya Kuwahara1 , Ryosuke Sato2 , Hiroshi Unno3 , and Naoki Kobayashi2
1

Knowledge Discovery Research Laboratories, NEC, kuwahara@me.jp.nec.com
2
The University of Tokyo, {ryosuke,koba}@kb.is.s.u-tokyo.ac.jp
3
University of Tsukuba, uhiro@cs.tsukuba.ac.jp

Abstract. We propose an automated method for disproving termination of higher-order functional programs. Our method combines higherorder model checking with predicate abstraction and CEGAR. Our predicate abstraction is novel in that it computes a mixture of under- andoverapproximations. For non-determinism of a source program (such as
random number generation), we apply underapproximation to generate
a subset of the actual branches, and check that some of the branches in
the abstract program is non-terminating. For operations on infinite data
domains (such as integers), we apply overapproximation to generate asuperset of the actual branches, and check that every branch is nonterminating. Thus, disproving non-termination reduces to the problemof checking a certain branching property of the abstract program, which
can be solved by higher-order model checking. We have implemented a
prototype non-termination prover based on our method and have confirmed the effectiveness of the proposed approach through experiments.

1

Introduction

We propose an automated method for disproving termination of higher-orderfunctional programs (i.e., for proving that a given program does not terminate forsome input). The method plays a role complementary to the automated method
for proving termination of higher-order programs (i.e., for proving that a given
program terminates for all inputs) [18]. Several methods have recently been proposed for proving non-termination of programs [7–9, 11, 13, 14, 19], but most ofthem have focused on first-order programs (or, while programs) that can be represented as finite control graphs. An exception is work on term rewriting systems(TRS) [9, 11]; higher-order programs can be encoded into term rewriting systems,
but the definition of non-termination is different: TRS is non-terminating if there
exists a term that has a non-terminating rewriting sequence, not necessarily the
initial term.
Our approach is based on a combination of higher-order model checking [15,21] with predicate abstraction and CEGAR (counterexample-guided abstraction
refinement). Values of a base type (such as integers) are abstracted to (tuples

of) Booleans by using predicates, and higher-order functions are abstracted accordingly. Higher-order model checking is then used to analyze the abstracted
program. A combination of predicate abstraction and higher-order model checking has been previously proposed for verifying safety properties of higher-orderprograms (i.e., for proving that a program does not reach an error state in all
execution paths) [16]. With respect to that work, the approach of the present
paper is novel in that we combine over approximation and under approximation.
Note that predicate abstraction [3, 12, 16] usually yields an overapproximation,i.e., an abstract program that contains a superset of possible execution paths ofthe original program. With such an abstraction, non-termination of the abstract
program (the existence of a non-terminating path) does not imply that of theoriginal program. To address this problem, we use both under- and overapproximations. For a deterministic computation step of the original program, we apply
overapproximation but check that every branch of the overapproximation has a
non-terminating path. For a non-deterministic branch of the original program(such as random number generation and an input from the environment), weapply under -approximation, and check that some branch of the underapproximation has a non-terminating path.
Figure 1 illustrates how under- and overapproximations are combined. The
program considered here is of the form:
let x = ∗ in let y = x + 1 in let z = ∗ in · · · .
Here, ∗ generates a random integer. Thus, the program has the execution tree
shown on the top of Figure 1. The first and third steps are non-deterministic,
while the second step (corresponding to y = x+1) is deterministic. Suppose thatthe predicates used for abstracting the values of x, y, and z are x > 0, y > 0, and0 ≤ z < x + y (these predicates do not necessarily yield a good abstraction, but
are sufficient for explaining the combination of under- and overapproximations).
Then, the abstract program has the execution tree shown on the bottom of the
figure. Due to the predicate abstraction, the infinitely many branches on thevalue of x have been replaced by two branches x > 0 and ¬x > 0. The node
∃ means that only one of the branches needs to have an infinite path (for theoriginal program having a non-terminating path). The deterministic path fromx = n to y = n + 1 has now been replaced by non-deterministic branches y > 0
and ¬y > 0. The node ∀ indicates that every child of the node must have an
infinite path. Below the node x > 0, however, we do not have a node for ¬y > 0,
as x > 0 and y = x + 1 imply y > 0. The infinite branches on z have been
replaced by non-deterministic branches on ¬(0 ≤ z < x + y) or 0 ≤ z < x + y.
As is the case for x, the branches are marked by ∃, meaning that one of the
branches needs to have an infinite path. Note that below the node ¬x > 0, weonly have a branch for ¬(0 ≤ z < x + y). This is because, when x ≤ 0, there
may be no z that satisfies 0 ≤ z < x + y; so, even if there may be an infinite
execution sequence along that path, we cannot conclude that the source program
is non-terminating. Thus, this part of the tree provides an under -approximationof the source program.

Before abstraction:···x = −1

x=0

x=1

y=0

y=1

y=2

···

··· z = 0 ··· ··· z = 0 ··· ··· z = 0 ···
···

···
∃

After abstraction:···¬x > 0

x>0

∀

∀
y>0

¬y > 0

y>0

∃

∃

∃
¬(0 ≤ z < x + y) ¬(0 ≤ z < x + y)···¬(0 ≤ z < x + y) 0 ≤ z < x + y

···
···
···
Fig. 1. Execution trees before/after abstraction

An abstract program is actually represented as a tree-generating programthat generates an execution tree like the one shown on the bottom of Figure 1.
Higher-order model checking is then used for checking, informally speaking, thatevery child of each ∀-node has a non-terminating path, and that some child ofeach ∃-node has a non-terminating path.
The use of overapproximation for disproving termination has also been proposed recently by Cook et al. [8]. Although their theoretical framework is general,
their concrete method for automation is limited to first-order programs. They
also propose a restricted form of combination of underapproximation and overapproximation, but underapproximation can be followed by overapproximation,
but not vice versa.
The rest of this paper is structured as follows. Section 2 defines the language used as the target of our verification. Sections 3 and 4 describe predicate
abstraction and CEGAR respectively. Section 5 reports experiments. Section 6
discusses related work and Section 7 concludes the paper.

2

LanguageIn this section, we introduce the language of source programs, used as the target
of non-termination verification. It is a simply typed, call-by-value higher-orderfunctional language. Throughout the paper, we often use the following abbrevi-P (programs) := {fi xei = ei }i∈{1...n}e (expressions) := ( ) | y ve | if a then e1 else e2| let x = a in e | let x = *int in ea (simple expressions) ::= x | n | op (ea)
v (values) := n | y ve
f x
e=e∈P

|e
x| = |ev|

f ve −→P [e
v /e
x] e

[[a]] = n
let x = a in e −→P [n/x] e

if n then e0 else e1 −→P e0 if n 6= 0

let x = *int in e −→P [n/x] e

if 0 then e0 else e1 −→P e1

Fig. 2. The syntax and operational semantics of the language

ations: ee for a possibly empty sequence e1 , . . . , en , and {ei }i∈{1,...,n} for the set{e1 , . . . , en }.
The syntax and operational semantics of the language is given in Figure 2.
The meta-variable fi ranges over a set of function names, and x, y range over theset of function names and ordinary variables. The meta-variable n ranges overthe set of integers, and op over a set of integer operations. We omit Booleans
and regard a non-negative integer as true, and 0 as false. We require that y ve
in the definition of e is a full application, i.e., that all the necessary arguments
are passed to y, and y ve has a base type. In contrast, y ve in the definition of v
is a partial application. Whether y ve is a full or partial application is actually
determined by the simple type system mentioned below.
The expression let x = *int in e randomly generates an integer, binds x toit, and evaluates e. The meanings of the other expressions should be clear. A
careful reader may notice that we have only tail calls. This is for the simplicity ofthe presentation. Note that it does not lose generality, because we can apply thestandard continuation-passing-style (CPS) transformation to guarantee that all
the function calls are in this form. We assume that for every program {fi xei =ei }i∈{1...n} , main ∈ {f1 , . . . , fn }.
We assume that programs are simply-typed. The syntax of types is given by:τ ::= int | ? | τ1 → τ2 . The types int and ? describe integers and the unit value( ) respectively. The type τ1 → τ2 describes functions from τ1 to τ2 . The typing
rules for expressions and programs are given in the full version [17], which arestandard except that the body of each function can only have type ?. This does
not lose generality since the CPS transformation guarantees this condition.
The one-step reduction relation e1 −→P e2 is defined by the rules in Fig. 2,
where [[a]] stands for the value of the simple expression a. A program P is nonterminating if there is an infinite reduction sequence main →− P e1 →− P e2 →− P . . ..

3

Predicate Abstraction

3.1

Target Language

The target language of predicate abstraction is a higher-order simply-typed
functional language having Booleans and special tree constructors as primitives. The syntax is given in Figure 3. We assume that for every programD (programs) := {fi xei = Mi }i∈{1...n}M (expressions) := c(M1 , . . . , Mk ) | y Ve | let x = (b1 , . . . , bk ) in M
| br∀ {ψ1 → M1 , . . . , ψk → Mk } | br∃ {ψ1 → M1 , . . . , ψk → Mk }b (Booleans) ::= true | false
V (values) ::= (b1 , . . . , bk ) | y Ve
ψ (Boolean expressions) ::= b | #i (x) | ψ1 ∨ ψ2 | ¬ψ
E[f V1 · · · Vk ] −→D E[[V1 /x1 , . . . , Vk /xk ]M ] if f x1 · · · xk = M ∈ D
E[let x = (b1 , . . . , bk ) in M ] −→D E[[(b1 , . . . , bk )/x]M ]E[br∀ {ψ1 → M1 , . . . , ψk → Mk }] −→D E[br∀ (Mi1 , . . . , Mi` )]if {ψi | i ∈ {1, . . . , k} , [[ψi ]] = true} = {ψi1 , . . . , ψi` }E[br∃ {ψ1 → M1 , . . . , ψk → Mk }] −→D E[br∃ (Mi1 , . . . , Mi` )]if {ψi | i ∈ {1, . . . , k} , [[ψi ]] = true} = {ψi1 , . . . , ψi` }E (evaluation contexts) ::= [ ] | c(M1 , . . . , Mi−1 , E, Mi+1 , . . . , Mn )Fig. 3. The syntax and semantics of the target language{fi x
ei = Mi }i∈{1...n} , main ∈ {f1 , . . . , fn }. Each expression generates a possibly
infinite tree, describing possible executions of a source program. The expressionc(M1 , . . . , Mk ) generates a node labeled with c, having the trees generated by
M1 , . . . , Mk as its children. Here, c ranges over the set {end, call, br∀ , br∃ } oftree constructors. The constructors end and call have arities 0 and 1 respectively, while br∀ and br∃ may have arbitrarily many children. We just write
end for end(). The expression let x = (b1 , . . . , bk ) in M binds x to the tuple (b1 , . . . , bk ), and evaluates M . The expression br∀ {ψ1 → M1 , . . . , ψk → Mk }(br∃ {ψ1 → M1 , . . . , ψk → Mk }, resp.) generates the node br∀ (br∃ , resp.), andadds the tree generated by Mi as a child of the node if ψi evaluates to true, where
the order of children does not matter. The Boolean expression #i x denotes the ith element of the tuple x. For example, let x = (true, false) in br∀ {#1 (x) →end, #2 (x) → call(call(end)), #1 (x)∨#2 (x) → call(end)} generates the tree:
br∀
end

call
end

The formal semantics is given through the reduction relation M −→D M 0 ,defined in Figure 3. The tree generated by a program D, written Tree(D), is
the “limit” of the trees obtained from a (possibly infinite) reduction sequencemain −→D M1 −→D M2 −→D · · ·. For example, the program {main = call(main)}generates an infinite (linear) tree consisting of infinitely many call nodes.
Intuitively, the tree generated by a program of the target language describes
possible execution sequences of a source program. The property that a source
program has a non-terminating execution sequence is transformed to the prop-erty of the tree that (i) every child of each br∀ node has an infinite path, and(ii) some child of each br∃ node has an infinite path. More formally, the set of(infinite) trees that represent the existence of a non-terminating computation is
the largest set NonTermTrees such that for every T ∈ NonTermTrees, Tsatisfies one of the following conditions.
1. T = call(T 0 ) and T 0 ∈ NonTermTrees
2. T = br∀ (T1 , . . . , Tk ) and Ti ∈ NonTermTrees for all i ∈ {1, . . . , k}.
3. T = br∃ (T1 , . . . , Tk ) and Ti ∈ NonTermTrees for some i ∈ {1, . . . , k}.
The property above can be expressed by MSO (the monadic second order logic;
or equivalently, modal µ-calculus or alternating parity tree automata); thus
whether the tree generated by a program of the target language belongs to
NonTermTrees can be decided by higher-order model checking [15, 21].
3.2

Abstraction

We now formalize predicate abstraction for transforming a source program toa program (of the target language) that generates a tree that approximately
represents the possible execution sequences of the source program. Following
Kobayashi et al. [16], we use abstraction types for expressing which predicate
should be used for abstracting each value. The syntax of abstraction types is:σ (abstraction types) ::= ? | int[Q1 , . . . , Qk ] | x : σ1 → σ2
Q (predicates) ::= λx.ϕ
ϕ ::= n1 x1 + · · · + nk xk ≤ n | ϕ1 ∨ ϕ2 | ¬ϕ
The type ? describes the unit value, and int[Q1 , . . . , Qk ] describes an integer thatshould be abstracted by using the predicates Q1 , . . . , Qk . For example, given an
abstraction type int[λx.x ≤ 1, λx.2x − 1 ≤ 0], the integer 1 is abstracted to(true, false). In the syntax above, we list only linear inequalities as primitive
constraints, but we can include other constraints (such as those on uninterpreted function symbols) as long as the underlying theory remains decidable.
The type x : σ1 → σ2 describes a function whose argument and return value
should be abstracted according to σ1 and σ2 respectively. In σ2 , the argument
can be referred to by x if x has an integer type int[Q1 , . . . , Qk ]. For example,
x : int[λx.x ≤ 0] → int[λy.y − x ≤ 0] describes a function from integers to integers whose argument should be abstracted using the predicate λx.x ≤ 0 andwhose return value should be abstracted using λy.y − x ≤ 0. Thus, the successor function (defined by f x = x + 1) will be abstracted to a Boolean function
λb.false (because the return value x + 1 is always greater than x, no matter
whether x ≤ 0 or not).
The predicate abstraction for expressions and programs is formalized using
the relations Γ ` e : σ
M and ` P : Γ
D, where Γ , called an abstraction
type environment, is of the form x1 : σ1 , . . . , xn : σn . Intuitively, Γ ` e : σMmeans that under the assumption that each free variable xi of e is abstracted
according to σi , the expression e is abstracted to M according to the abstractionΓ ` () : ?

(PA-Unit)end|= b1 Q1 (a) ∧ · · · ∧ bk Qk (a) ⇒ θΓ ψ(b1 ,...,bk ) (for each b1 , . . . , bk ∈ {true, false})
Γ, x : int[Q1 , . . . , Qk ] ` e : ?
MΓ ` let x : int[Q1 , . . . , Qk ] = a in e : ?
br∀ ψ(b1 ,...,bk ) → let x = (b1 , . . . , bk ) in M | b1 , . . . , bk ∈ {true, false}(PA-Sexp)|= x 6= 0 ⇒ θΓ ψ1|= x = 0 ⇒ θΓ ψ2
Γ ` e1 : ?
M1Γ ` e2 : ?
M2Γ ` if x then e1 else e2 : ?

br∀ {ψ1 → M1 , ψ2 → M2 }(PA-If)|= θΓ ψ(b1 ,...,bk ) ⇒ ∃x.b1 Q1 (x) ∧ · · · ∧ bk Qk (x) (for each b1 , . . . , bk ∈ {true, false})
Γ, x : int[Q1 , . . . , Qk ] ` e : ?
MΓ ` let x : int[Q1 , . . . , Qk ] = *int in e : ?
br∃ ψ(b1 ,...,bk ) → let x = (b1 , . . . , bk ) in M | b1 , . . . , bk ∈ {true, false}(PA-Rand)Γ (y) = x1 : σ1 → · · · → xk : σk → σΓ ` vi : [v1 /x1 , . . . , vi−1 /xi−1 ]σi
Vi for each i ∈ {1, . . . , k}
(PA-App)Γ ` y v1 · · · vk : [v1 /x1 , . . . , vk /xk ]σy V1 · · · Vk{fi : xe:σei → ?}i∈{1,...,k} , xe:σej ` ei : ?

Mi for each j ∈ {1, . . . , k}

` {fi xei = ei }i∈{1,...,k} : {fi : xe:σei → ?}i∈{1,...,k}{fi xei = call(Mi )}i∈{1,...,k}(PA-Prog)

Fig. 4. Predicate Abstraction Rules

type σ. In the judgment ` P : Γ
D, Γ describes how each function defined in
P should be abstracted.
The relations are defined by the rules in Figure 4. Here, we consider, without
loss of generality, only if-expressions of the form if x then e1 else e2 . Also,
function arguments are restricted to the syntax: v ::= y ve. (In other words,
constants may not occur; note that x c can be replaced by let y = c in x y.)
We assume that each let-expression is annotated with an abstraction type thatshould be used for abstracting the value of the variable. Those abstraction types,
as well as those for functions are automatically inferred by the CEGAR procedure described in Section 4.
The rule PA-Unit just replaces the unit value with end, which represents
termination. The rule PA-Sexp overapproximates the value of a simple expression a. Here, θΓ is the substitution that replaces each variable x of typeint[Q01 , . . . , Q0n ] in Γ with (Q01 (x), . . . , Q0n (x)). For example, if Γ = x:int[λx.x ≤0, λx.x ≤ 2], y : int[λy.y ≤ x], then θΓ (#2 (x) ∧ #1 (y)) is #2 (x ≤ 0, x ≤2) ∧ #1 (y ≤ x), i.e., x ≤ 2 ∧ y ≤ x. The formula bi Qi (a) stands for Qi (a) if
bi = true, and ¬Qi (a) if bi = false. Basically, the rule generates branches
for all the possible values (b1 , . . . , bk ) for (Q1 (a), . . . , Qk (a)), and combines themwith node br∀ (which indicates that this branch has been obtained by an overapproximation). To eliminate impossible values, we compute a necessary condition
ψ(b1 ,...,bk ) for (Q1 (a), . . . , Qk (a)) = (b1 , . . . , bk ) to hold, and guard the branch for(b1 , . . . , bk ) with ψ(b1 ,...,bk ) . The formula ψ(b1 ,...,bk ) can be computed by using an
SMT solver, as in ordinary predicate abstraction [3, 16]. (The rule generates 2k
branches, leading to code explosion. This is for the sake of simplicity; the eager
splitting of branches is avoided in the actual implementation.) The rule PA-If
is similar: branches for the then- and else-clauses are generated, but they are
guarded by necessary conditions for the branches to be chosen.
The rule PA-Rand for random number generation is a kind of dual to
PA-SExp. It applies an underapproximation, and generates branches for all thepossible values (b1 , . . . , bk ) for (Q1 (x), . . . , Qk (x)) under the node br∃ . Eachbranch is guarded by a sufficient condition for the existence of a value for x
such that (Q1 (x), . . . , Qk (x)) = (b1 , . . . , bk ), so that for each branch, there must
be a corresponding execution path of the source program. The rule PA-App
for applications is the same as the corresponding rule of [16]. Finally, the rule
PA-Prog for programs just transforms the body of each function definition, but
adds a special node call to keep track of function calls. Note that a program is
non-terminating if and only if it makes infinitely many function calls.
Example 1 Let us consider the following program LOOP.
loop h x =let b = (x > 0) in
if b then let d = *int in let y = x + d in h y (loop app) else ( )app m k =k m

main = let r = *int in loop app r

LOOP is non-terminating; in fact, if *int is always evaluated to 1, then wehave:main −→∗ loop app 1 −→∗ app 2 (loop app) −→∗ loop app 2 −→∗ · · ·Let ΓLOOP be an abstraction type environment:
loop : (int[λν.ν > 1] → (int[λν.ν > 1] → ?) → ?) → int[λν.ν > 1] → ?
app : int[λν.ν > 1] → (int[λν.ν > 1] → ?) → ?
By using ΓLOOP and the following abstraction types for b, d, and r:
b : int[λν.ν 6= 0], d : int[λν.x + ν > 1], r : int[λν.ν > 1],
the program LOOP is abstracted to the following program DLOOP .
loop h x = call(br∀ {true → let b = true in M1 ,¬x → let b = false in M1 })app m k = call(k m)main = call(br∃ {true → let r = true in loop app r,
true → let r = false in loop app r})
where
M1 = br∀ {b → M2 , ¬b → end}
M2 = br∃ {true → let d = true in M3 , true → let d = false in M3 }M3 = br∀ {d → let y = true in h y (loop app),¬d → let y = false in h y (loop app)}.

For example, let b : int[λν.ν 6= 0] = x > 0 in e is transformed by PA-Sexp
as follows:|= (x > 0) 6= 0 ⇒ true|= ¬((x > 0) 6= 0) ⇒ ¬(x > 1)(= θΓ (¬x))Γ, b : int[λν.ν = 0] ` e : ?
M1
Γ ` let b : int[λν.ν = 0] = x > 0 in ebr∀ {true → let b = true in M1 , ¬x → let b = false in M1 }where
Γ = ΓLOOP , h : (int[λν.ν > 1] → (int[λν.ν > 1] → ?) → ?), x : int[λν.ν > 1].
Here, recall that a non-zero integer is treated as true in the source language;thus, ¬((x > 0) 6= 0) means x ≤ 0. Since Tree(DLOOP ) ∈ NonTermTrees, we
can conclude that the program LOOP is non-terminating (based on Theorem 1
below).
tu
The soundness of predicate abstraction is stated as follows (see the full version [17] for a proof).
Theorem 1. Suppose ` P : Γ
non-terminating.

4

D. If Tree(D) ∈ NonTermTrees, then P is

Counterexample-Guided Abstraction Refinement(CEGAR)

This section describes our CEGAR procedure to refine abstraction based on acounterexample. Here, a counterexample output by a higher-order model checker
is a finite subtree T of Tree(D), obtained by removing all but one branches ofeach br∀ node. Figure 5 illustrates Tree(D) and a corresponding counterexample(showing Tree(D) 6∈ NonTermTrees). In the figure, “· · ·” indicates an infinite
path. For each br∀ node, a model checker picks one branch containing a finite
path, preserving the branches of the other nodes (br∃ , call, and end).

br∃
br∀
···

end

br∃
br∀

···

end

br∀ br∀end

end

Fig. 5. Tree(D) (left) and a corresponding counterexample (right)

We analyze each path of the counterexample tree to infer new abstraction
types for refining abstraction. To that end, we need to distinguish between two
types of paths in the counterexample tree: one that has been introduced due

Type I

Type IIif...

overapproximation

()

...

br

*

br
underapproximation

br
end

...

()

...

end

Fig. 6. Two types of paths in a counterexample

to overapproximation, and the other due to underapproximation. Figure 6 illustrates the two types. For each type, the lefthand side shows the computation
tree of a source program, and the righthand side shows the tree generated by
the abstract program. Thick lines show a path of a counterexample tree. In theexample of Type I, the computation of a source program takes the then-branch
and falls into a non-terminating computation, but predicate abstraction has introduced the spurious path taking the else branch, which was detected as apart of the counterexample. In the example of Type II, a source program generates a random number and non-deterministically branches to a non-terminating
computation or a terminating computation. After predicate abstraction, the two
branches by the random number generation have been merged; instead, the next
deterministic computation step has been split into two by an overapproximation.
This situation occurs, for example, for
let x : int[ ] = *int in let y : int[λy.y 6= 0] = x in if y then loop() else ().
The program generated by the abstraction isbr∃ {true → br∀ {true → let y = true in · · ·,true → let y = false in · · ·}}.
Thus, the branches at *int in the original program have been moved to thebranches at br∀ . The classification of the paths of a counterexample into Type I
or II can be performed according to the feasibility of the path, i.e., whether there
is a corresponding computation path in the source program. An infeasible path
is Type I, since it has been introduced by an overapproximation, and a feasible
path is Type II; it has a corresponding computation path, but the two kinds ofnon-determinism (expressed by br∃ and br∀ ) have been confused by predicate
abstraction. We need to refine the predicates (or, abstraction types) used foroverapproximation for a Type I path, and those used for underapproximation
for a Type II path. In the example program above, by refining the abstraction
type for x to int[λx.x 6= 0], we obtainbr∃ {true → let x = true in br∀ {x → let y = true in · · ·} ,true → let x = false in br∀ {¬x → let y = false in · · ·}}.
Thus, the branches on terminating/non-terminating paths are moved to the nodebr∃ .

The refinement of abstraction types based on Type I (i.e., infeasible) paths
can be performed in the same way as our previous work [16]. Thus, we focus
below on how to deal with a Type II path.
4.1

Dealing with Type II paths

Given a program P and a Type II path π, we first prepare fresh predicate
variables R1 , . . . , Rk (called separating predicates), and replace each expression
for random number generation let ri = *int in ei with:4
let ri = *int in assume(Ri (ri )); ei .
Here, an expression assume(φ); e evaluates to e only if φ is true. Then, we
instantiate Ri ’s so that the following conditions hold.
(C1) P has no longer an execution path along π.
(C2) If the execution along π reaches let ri = *int in assume(Ri (ri )); ei , there
is at least one value for ri such that Ri (ri ) holds.
Condition C1 is for separating the path π at br∃ node (recall Figure 6; theproblem of a Type II path has been that terminating/non-terminating paths are
merged at br∃ node). Condition C2 ensures that the paths separated from π arenot empty. By C2, for example, an absurd assume statement like assume(false)is excluded out. We then add the instantiations of R1 , . . . , Rk to the abstraction
types for r1 , . . . , rk .
For the example
let x : int[ ] = *int in let y : int[λy.y 6= 0] = x in if y then loop() else ()discussed above, we insert an assume statement as follows.
let x = *int in assume(R(x)); let y = x in if y then loop() else ().
Here, the Type II path π is the one that goes through the else-branch. Thus, acondition R(x) that makes it infeasible is x 6= 0. As a result, λx.x 6= 0 is added
to the abstraction type for x.
We sketch below how to instantiate R1 , . . . , Rk . Using the technique of [16]condition (I) can be reduced to a set of non-recursive Horn clauses over predicate
variables. Condition (II) is, on the other hand, reduced to constraints of the form
R1 (ex1 ) ∧ · · · ∧ Rn (exn ) ∧ C ⇒ ∃x.R(x) ∧ C 0 .
Thus, it remains to solve (non-recursive) existentially quantified Horn clauses [4].
To solve them, we first remove existential quantification by using a Skolemizationbased technique similar to [4]. We prepare a linear template of Skolem function
and move existential quantifiers out of universal quantifiers. For example, given∀r. (∃ν.ν ≤ 1 ∧ R(ν)) ∧ ∀r. (R(r) ∧ ¬(r > 0) ⇒ false) ,4

Actually, we apply the replacement to each instance of let ri = *int in ei along
the execution path π, so that different assume conditions can be used for different
instances of the same expression; we elide the details here.

program
cycle time (msec)
programcycle time (msec)
loopHO2
1,156 unfoldr nonterm 3
13,540indirect e
1
111
passing cond2
9,202
indirectHO e 1112
inf clos2
12,264foldr nonterm 4
20,498 fib CPS nonterm 1
133
alternate1
95 fixpoint nonterm 2
168
Table 1. The result of the first benchmark set

we prepare the linear template c0 + c1 r and transform the constraints into:∃c0 , c1 .∀ν.r. (ν = c0 + c1 r ⇒ ν ≤ 1 ∧ R(ν)) ∧ ∀ (R(r) ∧ ¬(r > 0) ⇒ false) .
We then remove predicate variables by resolution, and get:∀ν.r.ν = c0 + c1 r ⇒ ν ≤ 1 ∧ ν > 0
Finally, we solve constraints in the form of ∃ex.∀ey .φ and obtain coefficients oflinear templates that we introduced in the first step. We adopt the existing constraint solving technique based [24] on Farkas’ Lemma. For the running example,
we obtain c0 = 2, c1 = 0 as a solution of the constraints.
Now that we have removed existential quantification, we are left with nonrecursive Horn clause constraints, which can be solved by using the existing
constraint solving technique [23]. For the example above, we get∀ν.r. (ν = 2 ⇒ ν ≤ 1 ∧ R(ν)) ∧ (R(r) ∧ ¬(r > 0) ⇒ ⊥)and obtain R = λν.ν > 0 as a solution.

5

Implementation and Experiments

We have implemented a non-termination verifier for a subset of OCaml, as anextension of MoCHi [16], a software model checker for OCaml programs. We
use HorSat [5] as the backend higher-order model checker, and Z3 [20] as thebackend SMT solver. The web interface of our non-termination verification tool
is available online [1]. We evaluated our tool by experiments on two benchmark
sets: (1) test cases consisting of higher-order programs and (2) a standard benchmark set on non-termination of first-order programs [7, 19]. Both experiments
were conducted on a machine with Intel Xeon E3-1225 V2 (3.20GHz, 16GB ofmemory) with timeout of 60 seconds. The first benchmark set and an online
demo page are available from our website [1].
Table 1 shows the result of the first evaluation. The columns ‘program’,’cycle’, and ’time’ show the name of each test case, the number of CEGAR
cycles, and the elapsed time (in milliseconds), respectively. For foldr nonterm,
we have used a different mode for a backend constraint solver; with the default
mode, our verifier has timed out. All the programs in the first benchmark set arehigher-order programs; so, they cannot be directly verified by previous tools. Our
tool could successfully verify all the programs to be non-terminating (except that
we had to change the mode of a backend constraint solver for foldr nonterm).
We explain below two of the programs in the first benchmark set: inf closand alternate. The program inf clos is:
succ app f n = f (n + 1)
is zero n = (n = 0)f n cond = let b = cond n in if b then ( ) else f n (succ app cond)main = f *int is zero.
It has the following non-terminating reduction sequence:
main −→∗ f 1 is zero −→∗ f 1 (succ app is zero) −→∗ f 1 (succ app 2 is zero)−→∗ f 1 (succ app m is zero) −→∗ · · · .
Note that succ app m is zero n is equivalent to n+m = 0; hence b in the function
f always evaluates to false in the sequence above. For proving non-termination,
we need to reason about the value of the higher-order argument cond, so theprevious methods for non-termination of first-order programs are not applicable.
The following program alternate shows the strength of our underapproximation.
f g h z = let x = *int in if x > 0 then g (f h g) else h (f h g)proceed u = u ( )halt u = ( )main = f proceed halt ( )It has the following non-terminating reduction sequence:
main −→∗ f proceed halt ( )−→∗ if 1 > 0 then proceed(f halt proceed) else · · · −→∗ f halt proceed ( )−→∗ if − 1 > 0 then · · · else proceed(f proceed halt) −→∗ f proceed halt ( )−→∗ · · · .
Here, since the arguments g and h are swapped for each recursive call, theprogram does not terminate only if positive and negative integers are createdalternately by *int . Thus, the approach of Chen et al. [7] (which underapproximates a program by inserting assume statements and then uses a safety property
checker to prove that the resulting program never terminates) would not be applicable. In our approach, by using the abstraction type int[λx.x > 0] for x, f
is abstracted to:f g h z = br∃ {true → let x = true in br∀ {x → g(f h g)},true → let x = false in br∀ {¬x → h(f h g)}}.
Thus, both branches of the if-expression are kept in the abstract program, andwe can correctly conclude that the program is non-terminating.
For the second benchmark, we have borrowed a standard benchmark set
consisting of 78 programs categorized as “known non-terminating examples” [7,19]. (Actually, the original set consists of 81 programs, but 3 of them turned outto be terminating.) The original programs were written in the input language
for T2 [2]; we have automatically converted them to OCaml programs. Our tool
could verify 48 programs to be non-terminating in the time limit of 60 seconds.
According to Larraz et al. [19], CPPINV [19], T2-TACAS [7], APROVE [6, 10],JULIA [22], and TNT [13] could verify 70, 51, 0, 8, and 19 programs respectively,
with the same limit but under a different environment. Thus, our tool is not the
best, but competitive with the state-of-the-art tools for proving non-terminationof first-order programs, despite that our tool is not specialized for first-orderprograms. As for the comparison with T2-TACAS [7], our tool could verify 7
programs for which T2-TACAS failed, and ours failed for 10 programs that T2TACAS could verify.

6

Related Work

Methods for disproving termination have recently been studied actively [7, 8,
13, 19]. Most of them, however, focused on programs having finite control-flow
graphs with numerical data. For example, the state-of-the-art method by Larraz et al. [19] enumerates a strongly connected subgraph (SCSG), and checks
whether there is a computation that is trapped in the SCSG using a SMT solver.
Thus, it is not obvious how to extend those techniques to deal with recursion
and higher-order functions. Note that unlike in safety property verification, we
cannot soundly overapproximate the infinite control-flow graph of a higher-orderprogram with a finite one.
Technically, the closest to our work seems to be the series of recent workby Cook et al. [7, 8]. They apply an underapproximation by inserting assume
statements, and then either appeal to a safety property checker [7], or apply
an overapproximation [8] to prove that the underapproximated program is nonterminating for all execution paths. A problem of their underapproximation [7]is that when an assume statement assume(P ) is inserted, all the computations
such that ¬P are discarded; so if P is wrongly chosen, they may overlook a nonterminating computation present in the branch where ¬P holds. As in the casefor alternate discussed in Section 5, in the presence of higher-order functions,
there may be no proper way for inserting assume conditions. In contrast, with
our predicate abstraction, given a predicate P , we basically keep both branches
for P and ¬P , and apply an underapproximation only if the satisfiability of P
or ¬P is not guaranteed (recall Figure 1). In Cook et al.’s method [8], underapproximation cannot be applied after overapproximation, whereas under- andoverapproximation can be arbitrarily nested in our method. Furthermore, although the framework of Cook et al. [8] is general, their concrete method can beapplied to detect only non-termination in the form of lasso for programs having
finite control-flow graphs. Harris et al. [14] also combine under- and overapproximation, but in a way different from ours: they use under- and overapproximation
for disproving and proving termination respectively, not both for disproving termination.

There have also been studies on non-termination of term rewriting systems(TRS). Higher-order programs can be encoded into term rewriting systems, but
the resulting analysis would be too imprecise. Furthermore, as mentioned in
Section 1, the definition of non-termination is different.
Higher-order model checking has been recently applied to program verification [15, 16]. Predicate abstraction has been used for overapproximation forthe purpose of safety property verification, but the combination of under- andoverapproximation is new. Kuwahara et al. [18] have proposed a method forproving termination of higher-order programs; our new method for disproving
termination plays a complementary role to that method.
The constraints generated in our CEGAR phase can be regarded as special instances of “existentially quantified Horn clauses” considered by Beyene etal. [4], where only acyclic clauses are allowed. Our constraint solving algorithm
is specialized for the case of acyclic clauses. Incidentally, Beyene et al. [4] usedexistentially quantified clauses for verifying CTL properties of programs. Since
non-termination can be expressed by the CTL formula EG¬terminated , theirtechnique can, in principle, be used for verifying non-termination. Like othermethods for non-termination, however, the resulting technique seems applicable
only to programs with finite control-flow graphs.

7

Conclusion

We have proposed an automated method for disproving termination of higherorder programs. The key idea was to combine under- and overapproximations
by using predicate abstraction. By representing the approximation as a treegenerating higher-order program, we have reduced non-termination verification
to higher-order model checking. The mixture of under- and overapproximations
has also required a careful analysis of counterexamples, for determining whether
and how under- or overapproximations are refined. We have implemented the
proposed method and confirmed its effectiveness. Future work includes optimizations of the implementation and integration with the termination verifier [18].
Acknowledgments We would like to thank Carsten Fuhs for providing us with
their experimental data and pointers to related work, and anonymous referees
for useful comments. This work was partially supported by Kakenhi 23220001
and 25730035.

References
1. MoCHi(Non-termination): Model Checker for Higher-Order Programs. http://
www-kb.is.s.u-tokyo.ac.jp/~kuwahara/nonterm/
2. T2 temporal prover. http://research.microsoft.com/en-us/projects/t2/
3. Ball, T., Majumdar, R., Millstein, T., Rajamani, S.K.: Automatic predicate abstraction of C programs. In: PLDI ’01. pp. 203–213. ACM (2001)

4. Beyene, T.A., Popeea, C., Rybalchenko, A.: Solving existentially quantified hornclauses. In: CAV ’13. LNCS, vol. 8044, pp. 869–882. Springer (2013)
5. Broadbent, C., Kobayashi, N.: Saturation-based model checking of higher-orderrecursion schemes. In: CSL ’13. LIPIcs, vol. 23, pp. 129–148 (2013)
6. Brockschmidt, M., Ströder, T., Otto, C., Giesl, J.: Automated detection of nontermination and NullPointerExceptions for Java bytecode. In: FoVeOOS ’11.
LNCS, vol. 7421, pp. 123–141. Springer (2012)
7. Chen, H.Y., Cook, B., Fuhs, C., Nimkar, K., O’Hearn, P.W.: Proving nontermination via safety. In: TACAS ’14. LNCS, vol. 8413, pp. 156–171. Springer (2014)
8. Cook, B., Fuhs, C., Nimkar, K., O’Hearn, P.W.: Disproving termination with overapproximation. In: FMCAD ’14. pp. 67–74. IEEE (2014)
9. Emmes, F., Enger, T., Giesl, J.: Proving non-looping non-termination automatically. In: IJCAR ’12. LNCS, vol. 7364, pp. 225–240. Springer (2012)
10. Giesl, J., Brockschmidt, M., Emmes, F., Frohn, F., Fuhs, C., Otto, C., Plücker, M.,
Schneider-Kamp, P., Ströder, T., Swiderski, S., Thiemann, R.: Proving terminationof programs automatically with aprove. In: Proceedings of IJCAR 2014. pp. 184–
191 (2014)
11. Giesl, J., Thiemann, R., Schneider-Kamp, P.: Proving and disproving terminationin the dependency pair framework. In: Deduction and Applications. No. 05431 in
Dagstuhl Seminar Proceedings (2006)
12. Graf, S., Saı̈di, H.: Construction of abstract state graphs with PVS. In: CAV ’97.
LNCS, vol. 1254, pp. 72–83. Springer (1997)
13. Gupta, A., Henzinger, T.A., Majumdar, R., Rybalchenko, A., Xu, R.G.: Proving
non-termination. In: POPL ’08. pp. 147–158. ACM (2008)
14. Harris, W.R., Lal, A., Nori, A.V., Rajamani, S.K.: Alternation for termination. In:
Proceedings of SAS ’10. LNCS, vol. 6337, pp. 304–319. Springer (2010)
15. Kobayashi, N.: Model checking higher-order programs. Journal of the ACM 60(3)(2013)
16. Kobayashi, N., Sato, R., Unno, H.: Predicate abstraction and CEGAR for higherorder model checking. In: PLDI ’11. pp. 222–233. ACM (2011)
17. Kuwahara, T., Sato, R., Unno, H., Kobayashi, N.: Predicate abstraction and CEGAR for disproving termination of higher-order functional programs. Full version,
available from the last author’s web page (2015)
18. Kuwahara, T., Terauchi, T., Unno, H., Kobayashi, N.: Automatic termination verification for higher-order functional programs. In: ESOP ’14. LNCS, vol. 8410, pp.
392–411. Springer (2014)
19. Larraz, D., Nimkar, K., Oliveras, A., Rodrı́guez-Carbonell, E., Rubio, A.: Proving
non-termination using max-SMT. In: CAV ’14. LNCS, vol. 8559, pp. 779–796.
Springer (2014)
20. de Moura, L., Bjørner, N.: Z3: An efficient SMT solver. In: TACAS ’08. LNCS,
vol. 4963, pp. 337–340. Springer (2008)
21. Ong, C.H.L.: On model-checking trees generated by higher-order recursion
schemes. In: LICS ’06. pp. 81–90. IEEE (2006)
22. Spoto, F., Mesnard, F., Étienne Payet: A termination analyzer for java bytecode
based on path-length. ACM Trans. Prog. Lang. Syst. 32(3), 8:1–8:70 (Mar 2010)
23. Unno, H., Kobayashi, N.: Dependent type inference with interpolants. In: PPDP
’09. pp. 277–288. ACM (2009)
24. Unno, H., Terauchi, T., Kobayashi, N.: Automating relatively complete verificationof higher-order functional programs. In: POPL ’13. pp. 75–86. ACM (2013)