Predicate Abstraction and CEGAR
for Higher-Order Model Checking
Naoki Kobayashi

Ryosuke Sato

Hiroshi Unno

Tohoku University
koba@ecei.tohoku.ac.jp

Tohoku University
ryosuke@kb.ecei.tohoku.ac.jp

Tohoku University
uhiro@kb.ecei.tohoku.ac.jp

Abstract
Higher-order model checking (more precisely, the model checking of higher-order recursion schemes) has been extensively studied recently, which can automatically decide properties of programs written in the simply-typed λ-calculus with recursion andfinite data domains. This paper formalizes predicate abstraction
and counterexample-guided abstraction refinement (CEGAR) for
higher-order model checking, enabling automatic verification ofprograms that use infinite data domains such as integers. A prototype verifier for higher-order functional programs based on the formalization has been implemented and tested for several programs.
Categories and Subject Descriptors D.2.4 [Software Engineering]: Software/Program Verification; F.3.1 [Logics and Meanings
of Programs]: Specifying and Verifying and Reasoning about Programs
General Terms Languages, Reliability, Verification
Keywords Predicate Abstraction, CEGAR, Higher-Order Model
Checking, Dependent Types

1.

Introduction

The model checking of higher-order recursion schemes (recursion schemes, for short) has been extensively studied [19, 24, 28],
and recently applied to verification of functional programs [20,22, 26]. Recursion schemes are grammars for describing infinite
trees [19, 28], and the recursion scheme model checking is concerned about whether the tree generated by a recursion scheme
satisfies a given property. It can be considered an extension of finite state and pushdown model checking, where the model checking of order-0 and order-1 recursion schemes respectively correspond to finite state and pushdown model checking. From a programming language point of view, a recursion scheme is a termof the simply-typed, call-by-name λ-calculus with recursion andtree constructors, which generates a single, possibly infinite tree.
Various verification problems for functional programs can be easily reduced to recursion scheme model checking problems [20, 22,26]. Thanks to the decidability of recursion scheme model checking [28], the reduction yields a sound, complete, and automaticc ACM, 2011. This is the author’s version of the work. It is posted here by permissionof ACM for your personal use. Not for redistribution. The definitive version was
published in the Proceedings of PLDI’11.

verification method for programs written in the simply-typed λcalculus with recursion and finite data domains (such as booleans).
There is, however, still a large gap between the programs handled by the above-mentioned method and real functional programs.
One of the main limitations is that infinite data domains such as
integers and lists cannot be handled by the recursion scheme model
checking. To overcome that limitation, this paper extends the techniques of predicate abstraction [12] and counterexample-guided abstraction refinement (CEGAR) [4, 8] for higher-order model checking (i.e., recursion scheme model checking).
The overall structure of our method is shown in Figure 1. Givena higher-order functional program, predicate abstraction is first applied to obtain a higher-order boolean program (Step 1 in Figure 1).
For example, consider the following program M1 :let f x g = g(x+1) in let h y = assert(y>0) in
let k n = if n>0 then f n h else () in k(randi())
Here, assert takes a boolean as an argument and is reduced to
fail if the argument is false. The function randi returns a nondeterministic integer value. Using a predicate λx.x > 0, we obtainthe following higher-order boolean program e1 :let f b g = if b then g(true) else g(randb()) in
let h c = assert(c) in
let k () = if randb() then f true h else () in k()
Here, randb returns a non-deterministic boolean value. Note thatthe integer variables x and y have been replaced by the boolean
variable b and c respectively, which represents whether the valuesof x and y are greater than 0. In the abstract version of f, b beingtrue means that x>0, which implies x+1>0, so that true is passed tog in the then-part. In the else-part, x<=0, hence x+1>0 may or may
not hold, so that a non-deterministic boolean value is passed to g.
The higher-order boolean program thus obtained is an abstractionof the source program; for any reduction sequence of the source
program, there is a corresponding reduction sequence of the higherorder boolean program (but not vice versa). Thus, for example, if
the abstract program does not cause an assertion failure, neither
does the source program.
The higher-order boolean program is then represented as a recursion scheme and model-checked by using an existing recursion
scheme model checker [21, 22] (Step 2 in Figure 1). If the higherorder boolean program satisfies a given safety property,1 the source
program is also safe. Otherwise, an error path of the boolean program is inspected (Step 3 in Figure 1). If it is also an error pathof the source program, then it is reported that the program is unsafe. Otherwise, new predicates are extracted from the error path,in order to refine predicate abstraction (Step 4 in Figure 1).
1 For the sake of simplicity, throughout the paper, we only consider thereachability property.

be abstracted by using λν.ν > 0, rather than λν.ν ≥ 0. We use
types (called abstraction types) to express which predicate should
be used for each variable. For example, for the above program, thefollowing abstraction types are assigned to f , h, and k:

Functional
Program

Step 1: Predicate
Abstraction(Section 4)

Abstraction
Types

Step 4: Predicate
Discovery(Section 5.2)

BooleanPrograminfeasible
Step 2: Higher-Order
Model Checking(Section 3)
OK
safe

NG

Error Trace

Step 3: Feasibility
Check(Section 5.1)
feasible
unsafeFigure 1. Higher-Order Model Checking with Predicate Abstraction and CEGAR

f : int[λν.ν ≥ 0] → (int[λν.ν > 0] → ) → 
h : int[λν.ν > 0] → 
k : int[ ] → 
The type of f means that the first argument of f should be an
integer abstracted by the predicate λν.ν ≥ 0, and the second
argument be a function that takes an integer abstracted by thepredicate λν.ν > 0 as an argument and returns a unit value.2
By using these abstraction types, the problem of checking thatpredicates are consistently used boils down to a type checking
problem. For example, the standard rule for application:Γ  M : τ1 → τ2
Γ  N : τ1
Γ  M N : τ2
ensures that N is abstracted using the predicates expected by thefunction M ; there is no such case that an abstraction of function
M expects a value abstracted by using the predicate λν.ν > 0 but
the actual argument N is abstracted by using λν.ν ≥ 0.
A further twist is necessary to deal with multi-ary predicates.
For example, consider the following modified version M3 :In the example above, we actually start predicate abstraction
with the empty set of predicates, and obtain the following abstract
program e0 :let f x g = g(x+1) in let h z y = assert(y>z) in
let k n = if n>=0 then f n (h n) else () ink(randi())

let f g = g() in let h () = assert(randb()) in
let k () = if randb() then f h else () in k()

The variable y should now be abstracted by using λν.ν > z, which
depends on the value of z. Thus, the above program should be
abstracted by using the following dependent abstraction types:

The model checking of this program yields the following reduction
sequence, leading to an assertion failure:k() −→ if randb() then f h else ()−→ if true then f h else () −→ f h−→ h() −→ assert (randb())−→ assert (false) −→ fail· · · (1)The corresponding reduction sequence in the source program M1is:k n −→ if n>0 then f n h else () −→n>0 f n h−→ h(n+1) −→ assert (n+1>0) −→n+1<=0 fail · · · (2)Here, n is some integer, and we have annotated the sequence withthe conditions that should hold at each step. As n>0 ∧ n+1<=0
is unsatisfiable, we know that the reduction sequence above isactually infeasible, so that the source program may not cause an
assertion failure. From the unsatisfiable constraint above, we canlearn that information about whether an integer is positive is useful.
By using it, we get the refined abstract program shown earlier. As
the new abstract program is safe (i.e. does not cause an assertion
failure), we can conclude that the source program is also safe.
The idea sketched above is basically the same as the techniques
for predicate abstraction and CEGAR used already in finite stateand pushdown model checking [4, 8], except that models have been
replaced by higher-order boolean programs (or recursion schemes).
As discussed below, however, it turned out that there are many
challenging problems in developing effective methods for predicate
abstraction and CEGAR for higher-order model checking.
First, for predicate abstraction, it is unreasonable to use thesame set of predicates for all the integer variables. For example,
let us modify the program above into the following program M2 :let f x g = g(x+1) in let h y = assert(y>0) in
let k n = if n>=0 then f n h else () in k(randi())
Then, the predicate λν.ν ≥ 0 should be used for x, while λν.ν > 0
should be used for y. We should consistently use predicates; for example, with the choice of the predicates above, g’s argument shouldf : (x : int[ ] → (w : int[λν.ν > x] → ) → )h : (z : int[ ] → y : int[λν.ν > z] → )k : int[ ] → Here, please note that the types of the second arguments of f andh refer to the values of the first arguments. Thus, our type systemfor ensuring the consistency of predicates is actually a dependentone. A predicate abstraction algorithm is then formalized as a typedirected transformation relation Γ  M : τ ⇒ e based on thedependent abstraction type system, where M is a source programand e is an abstract program.3
The predicate abstraction mentioned above is sound in the sensethat if an abstract program is safe (i.e., does not reach fail), so
is the source program. Further, we can show that it is relatively
complete with respect to a dependent (refinement) intersection typesystem [32]: If a source program is typable in the dependent intersection type system, our predicate abstraction can generate a safe
abstract boolean program by using certain abstraction types. Thismeans that, as long as suitable predicates are provided (by a user oran automated method like the CEGAR discussed below), the combination of our predicate abstraction and higher-order model checking has at least the same verification power as (and actually strictly
more expressive than, as discussed later: see Remark 1 in Section 4)
the dependent intersection type system. Here, note that we need
only atomic predicates used in the dependent types; higher-ordermodel checking can look for arbitrary boolean combinations of theatomic predicates as candidates of dependent types. Thus, this partalone provides a good alternative to Liquid types [31], which alsoasks users to provide templates of predicates, and infers dependent
2 Here, abstraction types should not be confused with refinement types [35];the abstraction type of a term only tells how the term should be abstracted,
not what are possible values of the term. For example, integer 3 can havetype int[λν.ν < 0] (and it will be abstracted to the boolean value false).
3 To avoid the confusion, we call dependent abstraction types just abstraction types below. We use the term “dependent types” to refer to ordinary
dependent types used for expressing refinement of simple types.

types. Thanks to the power of higher-order model checking, however, our technique can infer dependent, intersection types unlike
Liquid types.
We now discuss the CEGAR part. Given an error path of an abstract boolean program, we can find a corresponding (possibly infeasible) error path of the source program. Whether the error pathis feasible in the source program can be easily decided by symbolically executing the source program along the error path, andchecking whether all the branching conditions in the path are satisfiable (recall the example given earlier). The main question is, if theerror path turns out to be infeasible, how to find a suitable refinement of abstraction types, so that the new abstraction types yieldan abstract boolean program that does not contain the infeasible
error path. This has been well studied for first-order programs [2–4, 8, 13–15], but it is not clear how to lift those techniques to deal
with higher-order programs.
Our approach to finding suitable abstraction types is as follows.
From a source program and its infeasible error path, we first construct a straightline higher-order program (abbreviated to SHP)
that exactly corresponds to the infeasible path, and contains neither recursion nor conditional branches. In the case of the programM3 above, this is easily obtained, as follows:
let f1 x g = g(x+1) in let h1 z y = assert(y>z) in
let k1 n = assume(n>=0); f1 n (h1 n) in k1(c)Here, c is a constant, and assume(b) evaluates b, and proceeds
to the next instruction only if b is true. (But unlike assert, it is
not reduced to fail even if b is false.) For general programs that
contain recursions, the construction is more involved: see Section 5.
For SHP, a standard dependent (refinement) type system issound and complete, in the sense that a program does not reach
fail if and only if the program is typable in the type system.
Further, (a sub-procedure of) previous algorithms for inferring dependent types based on interpolants [32, 33] is actually complete(modulo the assumption that the underlying logic is decidable andinterpolants can always be computed) for SHP. Thus, we can automatically infer the dependent type of each function in the straightline program. For example, for the program above, we obtain:
f1 : (x : int → (y : {ν : int | ν > x} → ) → )
h1 : (z : int → y : {ν : int | ν > z} → )
k1 : (z : int → )Here, the type of h1 means that given integers z and y such thaty > z, h1 z y returns a unit value without reaching fail. (These
dependent types should not be confused with abstraction types:
the latter only provides information about how the source program
should be abstracted.)
We then refine the abstraction type of each function in thesource program with predicates occurring in the dependent typesof the corresponding functions in the SHP. For example, given theabove dependent types, we get the following abstraction types:f : (x : int[ ] → (y : int[λν.ν > x] → ) → )h : (z : int[ ] → y : int[λν.ν > z] → )k : int[ ] → 
We can show that the abstraction types inferred in this manner are
precise enough, in that the abstract program obtained by using the
new abstraction types no longer has the infeasible error path. (Thus,
the so-called “progress” property is guaranteed as in CEGAR methods for finite-state or pushdown model checking.)
Based on the predicate abstraction and CEGAR techniques
mentioned above, we have implemented a prototype verifier for(simply-typed) higher-order functional programs with recursion
and integer base types, and tested it for several programs.
Our contributions include: (i) the formalization of predicate
abstraction for higher-order programs, based on the novel notionof abstraction types, (ii) the formalization of CEGAR for higher-

order programs, based on the novel notion of SHP and reduction of
the predicate discovery problem to dependent type inference, (iii)theoretical properties like the relative completeness of our methodwith respect to a dependent intersection type, the progress property,
etc., and (iv) the implementation and preliminary experiments.
The rest of this paper is structured as follows. Section 2 introduces the source language, and Section 3 introduces a language ofhigher-order boolean programs, and reviews the result on higherorder model checking. Sections 4 and 5 respectively formalize
predicate abstraction and CEGAR for higher-order programs. Section 6 reports our prototype implementation and preliminary experiments. Section 7 discusses related work, and Section 8 concludes.
For the space restriction, proofs are omitted, which are available ina full version [25].

2.

LanguageThis section introduces a simply-typed, higher-order functional
language, which is used as the target of our verification method.
We assume a set B = {b1 , . . . , bn } of data types, and a set[[bi ]] of constants, ranged over by c, for each data type bi . We also
assume that there are operators op : bi1 , . . . , bik → bj ; we write[[op]] for the function denoted by op. We assume that the set ofdata types includes  with [[]] = , and bool with [[bool]] ={true, false}, and that the set of operators includes = : b, b →bool for every b ∈ B, and boolean connectives such as ∧ :bool, bool → bool.
The syntax of the language is given by:
D (program)e (expressions)v (values)

::=
::=
|
::=

e1 = e1 , . . . , fm x
em = em }{f1 x
c | x ve | f ve | let x = e1 in e2 | op(ev)
fail | assume v; e | e1 ˜ e2
c | x | f ve

Here, xe abbreviates a (possibly empty) sequence x1 , . . . , xn . In
the definition f x
e = e, we call the length of xe the arity of f . In
the definition of values, the length of ve in f ve must be smaller than
the arity of f . (In other words, f ve must be a partial application.)
We assume that every function in D has a non-zero arity, and that
D contains a distinguished function symbol main ∈ {f1 , . . . , fm }whose simple type is  → .
Most of the expressions are standard, except the following ones.
The expression fail aborts the program and reports a failure. The
expression assume v; e evaluates e if v is true; otherwise it stops
the program (without a failure). The expression e1 ˜ e2 evaluates
e1 or e2 in a non-deterministic manner. Note that a standard conditional expression if v then e1 else e2 can be expressed as:(assume v; e1 ) ˜ (let x = ¬v in assume x; e2 ).
We can express the assertion assert v as if v then  else fail.
The random number generator randi used in Section 1 is definedby:randi  = (randiFrom 1)˜(randiTo 0)
randiFrom n = n˜(randiFrom (n + 1))
randiTo n = n˜(randiTo (n − 1))
We assume that a program is well-typed in the standard simple
type system, where the set of types is given by:τ ::= b1 | · · · | bn | τ1 → τ2 .
Furthermore, we assume that the body of each definition has a data
type bi , not a function type. This is not a limitation, as we canalways use the continuation-passing-style (CPS) transformation totransform a higher-order program to an equivalent one that satisfies
the restriction.
We define the set of evaluation contexts by: E ::= [ ] | let x =E in e. The reduction relation is given in Figure 2. We label the

fx
e=e∈D
E[f ve] −→D E[[e
v /e
x]e]


E[let x = v in e] −→D E[[v/x]e](E-L ET)E[op(ec)] −→D E[[[op]](ec)]
E[e0 ˜ e1 ] −→D E[ei ](E-A SSUME)

E[fail] −→D fail

(E-FAIL)

Figure 2. Call-by-Value Operational Semantics
reduction relation with 0, 1,  to record which branch has beenchosen by a non-deterministic expression e1 ˜ e2 ; it will be used
to relate reductions of a source program and an abstract program
l ···lnlater in Sections 4 and 5. We write e1 1=⇒ D e2 if




wf Γ
Γ wf σwf Γ, x : σ

Figure 3. Well-formed types and type environments(E-PAR)E[assume true; e] −→D E[e]lΓ wf σ1
Γ, x : σ1 wf σ2Γ wf x : σ1 → σ2
wf ∅(E-O P)i

A2S(Γ), x : b ST ψi : bool for each i ∈ {1, . . . , n}
Γ wf b[λx.ψ1 , . . . , λx.ψn ](E-A PP)



l



1
n
∗
∗
∗
e1 (−→D )∗ −→D (−→D ) · · · (−→D ) −→D (−→D ) e2 .

We often omit the subscript D when it is clear from the context.
The goal of our verification method is to check whethersmain  =⇒D fail.4

We can use a recursion scheme model checker TR EC S [21, 22]s
to decide the above property.5 If ∃s.(main =⇒D fail) holds,
the model checker generates an error path s. The knowledge about
recursion schemes is unnecessary for understanding the rest of thispaper, but an interested reader may wish to consult [20, 22, 28].

4.

Predicate Abstraction

This section formalizes predicate abstraction for higher-order programs. As explained in Section 1, we use abstraction types to express which predicates should be used for abstracting each subexpression. The syntax of abstraction types is given by:
σ (abstraction types)
P, Q (predicates)Γ (type environments)

::=
::=
::=

b1 [Pe] | · · · | bn [Pe] | x : σ1 → σ2
λx.ψ
∅ | Γ, f : σ | Γ, x : σ

Theorem 3.1. Let D be an HBP. The property ∃s.(main =⇒Dfail) is decidable.

Here, the meta-variable ψ represents an expression of type bool
(which is called a formula) that is constructed only from variablesof base types, constants, and primitive operations; we do not allow
formulas that contain function applications, like y > f (x). Thebase type bi [Pe] describes values v of type bi that should be abstracted to a tuple of booleans P1 (v), . . . , Pn (v). For example,
the integer 3 with the abstraction type int[λν.ν > 0, λν.ν < 2]
is abstracted to true, false. We often abbreviate b[ ] to b. The
dependent function type x:σ1 → σ2 describes functions that take avalue v of type σ1 , and return a value of type [v/x]σ2 . The scope ofx in the type x:σ1 → σ2 is σ2 . When x does not occur in σ2 , we often write σ1 → σ2 for x : σ1 → σ2 . As mentioned already, abstraction types only describe how each expression should be abstracted,
not the actual value. For example, 3 can have type int[λν.ν < 0],and λx.x can have type x : int[ ] → int[λν.ν = x + 1] (andabstracted to λx : .false).
We do not consider types whose predicates are ill-typed orviolate a variable’s scope, such as x : bool[ ] → int[λy.x + 1 = y]and x : int[λx.y > x] → y : int[ ] → bool[ ]. (The former uses aboolean variable as an integer, and the latter refers to the variable youtside its scope.) Figure 3 defines the well-formedness conditions
for types and type environments. In the figure, Δ ST e : τ denotes
the type judgment of the standard simple type system. We write
A2S(σ) and A2S(Γ) respectively for the simple type and the simple
type environment obtained by removing predicates. For example,
A2S(f : (x : int[ ] → int[λy.y > x]), z : int[λz.z > 0]) =f : int → int, z : int.
Figure 4 defines the predicate abstraction relation Γ  e1 :σ
e2 , which reads that an expression e1 (of the source language in Section 2) can be abstracted to an expression e2 (ofthe HBP language given in Section 3) by using the abstraction
type σ, under the assumption that each free variable x of e1 has
been abstracted using the abstraction type Γ(x). In the rules, it
is implicitly assumed that all the type environments and types
are well-formed. We do not distinguish between function vari-

4 Thus, we consider the reachability problem for a closed program. Note,however, that we can express unknown values by using non-determinism(recall randi). It is also easy to extend our method to deal with more generalverification problems, such as resource usage verification [22].

5 The gap between the operational semantics of our language and that ofrecursion schemes can be filled by the CPS transformation. Note also that
finite state or pushdown model checkers cannot be used, as higher-orderprograms are in general strictly more expressive [10].

3.

Higher-Order Boolean Programs and Model
Checking

A source program is translated to a higher-order boolean program(abbreviated to HBP) by the predicate abstraction discussed in
Section 4. The language of HBP is essentially the same as thesource language in the previous section, except:• The set of data types consists only of types of the formbool × · · · × bool (which is identified with  when m = 0, and
{z
}
|
m

bool when m = 1). We assume there are the following operators
to construct or deconstruct tuples:·, . . . , ·i::bool, . . . , bool → bool × · · · × bool
bool × · · · × bool → bool

• The set of expressions is extended with e1 ¨ e2 and unnamed functions λx.e. The former is used for expressing the nondeterminism introduced by abstractions; it is the same as e1 ˜ e2 ,which is used to express the non-determinism present in a source
program, except that the reduction is labelled with . This distinction is convenient for the CEGAR procedure discussed in Section 5
to find a corresponding execution path of the source program froman execution path of the abstract program. Unnamed functions areused just for technical convenience for defining predicate abstraction; with λ-lifting, we can easily get rid of λ-abstractions. (Theevaluation rules and evaluation contexts are accordingly extended
with E[(λx.e)v] −→ E[[v/x]e] and E ::= · · · | E e | v E.)
The following theorem is the basis of our verification method.
It follows immediately from the decidability of the model checkingof higher-order recursion schemes [28].
se is a constant, a variable or an expression of the form op(ev)
A2S(Γ) ST e : bΓ  e : b[λν.ν = e]true
(A-BASE)eΓ  e : b[Q]ee ST ψ : boole ST ψ  : boolβ(Γ, x : b[Q])β(Γ, x : b[Q])|= P (x) ⇒ θΓ,x:b[Q]|= ¬P (x) ⇒ θΓ,x:b[Q]e (ψ)
e (ψ )
e = (assume ψ; true) ¨ (assume ψ ; false)e P]
Γ  e : b[Q,let x = e in x, e (A-CA DD)e Pe]
Γ  e : b[Q,eΓ  e : b[Pe]let ex, ye = e in ey(A-CR EM)Γ(x) = (y1 : σ1 → · · · → yk : σk → σ)eiΓ, y1 : σ1 , . . . , yi−1 : σi−1  vi : [v1 /y1 , . . . , vi−1 /yi−1 ]σi(for each i ∈ {1, . . . , k})
let y1 = e1 in · · ·Γ  x ve : [e
v /e
y ]σ
let yk = ek in x ye
(A-A PP)Γ  e1 : σ e1Γ, x : σ   e2 : σe2Γ  let x = e1 in e2 : σ
let x = e1 in e2(A-L ET)β(Γ) ST ψ : bool|= θΓ (ψ)Γ  fail : σ
assume ψ; fail

(A-FAIL)Γ  v : bool[λx.x]
e1
Γ, x : bool[λx.v]  e : σe2Γ  assume v; e : σ
let x = e1 in assume x; e2Γ  e1 : σe1Γ  e2 : σΓ  e1 ˜ e2 : σe1 ˜ e2e2

(A-A SM)(A-PAR)eΓ, x : σ1  x : σ1e1Γ  e : (x : σ1 → σ2 )Γ, x : σ1 , x : σ1 , y : σ2  y : σ2e2
let f = e in
λx.let x = e1 inΓ  e : (x : σ1 → σ2 )let y = f x in e2(A-CF UN)fi : (exi : σei → σi ) ∈ ΓΓ, xei : σei  ei : σiei(for each i ∈ {1, . . . , m})Γ(main) = [ ] → [ ](A-P ROG)
 {f1 xe1 = e1 , . . . , fm x
em = em } : Γ


{f1 x
e1 = e1 , . . . , fm x
em = em }Figure 4. Predicate Abstraction Rules

ables and other variables (hence, A-A PP applies also to a function variable f ). In A-CA DD, assume e1 ; e2 is a syntax sugar for
let x1 = e1 in assume x1 ; e2 .
In A-CA DD and A-FAIL, β(σ) (β(Γ), resp.) represent the simple type (simple type environment, resp.) obtained by replacing
each occurrence of a base abstraction type b[P1 , . . . , Pm ] withbool × · · · × bool. Intuitively, β(Γ) represents the type environ{z}|mment for the output program of the transformation.
We explain the main rules. Base values are abstracted by using
three rules A-BASE, A-CA DD, and A-CR EM. Before explaining
those rules, let us discuss the following simplified version, specialized for a single predicate:|= P (e) ⇒ θΓ (ψ)|= ¬P (e) ⇒ θΓ (ψ  )Γ  e : b[P ](assume ψ; true) ¨ (assume ψ  ; false)(A-BS IMP)
Here, we assume that e is a constant, a variable, or an expression of
the form op(ev ) and has a base type b. ψ and ψ  are boolean formulas that may contain variables in Γ. As e may contain variables, weneed to take into account information about the values of the variables, which is obtained by using the substitution θΓ , defined as:{x → P1 (x), . . . , Pm (x) | Γ(x) = b[P1 , . . . , Pm ]}. For example, let Γ be x : int[λx.x > 0, λx.x < 0] and ψ be 1 (x) ∧ 2 (x).
Then, θΓ (ψ) = x > 0 ∧ x < 0. As in this example, the substitution θΓ maps a boolean expression of an abstract program to thecorresponding condition in the source program. In rule A-BS IMP
above, |= P (e) ⇒ θΓ (ψ) means that P (e) is true only if θΓ (ψ)
is true, i.e. the value of ψ in the abstract program is true. Thus, theabstract value of e may be true only if the value of ψ is true,
hence the part assume ψ; true in the abstract program. Similarly,
the abstract value of e may be false only if the value of ψ  is true,
hence the part assume ψ  ; false.
For example, let e ≡ x + 1, P ≡ λx ≥ 0, and Γ ≡ x : int[P ].
Then, |= P (x + 1) ⇒ true and |= ¬P (x + 1) ⇒ ¬P (x), so thate is abstracted to (assume true; true) ¨ (assume ¬x; false).
Note that θΓ (¬x) = [P (x)/x]¬x = ¬P (x).
We need to generalize the above rule to the case for multiple
predicates. The following is a naive rule.
Γ  e : b[Pi ]Γ  e : b[P1 , . . . , Pn ]ei
(A-BC ARTESIAN)
e1 , . . . , en 

This produces a well-known cartesian abstraction, which is often
too imprecise. The problem is that each boolean value of the abstraction is computed separately, ignoring the correlation. For example, let P1 ≡ λx.x > 0 and P2 ≡ λx.x ≤ 0 with n = 2.
Then, a possible abstraction of an unknown integer should betrue, false and false, true, but the above rule would generate (true ¨ false), (true ¨ false), which also contains
true, true and false, false.
The discussion above motivated us to introduce the three rules
A-BASE, A-CA DD, and A-CR EM. In order to abstract an expression e with b[P1 , . . . , Pn ], we first use A-BASE to abstract e totrue by using the abstraction type b[λν.ν = e]; this is necessary
to keep the exact information about e during the computation of abstractions. A-CA DD is then used to add predicates P1 , . . . , Pn one
by one, taking into account the correlation between the predicates.
Note that in A-CA DD, the result of abstraction by the other predicates is taken into account by the substitution θΓ,x:b[Q]e . Finally,
A-CR EM is used to remove the unnecessary predicate λν.ν = e.
See Example 4.1 for an application of these rules.
Note that rule A-CA DD is non-deterministic in the choice ofconditions ψ and ψ  , so that how to compute the conditions is left
unspecified. We have intentionally made so, because depending onbase data types, the most precise conditions (the strongest conditions entailed by P (x) and ¬P (x)) may not be computable or are
too expensive to compute. For linear arithmetics, however, we canuse off-the-shelf automated theorem provers to obtain such conditions.
In rule A-A PP, each argument vi is abstracted by using theabstraction type σi with y1 , . . . , yi−1 being replaced by the actualarguments. Note that this rule applies also to the case where thesequence ve is empty (i.e. k = 0). Thus, we can derive Γ  y : σ
y if Γ(y) = σ. Note also that the boolean expression ei in A-A PP
can depend on y1 , . . . , yi−1 .
In A-FAIL, the assume statement is inserted for filtering out
an invalid combination of abstract values. For example, let Γ be

x : int[λx.x > 0, λx.x < 0]. Then, assume (1 (x) ∧ 2 (x)); isinserted since x > 0 and x < 0 cannot be true simultaneously. In
A-A SM, we can use the fact that v is true in e for abstracting e.
Rule A-CF UN is used for changing the abstraction type of afunction from x : σ1 → σ2 to x : σ1 → σ2 , which is analogous
to the usual rule for subtyping-based coercion. If a function f isused in different contexts which require different abstraction typesof f , A-CF UN can be used to adjust the abstraction type of f tothat required for each context.
We can read the predicate abstraction rules for Γ  e : σe as an algorithm that takes Γ, e and σ as input, and outputse as an abstraction of e, by (1) restricting applications of therules for coercion (of names A-CX YZ) to the actual argumentsof function applications, and (2) fixing an algorithm to find theboolean formulas ψ and ψ  in A-CA DD. (Note that in A-L ET, theDtype σ  can be obtained from Γ and e1 .) The rule for  D : Γ
can then be interpreted as an algorithm that takes D and Γ as input,
and outputs an HBP D as an abstraction of D.
x : int[λν.ν ≥ 0], g : int[λν.ν > 0] → 
The body of f is transformed as follows. x + 1 is transformed by:
A-BASEΓ  x + 1 : int[λν.ν = x + 1]
true
A-CA DDΓ  x + 1 : int[λν.ν = x + 1, λν.ν > 0]
e1
A-CR EMΓ  x + 1 : int[λν.ν > 0]e2

Γ  g(x + 1) : e2

let y = if x then trueelse (true¨false) in g(y)Our predicate abstraction rules are applicable to programs thatuse infinite data domain other than integers. See [25] for an example of abstracting a list-processing program.
We discuss properties of the predicate abstraction relation below. First, we show that if abstraction types are consistent, there isalways a valid transformation. We write Γ AT e : σ for the typejudgment relation obtained from the predicate abstraction rules byremoving all the conditions on outputs: see [25].
Theorem 4.1. Suppose Γ AT e : σ. Then, A2S(Γ) ST e : A2S(σ).
e .
Furthermore, there exists e such that Γ  e : σ
Proof. Straightforward induction on the derivation of Γ AT e : σ.
Note that in the rule for A-CA DD, we can choose true as ψ andψ .
The following lemma guarantees that the output of the transformation is well-typed.
Lemma 4.2. If Γ  e1 : σs

D2 and main =⇒D1

The theorem above says that the abstraction is sound but not
how good the abstraction is. We compare below the verification
power of the combination of predicate abstraction and higher-ordermodel checking with the dependent intersection type system given
in [25], which is essentially equivalent to the one in [32].
We write B[ψ1 , . . . , ψk ] for the set of formulas constructedfrom ψ1 , . . . , ψk and boolean operators (true, false, ∧, ∨, ¬).
For an abstraction type σ, the set DepTy(σ) of dependent types is:
DepTy(b[P1 , . . . , Pn ]) = {{ν : b | ψ} | ψ ∈ B[P1 (ν), . . . , Pn (ν)]}
DepTy(x : σ1 → σ2 ) = {(x : δ11 → δ21 ) ∧ · · · ∧ (x : δ1m → δ2m )| δ11 , . . . , δ1m ∈ DepTy(σ1 ), δ21 , . . . , δ2m ∈ DepTy(σ2 )}DepTy({x1 : σ1 , . . . , xn : σn }) ={{x1 : δ1 , . . . , xn : δn } | δi ∈ DepTy(σi ) for each i ∈ {1, . . . , n}}
The following theorem says that our predicate abstraction (withhigher-order model checking) has at least the same verification
power as the dependent intersection type system.

Here, e1 ≡ let y1 = true in y1 , e3  and e2 ≡ let y1 , y2  =e1 in y2 , with e3 ≡ (assume true; true) ¨ (assume ¬(x ∧y1 ); false). Here, we used true and ¬(x∧y1 ) as ψ and ψ  respectively, in A-CA DD. (Note that P (y1 ) ⇒ θΓ,y1 :int[λν.ν=x+1] (ψ1 ),i.e., y1 ≤ 0 ⇒ ¬(x ≥ 0 ∧ y1 = x + 1) holds.) By simplifying e2 , we get if x then true else true¨false. Thus, the bodyg(x + 1) of function f is transformed by using A-A PP as follows:
Γ(g) = int[λν.ν > 0] → 

Theorem 4.3 (soundness). If  D1 : Γsfail, then main =⇒D2 fail.

We extend DepTy to a map from abstraction type environments tothe powerset of dependent type environments by:

Example 4.1. Recall the program M2 in Section 1. Let Γ be:..
.
Γ  x + 1 : int[λν.ν > 0](see [25] for the proof). Thus, the safety of the abstract program(which is decidable by Theorem 3.1) is a sufficient condition forthe safety of the source program.

e2 , then β(Γ) ST e2 : β(σ).

Proof. Straightforward induction on the derivation of Γ  e1 :σ
e2 .
The theorem below states that our predicate abstraction is soundin the sense that if a source program fails, so does its abstraction

Theorem 4.4 (relative completeness). Suppose DIT D : Δ. If
Δ ∈ DepTy(Γ), then there exists D such that  D : Γ
D andmain =⇒ D fail.
Remark 1. The converse of the above theorem does not hold: see[25]. Together with Theorem 4.4, this implies that our combinationof predicate abstraction and higher-order model checking is strictly
more powerful than the dependent intersection type system.
Remark 2. The well-formedness condition for abstraction types
is sometimes too restrictive to express a necessary predicate. For
example, consider the following program.
let apply f x = f x in let g y z = assert(y=z) in
let k n = apply (g n) n; k(n+1) in k(0)In order to verify that the assertion failure does not occur, we needa correlation between the argument of f and x, which cannot be
expressed by abstraction types. The problem can be avoided either
by adding a dummy parameter to apply (as let apply n f x= ...) and using the abstraction type n : int[ ] → (int[λν.ν =n] → ) → int[λν.ν = n] → , or by swapping the parameters
f and x. A more fundamental solution (which is left for futurework) would be to introduce polymorphic abstraction types, like∀m : int.(int[λν.ν = m] → ) → int[λν.ν = m] → , andextend the predicate abstraction rules accordingly.

5.

Counterexample-Guided Abstraction
Refinement (CEGAR)

This section describes a CEGAR procedure to discover new predicates used for predicate abstraction when the higher-order model
checker TR EC S has reported an error path s of a boolean program.
5.1 Feasibility checking
Given an error path s of an abstract program, we first check whetherss is feasible in the source program D, i.e. whether main =⇒D
fail. This can be easily checked by actually executing the source
program along the path s, and checking whether all the branchingconditions are true. (Here, we assume that the program is closed.
If we allow free variables for storing base values, we can just

symbolically execute the source program along the path, and check
whether all the conditions are satisfiable.) If the source programsindeed has the error path (i.e. main =⇒D fail), then we report
the error path as a counterexample.

(infeasible) execution path:main −→ k m =⇒ let x = g(g m) in · · ·01=⇒ let x = g(1) in · · · =⇒ let x = 2 + g(0) in · · ·
0

5.2

s

If the error path is infeasible (i.e. main =⇒D fail), we find new
predicates to refine predicate abstractions.
In the case of the model checking of first-order programs, thisis usually performed by, for each program point in the error
path, (i) computing the strongest condition C1 at , (ii) computing
the weakest condition C2 for reaching from to the failure node,and (iii) using a theorem prover to find a condition C such that
C1 ⇒ C and C ⇒ ¬C2 . Then the predicates in C can be used
for abstracting the state at the program point. For example, in the
reduction sequence (2) of M1 in Section 1, the condition C1 on thelocal variable x is n > 0 ∧ x = n, and the condition C2 is x + 1 ≥ 0.
From them, we obtain C ≡ x > 0 as a predicate for abstracting x.
It is unclear, however, how to extend it to deal with higherorder functions. For example, in the example above, how can wefind a suitable abstraction type for functions f and g? To address
this issue, as mentioned in Section 1, we use the following typebased approach. From an infeasible error path, we first constructa straightline higher-order program (abbreviated to SHP, whichis straightline in the sense that it contains neither branches norrecursion and that each function is called at most once) that hasexactly one execution path, corresponding to the path s of thesource program. We then infer the dependent types of functionsin the straightline program, and use the predicates occurring in
the dependent types for refining abstraction types of the source
program. We describe each step in more detail below.
5.2.1

Constructing SHPGiven a source program and a path s, the corresponding SHP is
obtained by (i) making a copy of each function for each call in theexecution path, and (ii) for each copy, removing the branches nottaken in s.
Example 5.1. Recall the program M3 in Section 1.
main = k m
f x g = g(x + 1)
h z y = (assume y > z; ) ˜ (assume ¬(y > z); fail)k n = (assume n ≥ 0; f n (h n))˜(assume ¬(n ≥ 0); )Here, we have represented conditionals and assert expressions in
our language.6 Given the spurious error path 0 · 1, we obtain thefollowing SHP.
main = k m
h z y = assume ¬(y > z); failf x g = g(x + 1)
k n = assume n ≥ 0; f n (h n)
It has been obtained by removing irrelevant non-deterministic
branches in h and k.
The construction of an SHP generally requires duplication offunction definitions and function parameters. For example, consider the following program:main = k mtwice f x = f (f x)g x = if x ≤ 0 then 1 else 2 + g(x − 1)
k n = let x = twice g n in assert (x > 0)
(where m is some integer constant). The program calls the function
g twice, and asserts that the result x is positive. Suppose that an
infeasible path 0101 has been given, which represents the following
6 Here, for the sake of simplicity, we assume that m is some integer constant. As already mentioned, the random number generator randi can actually be encoded in our language.

1=⇒ let x = 2 + 1 in · · · =⇒ assert 3 > 0 =⇒ fail

Predicate discovery and refinement of abstraction types

The path is infeasible because the final transition is invalid.
From the source program and the path above, we construct thefollowing straightline program:7
main = k mtwice f (1) , f (2)  x = f (2) (f (1) x)(1)g (3) x = assume x ≤ 0; 1
g x = assume x ≤ 0; 1(2)g x = assume ¬(x ≤ 0); 2 + g (3) (x − 1)
k n = let x = twice g (1) , g (2)  n in assume ¬(x > 0); failAs g is called three times, we have prepared three copies g (1) ,g (2) , g (3) of g, and eliminated unused non-deterministic branches.
Note that the function parameter f of twice has been replaced by afunction pair f (1) , f (2)  accordingly.
The general construction is given below. Consider a program
normalized to the following form:
D
e
a
v

::=
::=
::=
::=

{f1 x
e1 = e10 ˜e11 , . . . , fm x
em = em0 ˜em1 }assume v; a | let x = op(ev ) in a | x ve | f ve | failc | x ve | f ve

Here, for the sake of simplicity, we have assumed that every function definition has at most one (tail) function call, and the return value is ; this does not lose generality as the normal form
can be obtained by applying CPS transformation and λ-lifting.
Given a path s = b1 · · · b of D (which means that the branchbi has been chosen at ith function call), the corresponding SHP
D = SHP(D, s) is given by:(j)ei = [eibj ]j+1 | i ∈ {1, . . . , m}, j ∈ {1, . . . , },D = {fi xthe target of the jth function call is fi }(j)∪{fi xei =  | i ∈ {1, . . . , m}, j ∈ {1, . . . , },the target of the jth function call is not fi }∪{main = main(1) }
Here, [e]j is given by:[assume v; a]j = assume v; [a]j[let x = op(ev ) in a]j = let x = op(ev ) in [a]j
[]j = [fail]j = fail[x]j = x(k ≥ 1)[x v1 · · · vk ]j = j (x) v1 j+1 · · · vk j+1
[f v1 · · · vk ]j = f (j) v1 j+1 · · · vk j+1
cj = cxj = x (if x is a base variable)
jy ., . . . , λey ., j (x)(ev j ), . . . ,  (x)(ev j )
(x ve) = λe
{z
}
|
j−1

(if x is a function variable)y ., . . . , λey ., f (j) (ev j ), . . . , f () (ev j )
(f ve)j = λe
{z
}
|
j−1

Here, each function parameter has been replaced by a -tuple offunctions.
The SHP SHP(D, s), constructed from a source program
D and a spurious error path s, contains neither recursion nor
non-deterministic branch, and is reduced to fail if and only ifsmain =⇒D fail. Furthermore, each function in the SHP iscalled at most once.
7 For clarity, we have extended our language with tuples of functions. If
necessary, they can be removed by the currying transformation.

The generated straightline program satisfies the following properties.
Lemma 5.1. Suppose D = SHP(D, s). Then:
1. D contains neither recursions nor non-deterministic branchese1 ˜e2 .
s
2. main =⇒D fail if and only if main =⇒D fail.
(j)
3. Each function fi in D is called at most once.
5.2.2

Typing SHPThe next step is to infer dependent types for functions in SHP.
Thanks to the properties that SHP contains neither recursion nor
non-deterministic branch and that every function is linear, the standard dependent type system is sound and complete for the safetyof the program. Let us write DT D if D is typable in the fragment of the dependent type system presented in Section 4 without
intersection types (but extended with (non-dependent) tuple types).
Lemma 5.2. Let D = SHP(D, s). Then, DT D : Δ for some Δ
if and only if main =⇒D fail.
Proof sketch The “only if” part follows immediately from thesoundness of the dependent type system. For the “if” part, it suffices
to observe that, as every function in D is linear, each variable x ofbase type can be assigned a type {ν : b | ν = v}, where v is thevalue that x is bound to. ˜
We can use existing algorithms [32, 33] to infer dependent
types: we first prepare a template of a dependent type for eachfunction, generate constraints on predicate variables, and solve theconstraints. We give below an overview of the dependent type
inference procedure through an example; an interested reader may
wish to consult [32, 33].
Example 5.2. Recall the straightline program in Example 5.1. We
prepare the following templates of the types of functions f , h, k:f : (x : {ν : int | P1 (ν)} → (y : {ν : int | P2 (ν, x)} → ) → )h : (z : {ν : int | P3 (ν)} → y : {ν : int | P4 (ν, z)} → )k : (x : {ν : int | P0 (ν)} → )
From the program, we obtain the following constraints on P0 , . . . , P4 :∀x.(P1 (x) ⇒ P2 (x + 1, x))
P0 (m)∀z, y.(P3 (z) ∧ P4 (y, z) ⇒ y > z)∀n, y.P0 (n) ⇒(n ≥ 0 ⇒ (P1 (n) ∧ P3 (n) ∧ (P2 (y, n) ⇒ P4 (y, n))))Each constraint has been obtained from the definitions of main,f, g,
and k. They can be normalized to:∀ν.(ν = m ⇒ P0 (ν))∀n, ν.(P0 (n) ∧ n ≥ 0 ∧ ν = n ⇒ P1 (ν))∀x, ν.(P1 (x) ∧ ν = x + 1 ⇒ P2 (ν, x))∀n, ν.(P0 (n) ∧ n ≥ 0 ∧ ν = n ⇒ P3 (ν))∀n, z, ν.(P0 (n) ∧ n ≥ 0 ∧ z = n ∧ P2 (ν, n) ⇒ P4 (ν, z))∀z, y.(P3 (z) ∧ P4 (y, z) ⇒ y > z)
These constraints are “acyclic” in the sense that for each constraintx), Ci contains only (positive) occurrencesof the form Ci ⇒ Pi (eof predicates Pj ’s such that j < i occur. Such constraints can besolved by using a sub-procedure of existing methods for dependent
type inference based on interpolants [32, 33], and the following
predicates can be obtained. (The inferred predicates depend on theunderlying interpolating theorem prover.)P0 (ν) ≡ P1 (ν) ≡ P3 (ν) ≡ true
P2 (ν, x) ≡ P4 (ν, x) ≡ ν > x
Thus, we obtain the following types for f and h:f : (x : {ν : int | true} → (y : {ν : int | ν > x} → ) → )h : (z : {ν : int | true} → y : {ν : int | ν > z} → )

5.2.3

Refining abstraction types

The final step is to refine the abstraction types of the source program, based on the dependent types inferred for the straightline
program. Let δf,j be the inferred dependent type of f (j) . Then,
we can obtain an abstraction type σf,j such that undup(δf,j ) ∈DepTy(σf,j ) (the choice of such σf,j depends on what predicatesare considered atomic), where undup(δ) is defined by:undup({ν : b | ψ})
undup(x : δ1 → δ2 )==undup(δ1 × · · · × δn )={ν : b | ψ}
x : undup(δ1 ) → undup(δ2 )^undup(δi )i∈{1,...,n}

The new abstraction type σf of f is given by:
σf = σf  σf,1  · · ·  σf, ,where σf is the previous abstraction type of f and σ1  σ2 isobtained by just merging the corresponding predicates:e = b[Pe, Q]
eb[Pe]  b[Q](x : σ1 → σ2 )  (x : σ1 → σ2 ) = x : (σ1  σ1 ) → (σ2  σ2 )We write Refine(Γ, Δ) for the refined abstraction type environment f1 : σf 1 , . . . , fn : σf n . (There is a non-determinism comingfrom the choice of σf,j , but that does not matter below.)
Example 5.3. Recall Example 5.3. From the dependent types of f
and g, we obtain the following abstraction types:f : (x : int[ ] → (y : int[λν.ν > x] → ) → )h : (z : int[ ] → y : int[λν.ν > z] → )Suppose that the previous abstraction types weref : (x : int[ ] → (y : int[ ] → ) → )h : (z : int[λν.ν = 0] → y : int[λν.ν > 0] → )
Then, the refined abstraction types are:f : (x : int[ ] → (y : int[λν.ν > x] → ) → )h : (z : int[λν.ν = 0] → y : int[λν.ν > 0, λν.ν > z] → )
5.3 Properties of the CEGAR algorithm
We now discuss properties of the overall CEGAR algorithm. If therefined abstraction type is obtained from an infeasible error paths, the new abstract boolean program no longer has the path s.
This is the so called “progress property” known in the literatureon CEGAR for the usual (i.e. finite state or pushdown) model
checking. Formally, we can prove the following property (see [25]for the proof):
Theorem 5.3 (progress). Let D1 be a well-typed program and s
be an infeasible path of D1 . Suppose D2 = SHP(D1 , s) andDIT D2 : Δ with Γ = Refine(Γ , Δ) for some Γ . Then, theres
D3 , and main =⇒
exists D3 such that  D1 : Γ
D3 fail.
The progress property above does not guarantee that the verification will eventually terminate: There is a case where the entire
CEGAR loop does not terminate, finding new spurious error paths
forever (see Section 6). Indeed, we cannot expect to obtain a soundand complete verification algorithm, as the reachability is undecidable in general even if programs are restricted to those using only
linear arithmetics.
We can however modify our algorithm so that it is relatively
complete with respect to the dependent intersection type system, inthe sense that all the programs typable in the dependent intersection
type system can be verified by our method. Let genP be a total map
from the set of integers to the set of predicates. (Such a total map
exists, as the set of predicates is recursively enumerable.) Upon
the i-th iteration of the CEGAR loop, add the predicate genP(i)to each position of abstraction type, in addition to the predicates
inferred from counterexamples. Then, if a program is well-typed
under Δ in the dependent intersection type system, an abstraction
type environment Γ such that Δ ∈ DepTy(Γ) is eventually found,so that by Theorem 4.4, our verification succeeds. Of course, thisis impractical, but we may be able to adapt the technique of [18] toget a practical algorithm.

6.

Implementation and Preliminary Experiments

Based on our method described so far, we have implemented a
prototype verifier for a tiny subset of Objective Caml, having
only booleans and integers as base types. Instead of the nondeterministic choice (e1 ˜e2 ), the system allows conditionals andfree variables (representing unknown integers). Our verifier uses
TR EC S [21, 22] as the underlying higher-order model checker(for Step 2 in Figure 1), and uses CSIsat [6] for computing interpolants to solve constraints (for Step 4). CVC3 [5] is used forfeasibility checking (for Step 3) and computing abstract transitions (i.e., to compute formulas ψ and ψ  in rule A-CA DD of
Figure 4 for Step 1). As computing the precise abstract transitions (i.e. the strongest formulas ψ and ψ  in rule A-CA DD)
is expensive, we have adapted several optimizations describedin Section 5.2 of [2] such as bounding the maximum numberof predicates taken into account for computing abstraction witha sacrifice of the precision. The implementation can be tested
at http://www.kb.ecei.tohoku.ac.jp/∼ryosuke/cegar/.
The full version [25] contains more details about the experiments.
The results of preliminary experiments are shown in Table 1.
The column “S” shows the size of programs, measured in word
counts. The column “O” shows the largest order of functions in the
program (an order-1 function takes only base values as arguments,
while an order-2 function takes order-1 functions as arguments).8
The column “C” shows the number of CEGAR cycles. The remaining columns show running times, measured in seconds. The column“abst” shows the time spent for computing abstract programs (fromgiven programs and abstraction types). The column “mc” shows
the time spent (by TR EC S) for higher-order model checking. The
column “cegar” shows the time spent for finding new predicates(Step 4 in Figure 1). The column “total” shows the total running
time (machine spec.: 3GHz CPU with 8GB memory).
The programs used in the experiment are as follows. Free variables denote unknown integers.
• intro1, intro2, and intro3 are the three examples in Section 1.
• sum and mult compute 1 + · · · + n and n + · · · + n respec{z}|ntively, and asserts that the result is greater than or equal to n. Hereis the code of sum.
let rec sum n =if n <= 0 then 0 else n + sum (n - 1)
in assert (n <= sum n)• max defines a higher-order function that takes a function thatcomputes the maximum of two integers, and three integers as input,
and returns the maximum of the three integers:
let max max2 x y z = max2 (max2 x y) z inlet f x y = if x >= y then x else y inlet m = max f x y z in assert (f x m = m)
The last line asserts that the return value of max is greater than orequal to x (with respect to the function f ).
• mc91 is McCarthy 91 function.
let rec mc91 x =8 Because of the restriction of the model checker TR EC S, all the source

programs are actually verified after the CPS transformation. Thus, all thetested programs are actually higher-order, taking continuation functions.

if x > 100 then x - 10 else mc91(mc91(x + 11))in if n <= 101 then assert (mc91 n = 91)
The last line asserts that the result is 91 if the argument is less thanor equal to 101.
• ack defines Ackermann function ack and asserts ack(n) ≥ n.
• repeat defines a higher-order function that takes a function
f and integers n, s, then returns f n (s).
let rec repeat f n s =if n = 0 then s else f (repeat f (n - 1) s) in
let succ x = x + 1 inassert (repeat succ n 0 = n)
• fhnhn is a program not typable in the dependent intersection
type system but verifiable in our method (c.f. Remark 1):
let f x y = assert (not (x() > 0 && y() < 0)) in
let h x y = x in let g n = f (h n) (h n) in g m• hrec is a program that creates infinitely many function closures:let rec f g x =if x >= 0 then g x else f (f g) (g x) in
let succ x = x + 1 in assert(f succ n >= 0)• neg is an example that needs nested intersection types:
let g x y = x inlet twice f x y = f (f x) y inlet neg x y = -x() in
if n >= 0 then assert(twice neg (g n) () >= 0)
else ()• apply is the program discussed in Remark 2.
• a-prod, a-cppr, and a-init are programs manipulatingarrays. A (functional) array has been encoded as a pair of the size
and a function from indices to array contents. For example, thefunctions for creating and updating arrays are defined as follows.
let mk_array n i = assert(0<=i && i<n); 0
let update i n a x =a(i); let a’ j = if i=j then x else a(i) in a’
For a-prod and a-cppr, it has been verified that there is no arrayboundary error. Program a-init initializes an array, and asserts thecorrectness of initialization. and a-max creates an array of size nwhose i-th element is n−i, computes the maximum element m, andasserts that m ≥ n. These examples show an advantage of higherorder model checking; various data structures can be encoded as
higher-order functions, and their properties can be verified in a
uniform manner.
• l-zipunzip and l-zipmap are taken from list-processing
programs. We have manually abstracted lists to integers (representing the list length), and then verified the size properties of list functions. For example, the code for l-zipunizp is:let f g x y = g (x+1) (y+1) in
let rec unzip x k =if x=0 then k 0 0 else unzip (x-1) (f k) in
let rec zip x y =if x=0 then if y=0 then 0 else fail()else if y=0 then fail() else 1+zip(x-1)(y-1)
in unzip n zip• hors encodes a model checking problem for higher-orderrecursion schemes extended with integers (which cannot be handled
by recursion scheme model checkers).
• e-simpl and e-fact model programs that use exceptions,where an exception handler is expressed as a continuation, and assert that there are no uncaught exceptions. The idea of the encoding of exceptions is similar to [20], but unlike [20], exceptions can
carry integer values.
• r-lock and r-file model programs that use locks and files,
and assert that they are accessed in a correct manner. The encoding
is similar to [22], but (unlike [22]) the programs’ control behaviors
depend on integer values.

• A program of name “xxx-e” is a buggy version of the program“xxx”.
The above programs have been verified (or rejected, for wrong
programs) correctly, except apply. As discussed in Remark 2,
apply cannot be verified because of the fundamental limitationof abstraction types. Our system continues to infer new (but too
specific) abstraction types (int[λν.ν = i] → ) → int[λν.ν =i] →  for i = 0, 1, 2, . . . forever and (necessarily) does not
terminate. The program can however be verified if the arguments
of apply are swapped. The same problem has been observed forvariations of some of the programs above: sometimes we had to
add or swap arguments of functions.
Another limitation revealed by the experiments is that for somevariations of the programs, the system infers too specific predicatesand does not terminate. For example, the verification for a-max
fails if we assert m ≥ a(j) instead of m ≥ n (where m is the
maximal element computed, a is the array, and j is some index).
Relaxing these limitations seems necessary for verification of larger
programs, and we plan to do so by adding heuristics to generalize
inferred abstraction types (e.g. by using widening techniques [9]).
Apart from the limitations above, our system is reasonably
fast. This indicates that, although higher-order model checking
has the extremely high worst-case complexity (n-EXPTIME complete [28]), our overall approach works at least for small programs
as long as suitable predicates are found. See further discussions on
the scalability in Section 8.

7.

Related Work

7.1

Model Checking of Higher-Order Programs

The model checking of higher-order recursion schemes has been
extensively studied [19, 24, 28]. Ong [28] proved the decidability of the modal μ-calculus model checking of recursion schemes.
Kobayashi [22] then proposed a new framework of higher-orderprogram verification based on the model checking of recursion
schemes, already suggesting a use of predicate abstraction and CEGAR to deal with programs manipulating infinite data domain.
There were two missing pieces in his framework, however. One
was a practical model checking algorithm for recursion schemes(note that the model checking of recursion schemes is in general nEXPTIME-complete), and the other was a method to apply predicate abstraction and CEGAR to higher-order programs. The former
piece has been supplied later by Kobayashi [20], and supplying thelatter piece was the goal of the present paper.
In parallel to the present work, Unno et al. [26, 34] and Ong andRamsay [29] proposed applications of higher-order model checking
to verification of tree-processing programs. Their approaches areradically different from ours. First, they use different abstraction
techniques: tree data are abstracted using either tree automata [26,34] or patterns [29], which cannot abstract values using binary
predicates (such as 2 × x ≥ y). Secondly, The method of [26]applies only to programs that can be expressed in the form of(higher-order) tree transducers, and the extension in [34] requires
user annotations. Ong and Ramsay’s method [29] applies to generalfunctional programs and includes a CEGAR mechanism, but the
precision of their method is heavily affected by that of a variablebinding analysis, and their CEGAR is completely different fromours. Their technique does not satisfy relative completeness like
Theorem 4.4.
7.2

Dependent Type Inference

There have been studies on automatic or semi-automatic inferenceof dependent types [7, 11, 16, 31–33]. There are similarities between the goals of those studies and that of our work. First, one of
the goals of dependent type inference is to prove the lack of asser-tion failures, as in the present work. Secondly, our technique canactually be used for inferring dependent types. Recursion scheme
model checker TR EC S [20] is type-based, and produces type information as a certificate of successful verification. For example, forthe abstraction of the last example in Section 1, it infers the type
 → (true → ) →  for (the abstract version of) f . Combinedwith the abstraction type of f , we can recover the following dependent type for f : (x : int → (y : {ν : int | ν > x} → ) → ).
Though the goals are similar, the techniques are different. Rondon et al.’s liquid types [31] requires users to specify predicates (ormore precisely, shapes of predicates, called qualifiers) used in dependent types. Jhala et al. [16] proposed an automatic method for
inferring qualifiers for liquid types. Their method extracts qualifiers
from a proof that a finite unfolding of a source program does not
get stuck, and has some similarity to our method to infer abstraction types from an error path. Unno and Kobayashi [33] proposed
an automatic method for inferring dependent types. They first prepare templates of dependent types (that contain predicate variables)and generate (possibly recursive) constraints on predicate variables.
They then solve the constraints by using an interpolating theorem
prover. Jhala et al. [17] also propose a similar method, where they
reduce the constraint solving in the last phase to model checkingof imperative programs. These approaches [16, 17, 31, 33] do support higher-order functions, but in a limited manner, in the sensethat nested intersection types are not allowed. The difference between dependent types with/without intersections is like the one
between context (or flow) sensitive/insensitive analyses. The former is more precise though it can be costly.9 In general, nested
intersection types are necessary to verify a program when function
parameters are used more than once in different contexts. Indeed,as discussed in [25], several of the programs in Section 6 (e.g. neg,where the first argument of twice is used in two different contexts)
require nested intersection types, and almost all the examples given
by Kobayashi [20, 22] call for nested intersection types.
The limitation of our current prototype implementation is thatthe supported language features are limited. We believe that it ispossible to extend our implementation to deal with data structures.
In fact, the predicate abstraction introduced in Section 4 applies todata structures given an appropriate theorem prover. We expect the
CEGAR part can also be extended, e.g. by restricting the properties
on data structures to size properties, by treating data constructors
as uninterpreted function symbols, etc.
Technically, most closest to ours is Terauchi’s work [32]. In his
method, candidates for dependent types are inferred from a finite
unfolding of a source program, and then a fixedpoint computation
algorithm is used to filter out invalid types. If the source program
is not typable with the candidates for dependent types, the program is further unfolded and more candidates are collected. This
cycle (which may diverge) is repeated until the source program isfound to be well-typed or ill-typed. This is somewhat similar to
the way our verification method works: abstraction types are inferred from an error trace (instead of an unfolding of a program),and then higher-order model checking (which also involves a fixedpoint computation) is applied to verify the abstract program. If theverification fails and an infeasible error path is found, the error
path is used to infer more predicates, and this cycle is repeated.
Thus, roughly speaking, our CEGAR phase corresponds to that ofTerauchi to find candidates for dependent types, and our phases
for predicate abstraction and higher-order model checking corresponds to Terauchi’s fixedpoint computation phase. Advantages ofours are: (i) our method can generate an error path as a counterexample; there is no false alarm. On the other hand, a counterexample
9 Our method is an extreme case of context/flow sensitive analysis, which issound and complete for programs with finite data domains.

program
intro1
intro2
intro3
sum
mult
max
mc91
ack
repeat
fhnhn
hrec
neg
apply
a-proda-cppr

S
27
29
30
24
31
42
32
53
37
37
34
47
34
70
149

O
2
2
2
1
1
2
1
1
2
2
2
2
2
2
2

C
1
1
1
2
2
1
2
3
3
1
2
1
4
6

abst
0.00
0.00
0.00
0.00
0.01
0.00
0.01
0.02
0.01
0.01
0.00
0.01
0.07
0.32

mc
0.00
0.00
0.00
0.00
0.00
0.00
0.04
0.09
0.02
0.01
0.01
0.01
0.06
2.82

cegar
0.00
0.00
0.00
0.01
0.02
0.03
0.02
0.03
0.12
0.02
0.02
0.01
0.08
0.26

total
0.01
0.00
0.00
0.02
0.03
0.03
0.07
0.15
0.15
0.04
0.03
0.03
0.22
3.40

programa-inita-max
l-zipunzip
l-zipmaphorse-simplee-factr-lockr-filesum-emult-emc91-erepeat-e
a-max-er-lock-e
excep-e

S
96
70
81
65
64
27
55
54
168
26
33
32
35
70
54
27

O
2
2
2
2
2
2
2
1
1
1
1
1
2
2
1
2

C
5
5
3
4
2
1
2
5
12
0
0
0
0
2
0
0

abst
0.16
2.34
0.03
0.07
0.00
0.00
0.00
0.01
0.30
0.00
0.00
0.00
0.00
0.01
0.00
0.00

mc
0.18
2.01
0.08
0.09
0.00
0.00
0.01
0.02
4.78
0.00
0.00
0.00
0.00
0.06
0.00
0.00

cegar
0.38
0.43
0.02
0.03
0.00
0.00
0.00
0.02
0.16
0.00
0.00
0.00
0.00
0.06
0.00
0.00

total
0.73
4.78
0.12
0.20
0.01
0.00
0.01
0.04
5.23
0.00
0.00
0.00
0.00
0.13
0.00
0.00

Table 1. Results of preliminary experimentsof Terauchi’s method is an unfolding of a program, which may actually be safe. (ii) We infer predicates from an error trace, rather
than from an unfolding of a program; From the latter, too many
constraints are generated, especially for programs containing nonlinear recursions. (iii) Our method can find dependent types constructed from arbitrary boolean combinations of the inferred predicates, while Terauchi’s method only looks for dependent types constructed from the formulas directly generated by an interpolating
theorem prover; thus, the success of the latter more heavily relieson the quality or heuristics of the underlying interpolating theorem
prover. (iv) Because of the point (iii) above, our method (predicate
abstraction + higher-order model checking) can also be used in aliquid type-like setting [31] where atomic predicates are given by auser. (v) Because of the point discussed in Remark 1, the combination of our predicate abstraction and higher-order model checking
is strictly more powerful than Terauchi’s approach (as long as suitable predicates are found). (vi) Our method can be extended to verify more general properties (expressed by the modal μ-calculus), byappealing to the results on higher-order model checking [24, 28].

stract transition functions) in the context of conventional model
checking [2, 27]. We have already borrowed some of the optimization techniques as mentioned in Section 6, and plan to adapt more
techniques.

7.3

8.

Traditional Model Checking

Predicate abstraction and CEGAR have been extensively studied
in the context of finite state or pushdown model checking [2–4, 8, 12–15]. Predicate abstraction has also been applied to thegame-semantics-based model checking [1]. We are not, however,aware of previous work that applies predicate abstraction and CEGAR to higher-order model checking. As discussed in Section 1,
the extension of predicate abstraction and CEGAR to higher-ordermodel checking is non-trivial. One may think that defunctionalization [30] can be used to eliminate higher-order functions andapply conventional model checking. The defunctionalization however uses recursive data structures to represent closures, so that theresulting verification method is too imprecise, unless a clever abstraction technique for recursive data structures is available.
The three components of our verification method, predicate abstraction, higher-order model checking (TR EC S), and CEGAR,
may be seen as higher-order counterparts of the three components
of SLAM [2–4]: C2 BP, B EBOP, and N EWTON. Our use of dependency in abstraction types appears to subsume Ball et al.’s polymorphic predicate abstraction [3]. For example, the id function in[3] can be abstracted by using the abstraction type x : int[ ] →int[λy.y = x].
There are a lot of studies to optimize predicate abstraction (especially for optimizing or avoiding the costly computation of ab-

7.4 Abstract Interpretation
The combination of predicate abstraction and higher-order model
checking may be viewed as a kind of abstract interpretation [9]. The
abstract domain used for each functional value is defined by abstraction types, and predicate abstraction transforms a source program into an HBP whose semantics corresponds to the abstract semantics of the source program. Higher-order model checking thencomputes the abstract semantics. An advantage here is that thanks
to the model checking algorithm [20] for higher-order recursion
schemes, the computation of the abstract semantics is often much
faster than a naive fixed-point computation (which is extremely
costly for higher-order function values).

Conclusion

We have proposed predicate abstraction and CEGAR techniques
for higher-order model checking, and implemented a prototype verifier. We believe that this is a new promising approach to automatic
verification of higher-order functional programs. Optimization of
the implementation and larger experiments are left for future work.
We conclude the paper with discussions on the scalability of
our method. The current implementation is not scalable for large
programs, but we expect that (after several years of efforts) we
can eventually obtain a much more scalable verifier based on our
method, for several reasons. First, the complexity of the model
checking of higher-order recursion schemes is n-EXPTIME complete [28], but with certain parameters being fixed, the complexity
is actually polynomial (linear, if restricted to safety properties) timein the size of a recursion scheme (or, the size of HBP). Furthermore,
n-EXPTIME completeness is the worst-case complexity, and recent model checking algorithms [20, 23] do not immediately sufferfrom the n-EXPTIME bottleneck. Secondly, the implementation of
the underlying higher-order model checker TR EC S is premature,and there is a good chance for improvement. Thirdly, the current
implementation of predicate abstraction and CEGAR is also quite
naive. For example, the current implementation computes abstract
programs eagerly. We expect that a good speed-up is obtained bycomputing abstract programs lazily.

Acknowledgment
We would like to thank members of our research group for discussion and comments. We would also like to thank anonymousreferees for useful comments. This work was partially supported
by Kakenhi 20240001.

References[1] A. Bakewell and D. R. Ghica. Compositional predicate abstraction
from game semantics. In TACAS ’09, pages 62–76. Springer, 2009.
[2] T. Ball, R. Majumdar, T. Millstein, and S. K. Rajamani. Automatic
predicate abstraction of C programs. In PLDI ’01, pages 203–213.
ACM, 2001.
[3] T. Ball, T. Millstein, and S. K. Rajamani. Polymorphic predicate abstraction. ACM Transactions on Programming Languages and Systems, 27(2):314–343, 2005.
[4] T. Ball and S. K. Rajamani. The SLAM project: debugging system
software via static analysis. In POPL ’02, pages 1–3. ACM, 2002.
[5] C. Barrett and C. Tinelli. CVC3. In CAV ’07, volume 4590 of LNCS,
pages 298–302. Springer, 2007.
[6] D. Beyer, D. Zufferey, and R. Majumdar. CSIsat : Interpolation for
LA+EUF (tool paper). In CAV ’08, volume 5123 of LNCS, pages 304–
308, 2008.
[7] W.-N. Chin and S.-C. Khoo. Calculating sized types. Higher-Orderand Symbolic Computation, 14(2-3):261–300, 2001.
[8] E. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith. Counterexampleguided abstraction refinement for symbolic model checking. Journalof the ACM, 50(5):752–794, 2003.
[9] P. Cousot and N. Halbwachs. Automatic discovery of linear restraints
among variables of a program. In POPL ’78, pages 84–96. ACM,
1978.
[10] W. Damm. The IO- and OI-hierarchies. Theoretical Computer Science, 20(2):95 – 207, 1982.
[11] C. Flanagan. Hybrid type checking. In POPL ’06, pages 245–256.
ACM, 2006.
[12] S. Graf and H. Saı̈di. Construction of abstract state graphs with PVS.
In CAV ’97, volume 1254 of LNCS, pages 72–83. Springer, 1997.
[13] M. Heizmann, J. Hoenicke, and A. Podelski. Nested interpolants. In
POPL ’10, pages 471–482. ACM, 2010.
[14] T. A. Henzinger, R. Jhala, R. Majumdar, and K. L. McMillan. Abstractions from proofs. In POPL ’04, pages 232–244. ACM, 2004.
[15] T. A. Henzinger, R. Jhala, R. Majumdar, and G. Sutre. Lazy abstraction. In POPL ’02, pages 58–70. ACM, 2002.
[16] R. Jhala and R. Majumdar. Counterexample refinement for functional
programs. Manuscript, available from http://www.cs.ucla.edu/∼rupak/Papers/CEGARFunctional.ps, 2009.
[17] R. Jhala, R. Majumdar, and A. Rybalchenko. Refinement type inference via abstract interpretation. arXiv:1004.2884v1, 2010.
[18] R. Jhala and K. L. McMillan. A practical and complete approach topredicate refinement. In TACAS ’06, volume 3920 of LNCS, pages
459–473. Springer, 2006.
[19] T. Knapik, D. Niwinski, and P. Urzyczyn. Higher-order pushdown
trees are easy. In FoSSaCS ’02, volume 2303 of LNCS, pages 205–
222. Springer, 2002.
[20] N. Kobayashi. Model-checking higher-order functions. In PPDP ’09,
pages 25–36. ACM, 2009.
[21] N. Kobayashi. TR EC S. http://www.kb.ecei.tohoku.ac.jp/∼koba/trecs/, 2009.
[22] N. Kobayashi. Types and higher-order recursion schemes for verification of higher-order programs. In POPL ’09, pages 416–428. ACM,
2009.
[23] N. Kobayashi. A practical linear time algorithm for trivial automata
model checking of higher-order recursion schemes. In FoSSaCS ’11.
Springer, 2011.

[24] N. Kobayashi and C.-H. L. Ong. A type system equivalent to the modal
mu-calculus model checking of higher-order recursion schemes. In
LICS ’09, pages 179–188. IEEE, 2009.
[25] N. Kobayashi, R. Sato, and H. Unno. Predicate abstraction and CEGAR for higher-order model checking. An extended version, available
from http://www.kb.ecei.tohoku.ac.jp/∼uhiro/, 2011.
[26] N. Kobayashi, N. Tabuchi, and H. Unno. Higher-order multiparameter tree transducers and recursion schemes for program verification. In POPL ’10, pages 495–508. ACM, 2010.
[27] K. L. McMillan. An interpolating theorem prover. Theoretical Computer Science, 345(1):101–121, 2005.
[28] C.-H. L. Ong. On model-checking trees generated by higher-orderrecursion schemes. In LICS ’06, pages 81–90. IEEE, 2006.
[29] C.-H. L. Ong and S. J. Ramsay. Verifying higher-order functional
programs with pattern-matching algebraic data types. In POPL ’11,
pages 587–598. ACM, 2011.
[30] J. C. Reynolds. Definitional interpreters for higher-order programming
languages. In Proceedings of the ACM annual conference - Volume 2,
pages 717–740. ACM, 1972.
[31] P. Rondon, M. Kawaguchi, and R. Jhala. Liquid types. In PLDI ’08.
ACM, 2008.
[32] T. Terauchi. Dependent types from counterexamples. In POPL ’10,
pages 119–130. ACM, 2010.
[33] H. Unno and N. Kobayashi. Dependent type inference with interpolants. In PPDP ’09, pages 277–288. ACM, 2009.
[34] H. Unno, N. Tabuchi, and N. Kobayashi. Verification of treeprocessing programs via higher-order model checking. In APLAS ’10,
volume 6461 of LNCS, pages 312–327. Springer, 2010.
[35] H. Xi and F. Pfenning. Dependent types in practical programming. In
POPL ’99, pages 214–227. ACM, 1999.