Towards a Scalable Software Model
Checker for Higher-Order Programs
Ryosuke Sato

Hiroshi Unno

Naoki Kobayashi

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

University of Tsukuba
uhiro@cs.tsukuba.ac.jp

University of Tokyokoba@is.s.u-tokyo.ac.jp

Abstract
In our recent paper, we have shown how to construct a fullyautomated program verification tool (so called a “software model
checker”) for a tiny subset of functional language ML, by combining higher-order model checking, predicate abstraction, and CEGAR. This can be viewed as a higher-order counterpart of previous software model checkers for imperative languages like BLAST
and SLAM. The naı̈ve application of the proposed approach, however, suffered from scalability problems, both in terms of efficiency
and supported language features. To obtain more scalable softwaremodel checkers for full-scale functional languages, we propose aseries of optimizations and extensions of the previous approach.
Among others, we introduce (i) selective CPS transformation, (ii)selective predicate abstraction, and (iii) refined predicate discovery
as optimization techniques; and propose (iv) functional encoding ofrecursive data structures and control operations to support a larger
subset of ML. We have implemented the proposed methods, andobtained promising results.
Categories and Subject Descriptorsing]: Software/Program Verification

D.2.4 [Software Engineer-

Keywords Higher-Order Model Checking, Predicate Abstraction,
Abstraction Refinement, Dependent Types, CPS Transformation

1.

Introduction

In our recent paper [15], we have shown how to construct a fullyautomated program verification tool (so called a “software model
checker”) for a tiny subset of functional language ML, a simplytyped lambda calculus with recursion and integers. The framework
is an extension of higher-order model checker (more precisely, themodel checker for higher-order recursion scheme) for infinite data
domains such as integers, obtained by combining the techniquesof predicate abstraction [8] and counterexample-guided abstraction
refinements (CEGAR) [1, 6]. This can be viewed as a higher-ordercounterpart of previous software model checkers for imperative
languages like BLAST [9] and SLAM [1]. We have implemented averification tool, MoCHi, based on the framework.
The naı̈ve application of the proposed approach, however, suffered from scalability problems, both in terms of efficiency andsupported language features. For example, the previous frameworkc ACM, 2013. This is the author’s version of the work. It is posted here by permission⃝of ACM for your personal use. Not for redistribution. The definitive version was
published in the Proceedings of the ACM SIGPLAN 2013 Workshop on Partial
Evaluation and Program Manipulation (PEPM 2013)

Functional
Program

Step 1:
Predicate
Abstraction

New Predicates

Step 5:Predicate
Discovery
infeasible
Step 4:
Feasibility
Check

CBV
BooleanProgramfeasible

unsafeError TraceNG

Step 2:CPS
transformation

CBN
BooleanProgram

Step 3:
OK
Higher-Order
Model Checking

safe

Figure 1. Higher-Order Model Checking with Predicate Abstraction and CEGAR
does not support recursive data structures and our implementation
based on the framework does not support control operations. To
explain the problem of the previous framework/implementation, let
us first review our previous framework.
Our previous verification framework [15] is based on predicate
abstraction and CEGAR for a higher-order model checker. Figure 1
shows the overall structure of our previous method. In Step 1, an
input program, written in a simply typed call-by-value lambda calculus with recursion and integers, is abstracted to a higher-orderboolean program by predicate abstraction. The abstracted programis verified by a higher-order model checker, where models are described by higher-order recursion schemes, in Step 3. Higher-orderrecursion schemes [18] can be viewed as a simply typed call-byname lambda calculus with finite data domains and recursion. To
resolve the gap between the evaluation strategies of higher-orderrecursion schemes and higher-order boolean programs, we translate the call-by-value (CBV) program into a call-by-name (CBN)
program in Step 2. If the abstracted program is safe (i.e., assertions never fail), the original functional program is also safe. If
not, by using a counterexample produced by the higher-order model
checker, we check whether the original program is in fact unsafe or
the abstraction is too coarse in Step 4. If the latter, we discover new
predicates in Step 5. We repeat these steps until we find whether
the program is safe or not.
In this paper, we address several limitations of our previous
work. We discuss each problem and explain our approach below.
1. Continuation-passing style (CPS) transformation in Step 2
caused an efficiency problem for the previous version of MoCHi.

letrec check x f = f x; check (x+1) f
let f x = assert (x >= 0)
let main n = check n f
Figure 2. Example Program of Selective CPS Transformation
let add x y = x + yletrec sum x = if x<=0 then 0 else add x (sum(x-1))
let main x = assert (sum x >= x)
Figure 3. Example Program of Selective Predicate Abstraction

As stated above, our approach requires CPS transformation to resolve the gap between the evaluation strategies of higher-orderrecursion schemes and higher-order boolean programs. However,
CPS transformation significantly increases the order1 of programs.
Since the complexity of model checking of higher-order recursion
scheme is n-EXPTIME complete for order-n recursion scheme, theincrease of the order of an input is crucial to the verification time.
For example, consider the program shown in Figure 2. The above
program is translated into the following program by a naı̈ve callby-value CPS transformation [20].
letrec check x k1 =k1 (λf.λk2.f x (λ_.check (x+1) (λg.g f k2)))
let f x k = assert (x >= 0); k ()let main n k = check n (λg. g f k)
To preserve the evaluation order of an original call-by-value program, each function of the translated call-by-name program takes
a continuation and passes its return value to the continuation. Notehere that the order of the translated program has increased to 5. The
continuation k1 of check can actually be omitted however, since apartial application of check in the original program never causes
side effects including an assertion failure. We can, therefore, obtainthe following order-3 program.
letrec check x f k = f x (λ_.check (x+1) f k)
let f x k = assert (x >= 0); k ()let main n k = check n f k
Our CPS transformation avoids such unnecessary insertion of continuations. We formalize this transformation, called selective CPS
transformation.
2. The main bottleneck of the previous version of MoCHi was
the predicate abstraction and discovery (Steps 1 and 5), rather thanhigher-order model checking. Our previous method for predicate
abstraction tried to abstract every function in the program. As aresult, verification of a program did not succeed until an appropriate
set of predicates is found for every function. For example, consider
the program shown in Figure 3. The program can be successfully
verified if we abstract the program by using predicates λy. y ≥ 0
for the second argument of add and λr. r ≥ x for the return valuesof add and sum. The following is the abstracted program obtainedby using the above predicates.
let add () b = b
letrec sum () = if * then trueelse add () (if sum () then true else *)let main x = assert (sum ())
Here, * means a non-deterministic boolean value. The argument b
denotes whether y ≥ 0 holds or not. In the previous paper [15], wehave adapted CEGAR to find such predicates, but the technique isnecessarily heuristic, and often fails. If we cannot find the predicates for add, we get the following abstracted program.
let add () () = ()letrec sum u = if * then true

letrec copy x = if x=0 then 0 else 1 + copy (x-1)
let main n = assert (copy (copy n) = n)Figure 4. Example Program for Refined Predicate Discovery

else let b = sum () and u = add () () in *let main x = assert (sum ())
Since the return value of add is non-informative, the abstraction is
too coarse for proving the safety of the original program.
To reduce the burden to the predicate discovery phase, we introduce
a refinement of predicate abstraction called selective predicate abstraction. As the name suggests, the selective predicate abstraction
applies predicate abstraction to only a certain set of functions, andavoids abstraction of the other functions by inlining them. The selective predicate abstraction generates the following safe programby using only the predicate λr. r ≥ x for the return values of sum
and inlining add.
letrec sum () =if * then true else if sum() then true else *let main () = assert (sum ())
In this way the selective predicate abstraction improves the precision of abstraction and reduces the number of CEGAR iterations.
3. Even with the selective predicate abstraction, the previous
version of MoCHi sometimes failed to discover an appropriate setof predicates. For example, consider the program shown in Figure 4. The program can be successfully verified if we abstract the
program by using the predicate r = x on the argument x and thereturn value r of copy. The old version of MoCHi, however, continued to find too specific predicates such as x = 0∧r = 0, x = 1∧
r = 1, ..., infinitely. This is due to the too much path- and contextsensitivity of MoCHi. In Step 5, MoCHi first prepares a template ofa refinement type for each function call in the spurious error path.
For example, if there are two calls of the copy function, we prepare
two templates x : {v : int | P1 (v)} ⇒ {r : int | Q1 (x, r)} andx : {v : int | P2 (v)} ⇒ {r : int | Q2 (x, r)}. MoCHi then generates and solves constraints on the predicate variables in the template. The advantages of the approach are the context-sensitivity(different types can be assigned to different calls) and the existenceof a complete algorithm (modulo certain assumptions) to solve theconstraints, but the disadvantage is that the inferred constraints areoften too specific. To address this problem, we refine our predicate
discovery method by merging information about multiple calls of
the same function as much as possible; in the example above, wemerge P1 with P2 , and Q1 with Q2 as long as the resulting constraints are satisfiable. Combined with some heuristic for using an
underlying theorem prover, the refined method tends to discover abetter set of predicates, as confirmed by experiments.
4. Another limitation was that many important language features such as recursive data structures and exceptions were not supported. Predicate abstraction can in principle be applied to recursive data structures, but there is not a good practical (interpolating)theorem prover that can be used for finding appropriate predicateson recursive data structures.2 To support recursive data structures
without relying on an interpolating theorem prover for them, we
encode recursive data structures using higher-order functions andreduce verification of programs manipulating data structures to thatof programs manipulating integers. For example, a list is encoded
to a function that maps an index i to the i-th element. Similarly,
we support control operations (e.g., exceptions and call/cc) byencoding them using higher-order functions.
2 One approach would be to treat data constructors as uninterpreted function

1 The order of program t is the maximum order of the types of functions in

t. The order of type τ is defined by order (int) = 0, order (τ1 → τ2 ) =max (order (τ1 ) + 1, order (τ2 )).

(UF) symbols, and use an interpolating theorem prover that handles UF. It
cannot, however, be used for finding inductive predicates such as “a list ℓ isa sequence of the form (ab)∗ ”.

The rest of this paper is organized as follows. We first formalize
the source language of verification in Section 2. Section 3 formalizes the selective predicate abstraction and the selective CPS transformation. Section 4 shows the refined predicate discovery. Section 5 describes the language extensions for recursive data structures and control operations. Section 6 reports experiments. Section 7 discusses related work and Section 8 concludes the paper.
For the space restriction, proofs are omitted, which will be available in the first author’s forthcoming PhD thesis.

2.

In this section, we introduce the source language of our verification method. The source language is a simply-typed call-by-value
higher-order functional language with recursion and integers (a la“PCF”) with the syntax defined by:v (values)τ (types)

::=
::=
|
::=
::=

{f1 = v1 , . . . , fn = vn }n | x | λx. t | t1 t2 | op(t1 , t2 )if0 t1 then t2 else t3 | failn | x | λx. t
int | τ1 → τ2

The meta-variable op ranges over the set of operators over integers.
The expressions are standard except that there is a primitive failthat aborts a program. We use true and false as aliases of 0 and
1, and we write assert(t) for if0 t then 0 else fail, let x =t1 in t2 for (λx. t2 ) t1 , (t1 op t2 ) for op(t1 , t2 ). We assume that(i) a program is well-typed in the standard simple type system, (ii)every function in a program D has a function type, and (iii) D
contains a distinguished function symbol main ∈ {f1 , . . . , fn }whose type is int → int. The goal of our verification is to check
whether main n ̸−→∗D fail for all integer n.

3.

Optimizations

This section introduces optimizations for each phase of CPS transformation (Step 2) and predicate abstraction (Step 1) in Figure 1.
3.1(CPS-C ONST)(CPS-VAR)Γ ⊢ t1 : int, N ; t′1

Γ ⊢ t2 : int, N ; t′2(CPS-O P N)Γ ⊢ op(t1 , t2 ) : int, N ; op(t′1 , t′2 )Γ ⊢ t1 : int, ℓ1 ; t′1
Γ ⊢ t2 : int, ℓ2 ; t′2ℓ′1
Γ ⊢ op(t1 , t2 ) : int, N ; @ (t1 , λx1 . @ℓ2 (t′2 , λx2 . op(x1 , x2 )))(CPS-O P C)
Γ, x : τ1 ⊢ t : τ2 , N ; t′Γ ⊢ λx. t : τ1 →N τ2 , N ; λx. t′

Source Language

D (programs)t (terms)Γ ⊢ n : int, N ; n
Γ, x : τ ⊢ x : τ, N ; x

Selective CPS transformation

This section formalizes selective CPS transformation for abstracted
programs. As stated in Section 1, the idea of the selective CPS
transformation is to distinguish whether a continuation parametershould be inserted to each expression or not based on whether it
has a side-effect. When a function application has no side-effects,
we need not insert a continuation. Here, fail, non-deterministic
branch, and non-termination are considered as side-effects. A similar transformation has been proposed by Nielsen [17]. The transformation does not fit our purpose to translate call-by-value programs into equivalent call-by-name programs. A non-terminating
program may be transformed into a terminating (call-by-name) program by his transformation.
We first define the source language (and the target language)of selective CPS transformation. The language is the same as theone in Section 2 except: (i) the set of terms is extended with nondeterministic branch t1 ■t2 , and (ii) a label ℓ ∈ {C, N } is attachedto each function type, like τ1 →ℓ τ2 . The labels indicate whether
we should insert a continuation or not.
Below, we formalize the selective CPS as a type-based transformation. Figure 5 shows the rules of the selective CPS transformation. In the figure, @ℓ (−, −) is an operation defined as @N (t, k) =k t and @C (t, k) = t k. The relation Γ ⊢ t : τ, ℓ ; t′ means thata term t is translated to a term t′ by using a type τ , under the assumption that (i) each free variable x of t has been transformed
using the type Γ(x), (ii) t may have a side-effect if ℓ = C, and (iii)t has no side-effect if ℓ = N . The relation Γ ⊢ D ; D′ meansthat a program D is translated to a program D′ according to Γ. The
rules are designed in such a way that transformed term t′ has type

(CPS-A BS N)

Γ, x : τ1 ⊢ t : τ2 , ℓ ; t′Γ ⊢ λx. t : τ1 →C τ2 , N ; λx. λk. @ℓ (t′ , k)
Γ ⊢ t0 : τ1 →N τ , N ; t′0 Γ ⊢ t1 : τ1 , N ; t′1
Γ ⊢ t0 t1 : τ, N ; t′0 t′1(CPS-A BS C)(CPS-A PP N)Γ ⊢ t0 : τ1 →ℓ τ , ℓ0 ; t′0Γ ⊢ t1 : τ1 , ℓ1 ; t′1ℓ′Γ ⊢ t0 t1 : τ, C ; λk. @ 0 (t0 , λx0 . @ℓ1 (t′1 , λx1 . @ℓ (x0 x1 , k)))(CPS-A PP C)Γ ⊢ fail : τ, C ; λk. fail

(CPS-FAIL)Γ ⊢ t1 : int, N ; t′1 Γ ⊢ t2 : τ, N ; t′2 Γ ⊢ t3 : τ, N ; t′3Γ ⊢ if0 t1 then t2 else t3 : τ, N ; if0 t′1 then t′2 else t′3(CPS-I F N)
Γ ⊢ t1 : int, ℓ1 ; t′1 Γ ⊢ t2 : τ, ℓ2 ; t′2 Γ ⊢ t3 : τ, ℓ3 ; t′3Γ ⊢ if0 t1 then t2 else t3 : τ, C ; λk. App ℓ1 (t′1 ,λm. if0 m then @ℓ2 (t′2 , k) else @ℓ3 (t′3 , k))(CPS-I F C)
Γ ⊢ t1 : τ, ℓ1 ; t′1

Γ ⊢ t2 : τ, ℓ2 ; t′2Γ ⊢ t1 ■ t2 : τ, C ; @ℓ1 (t′1 , k) ■ @ℓ2 (t′2 , k)

(CPS-B R)

vi is of the form λx1 . λx2 . . . . λxj . ti
ti is not of the form λx. t′i
Γ(fi ) is of the form τi1 →ℓ1 τi2 →ℓ2 · · · →ℓi(j−1) τij →C τΓ ⊢ vi : Γ(fi ), N ; vi′ for each i ∈ {1, . . . , n}′ }
Γ ⊢ {f1 = v1 , . . . , fn = vn } ; {f1 = v1′ , . . . , fn = vn
(CPS-P ROG)

Figure 5. Selective CPS transformation[[τ ]] if Γ ⊢ t : τ, N ; t′ holds, and the transformed term t′ has type([[τ ]] → X ) → X if Γ ⊢ t : τ, C ; t′ holds, where X is the answer
type and [[τ ]] is defined by:[[int]] = int[[τ1 →N τ2 ]] = [[τ1 ]] → [[τ2 ]]C[[τ1 → τ2 ]] = [[τ1 ]] → ([[τ2 ]] → X ) → X
Thus, a continuation should be inserted only for functions of type
τ1 →C τ2 , not for functions of type τ1 →N τ2 .
In the rule CPS-A BS C, a term λx. t is transformed in a standard
way, i.e. a continuation parameter k is inserted and t′ , the CPS version of t, is applied to k. On the other hand, in the rule CPS-A BS N,
no continuation parameter is inserted and direct style is preserved.
The rules for applications are similar. In the rule CPS-A PP C, acontinuation is inserted, but not in the rule CPS-A PP N. In the rule
CPS-B R, a term t1 ■t2 should be transformed with C and a continuation is needed because we need to treat non-deterministic branch
as a side-effect. In the rule CPS-P ROG, since an application of
a top-level function may cause a side-effect, non-termination, thefunction type for the last argument is annotated with C. For thesake of simplicity, regardless of whether functions are recursive,
we consider all the top-level functions may not terminate conservatively. We can avoid redundant insertion of continuations by sometermination analysis.
As an example, Figure 6 shows the selective CPS transformation of λx. λy. assert(x = y) with type int →N int →C int
for (a) and int →C int →C int for (b). The transformation ofΓxy ⊢ assert : bool →C unit, N ; assertCPS(a)x∈/ dom(E)Γ(x) = (y1 : σ1 → · · · → yn : σn → σ)Γ, y1 : σ1 , . . . , yi−1 : σi−1 | E ⊢for each i ∈ {1, . . . , n}vi : [v1 /y1 , . . . , vi−1 /yi−1 ]σi ; ei
Γ|E ⊢xv
e : [ev /ey ]σ ; let y1 = e1 in · · · let yn = en in x ye
(A-A PP)
E(x) = λex. e
Γ | E ⊢ [ev /ex]e : σ ; e′
(A-A PP E XP)
Γ|E ⊢xv
e : σ ; e′.
..

Γxy ⊢ t : unit, C ; λk. t′ kΓx ⊢ λy. t : int →C unit, N ; λy. λk. t′ k(b)Γ ⊢ λx. λy. t : int →N int →C unit, N ; λx. λy. λk. t′ k..
.
Γx ⊢ λy. t : int →C unit, N ; λy. λk. t′ k

Γ | E ⊢ vi : Γ(fi ) ; vi′
for each i s.t. fi ∈/ dom(E)E ⊆ {f1 = v1 , . . . , fn = vn }dom(Γ) ∩ dom(E) = ∅Γ | E ⊢ {f1 = v1 , . . . , fn = vn } ; {fi = vi′ | fi ∈/ dom(E)}(A-P ROG)Γ ⊢ λx. λy. t : int →C int →C unit, N ;λx. λk′ . k′ (λy. λk. t′ k)

Figure 6. Transformations of λx. λy. assert(x = y). (t =assert(x = y), t′ = assertCPS (x = y), Γx = Γ, x : int.
Γxy = Γx , y : int. assertCPS b k asserts b and returns k ())λy. assert(x = y) in (b) is the same as the one in (a). In (a), there
is no need to insert a continuation parameter after x. On the other
hand, in (b), a continuation parameter is inserted.
When we infer types and labels, we attach label N to function
types as much as possible. Consider function check shown in
Figure 2. By the rule CPS-P ROG, the type of check τ must be′of the form int →ℓ (int →ℓ unit) →C unit. Since there is noconstraint such that τ = τ1 →C τ2 , we instantiate ℓ to label N .
We state properties of the selective CPS transformation. The
first theorem below states that we can transform arbitrary simplytyped programs by the selective CPS transformation. The second
theorem states that the selective CPS transformation is correct inthe sense that the transformed program is reduced to the same value
as the original program.
Theorem 3.1. Suppose D is typable in Γ. There exists Γ′ and D′
such that Γ = Elim(Γ′ ) and Γ′ ⊢ D ; D′ , where Elim(Γ) is thetype environment obtained from Γ by removing annotations.
Theorem 3.2 (Correctness of CPS Transformation). If Γ ⊢ D ;
D′ , then the following holds: main n −→∗D fail if and only ifmain n (λx. x) −→∗D′ fail.
3.2 Selective Predicate Abstraction
We introduce an optimization technique for predicate abstraction,
called selective predicate abstraction.
The idea of selective predicate abstraction is to apply predicate
abstractions only to a certain set of functions and inline the otherfunctions. For example, the program in Figure 3 can be verified by
abstracting only sum and main as stated in Section 1.
We formalize selective predicate abstraction as an extensionof the previous predicate abstraction. In the previous framework,
predicate abstraction is defined as the relation Γ ⊢NS t : σ ; t′which means that t is abstracted to t′ by using the abstraction typeσ under the assumption that each free variable x of t has been
abstracted using the abstraction type Γ(x). Abstraction types aretypes to express which predicate should be used to abstract eachvalue. For example, an abstraction type int[P1 , . . . , Pn ] means thata value v of that type should be abstracted to a tuple (b1 , . . . , bn ),where bi denotes whether Pi (v) holds or not. See our previous
paper [15] for details. We extend the predicate abstraction relation
by adding the set of inlined functions E like Γ | E ⊢ t :σ ; t′ . Here, functions in E are not abstracted and are inlinedin the process of abstraction. An alternative approach would be toinline all the functions in E first, and then apply ordinary predicate
abstraction [15]; we prefer the formalization below (that inline
functions on-demand) as it seems more conveninent for further
optimizations such as memoization of abstractions.

Figure 7. Selective Predicate Abstraction

.
..

.
..
Γ′ | E ⊢ x + s : int[λr. r ≥ x] ; if0 s then true else ∗Γ′ | E ⊢ add x s : int[λr. r ≥ x] ; if0 s then true else ∗Γ | E ⊢ let s = sum (x − 1) in add x s : int[λr. r ≥ x] ;let s = sum () in if0 s then true else ∗Figure 8. Abstraction of add x (sum (x − 1)). (Γ = x :int[], sum : (y : int[] → int[λr. r ≥ y]), x > 0. Γ′ = Γ, s :int[λs. s ≥ x − 1]. E = {add = λx. λy. x + y}, * is a syntactic
sugar for true ■ false.)
Figure 7 shows the key rules of the selective predicate abstraction. Other rules are the same as the previous predicate abstraction
relation [15] except that the set of inlined functions E is added. The
relation Γ | E ⊢ t : τ ; t′ means that t is abstracted to t′ by using
the abstraction type τ under the assumption that each free variablex ∈ dom(Γ) of t has been abstracted using the abstraction typeΓ(x) and each free variable x ∈ dom(E) of t is inlined. If E isempty, the selective predicate abstraction relation is the same as theprevious predicate abstraction.
Figure 8 shows a part of the abstraction of the program shownin Figure 3 with E = {add = λx. λy. x + y}. Due to the restriction of the source language of previous predicate abstraction [15], we translated the term add x (sum (x − 1)) to let s =sum (x − 1) in add x s. In the abstraction of add x s, add is inlined since the definition of add is in E. On the top of the derivation, x + s is abstracted to if0 s then true else (true ■ false)
since s ≥ x holds if translated s is true (that denotes s ≥ x − 1),and we do not know whether s ≥ x otherwise.
For some D and E, there is D′ such that Γ | E ⊢ D ; D′ aslong as there is no cyclic definitions in E like {f = λx. g x, g = λy. f }.
Therefore, one way to decide E is to find a maximal set of the functions that has no cyclic definitions. Even if E has some functions
which are recursive in D, there is D′ such that Γ | E ⊢ D ; D′ insome cases. For example, the following program can be abstractedwith E = {odd = vodd }.
letrec even x = if x = 0 then true else odd (x-1)
and odd x = if x = 0 then false else even (x-1)
let main () = assert (even (n+n))
The following is the abstraction of the program with Γ = even :int[Pe ]→bool, main:int[]→unit where Pe = λx. (x mod 2 = 0).
letrec even b =if (if b then * else false) then trueelse if (if b then false else *) then false
else even b
let main () = assert (even b)
The abstracted program is safe. For comparison, consider the casewhere Γ = even : int[Pe ] → bool, odd : int[] → bool, main :int[] → unit and E = ∅ (which corresponds to our previous
approach [15] where the predicates for odd have not been found).

letrec copy x = if x=0 then 0 else 1 + copy (x-1)
let main n = assert (copy n = n)Figure 9. A Simplified Version of the Program in Figure 4

letrec even b = if (if b then * else false)then true else odd ()and odd () = if * then false else even *let main () = assert (even b)
Since the abstraction of odd is too coarse, the abstracted evenreturns a non-deterministic booleans. Thus, the abstracted programis unsafe.
We state properties of the selective predicate abstraction. The
theorem below states that the predicate abstraction is sound in thesense that if the original program fails, so does its abstraction.
Theorem 3.3 (Soundness). If Γ | E ⊢ D1 ; D2 , andmain n −→∗D1 fail, then main n −→∗D2 fail.
The proposition below states that selective predicate abstraction
is more precise compared to our previous predicate abstraction.
Here, Γ ⊢NS D : τ ; D1 is the predicate abstraction relationin our previous paper [15].
Proposition 3.4. If Γ ⊢NS D : τ ; D1 , Γ | E ⊢ D ; D2 , andmain n −→∗D2 fail, then main n −→∗D1 fail.

4.

Predicate Discovery

In this section, we propose an extension of our previous predicate
discovery method for higher-order programs used in MoCHi [15].
First, we briefly overview the previous method in Section 4.1 andthen discuss its limitation in Section 4.2. Section 4.3 explains theextension of the method, which remedies the limitation.
4.1

Previous Method

In MoCHi, predicates for abstracting each term of a given program
are specified as a kind of dependent types called abstraction types.
MoCHi infers abstraction types automatically in a counterexampleguided manner (recall Figure 1): In a CEGAR iteration of MoCHi,
if the predicate abstraction at that point is not precise enoughto show the safety of the original program, an error path of theabstracted program is returned as a result of higher-order model
checking. If the abstract error path is infeasible (i.e., not a genuine path of the original program), MoCHi generates a straightline
higher-order program (SHP) that is safe if and only if the abstract
error path is infeasible. MoCHi then uses an existing method [24]to infer refinement types that witness the safety of the SHP. Here,to make the inference context-sensitive and complete as discussed
in Section 1, MoCHi ensures the generated SHP to be linear (i.e.,each function is called exactly once) and recursion-free by duplicating and renaming the functions called multiple times in the infeasible error path (see [15] for more details). Finally, MoCHi extracts
abstraction types from the refinement types, which contain precise
enough predicates to refute the infeasible error path.
The key ingredient of the above predicate discovery procedureis the refinement type inference method [24], which consists of two
steps: constraint generation and solving. We review the two steps
respectively in Sections 4.1.1 and 4.1.2.
4.1.1

Constraint Generation

Given a spurious error path, we can construct a SHP D which istypable under a refinement type system (see, for example, [24]for the definition of the system). For example, let us consider
the program in Figure 9, which is a simplified version of the one

in Figure 4. In the course of its verification, we may obtain thefollowing SHP Dcopy :let copy1 x = assume (x<>0); 1 + copy2 (x-1)
let copy2 x = assume (x=0); 0
let main n = assume (copy1 n <> n); failHere, assume e evaluates e and proceeds to the next command
only if e evaluates to true. The SHP corresponds to an infeasible
error path where the else- and the then-branches of copy are respectively taken in the first and the second function call of copy,
and the assertion in the main function fails. Note here that Dcopy
is safe (i.e., fail is not reachable), and hence is typable under therefinement type system.
From a SHP D, we generate Horn-clause-like constraints which
are satisfiable if and only if D is typable. To this end, for eachfunction in D, we prepare a refinement type template with predicate variables, which act as placeholders of refinement predicates tobe inferred. We then generate a typing derivation for D under thetype environment that associates each function with its type template. Horn-clause-like constraints on the predicate variables arethen extracted from the derivation. Since the SHP D is linear andrecursion-free, generated constraints are non-recursive. This is desirable since constraint solving of non-recursive Horn clauses overdecidable underlying theories (e.g., linear arithmetic) is decidable.
For the running example Dcopy , we use the following templates:3
copy1 : (x : int → {ν : int | P1 (x, ν)}) and copy2 : (x : int →{ν : int | P2 (x, ν)}).
copy1 : (x : int → {ν : int | P1 (x, ν)})copy2 : (x : int → {ν : int | P2 (x, ν)})By using them, we obtain the following set Ccopy of constraints:
x = 0 ∧ y = 0 ⇒ P2 (x, y)
P2 (x − 1, y) ∧ x ̸= 0 ∧ z = 1 + y ⇒ P1 (x, z)
P1 (n, x) ⇒ x = n
4.1.2

Constraint Solving

Given a set C of non-recursive Horn clauses, our previous constraint solving algorithm returns a substitution θ for predicate variables in C such that θC is valid. The algorithm iteratively finds asolution for each predicate variable P in C as follows: The algorithm first computes equi-satisfiable constraints CP of the following form by eliminating the other predicate variables in C than P :ϕP ⇒ P (ex)

P (ex) ⇒ ϕ′P

Here, FV (ϕP ) ∩ FV (ϕ′P ) ⊆ {ex} always holds. Intuitively, thepredicate P (ex) represents an invariant of some subexpression e in
the SHP, where some variable ν ∈ {ex} represents the value of e
and each variable in {ex} \ {ν} represents a free variable in e. ϕPand ϕ′P respectively represent the strongest condition satisfied by
the value ν and the weakest condition on ν required by the context
of e. The algorithm then computes I(ϕP , ¬ϕ′P ) as a solution forP (ex) with the help of a technique called interpolation [4, 16] fromautomated theorem proving. Here, an interpolant I(ϕ1 , ϕ2 ) of ϕ1
and ϕ2 (such that ϕ1 and ϕ2 are inconsistent) is a formula ϕ thatsatisfies the following conditions:4• ϕ1 implies ϕ,• ϕ and ϕ2 are inconsistent, and• FV (ϕ) ⊆ FV (ϕ1 ) ∩ FV (ϕ2 ).
For the running example Ccopy , we obtain the following constraints
by eliminating the other predicate variables than P1 :x = 1 ∧ y = 0 ∧ x ̸= 0 ∧ ν = 1 + y
P1 (x, ν)⇒⇒P1 (x, ν)
ν=x

3 For the sake of simplicity, we here omit the type template of main as wellas the refinement predicates for the argument of copy1 and copy2.
4 Note that interpolants of ϕ and ϕ are not unique. Actually, existing
1
2
theorem provers [4, 16] return one of them, which is denoted by I(ϕ1 , ϕ2 ).

We then obtain, for example, the following solution for P1 (x, ν):I(x = 1 ∧ y = 0 ∧ x ̸= 0 ∧ ν = 1 + y, ¬ν = x) ≡ ν = x.
By substituting this for P1 in Ccopy , we get:
x=0∧ν =0P2 (x, ν)⇒⇒

P2 (x, ν)(x + 1 ̸= 0 ∧ z = 1 + ν ⇒ z = x + 1)

We then get, for example, the following solution for P2 (x, ν):type of the function that type-checks the multiple calling contexts,
while preserving the path- and context-sensitivity. In other words,
the extended method generates constraints from multiple infeasible
error paths (see Section 4.3.1), and tries to find the same solution(if possible) for related predicate variables (see Section 4.3.2).
4.3.1

Extensions of Constraint Generation

We extend the previous constraint generation algorithm overviewed
I(x = 0 ∧ ν = 0, ¬(x + 1 ̸= 0 ∧ z = 1 + ν ⇒ z = x + 1)) in Section 4.1.1 as follows.
• For each CEGAR iteration, we generate constraints from≡ ν = x.
multiple infeasible error paths instead of a single path: We keep
We thus obtain the following refinement types for Dcopy :the set {π1 , · · · , πn } of the infeasible error paths found so far,generate the set Ci of Horn clauses for each path πi , and pass
copy1 : (x : int → {ν : int | x = ν})
C = C1 ∪ · · · ∪ Cn to the extended constraint solving algorithm
copy2 : (x : int → {ν : int | x = ν})described in Section 4.3.2 as an input.
• We also construct and pass an equivalence relation E on the
4.2 Limitation of Previous Method
predicatevariables in C such that P E Q if and only if the predicate
We now explain the limitation of the previous method by using thevariables P and Q represent (possibly different) refinement predprogram in Figure 4. Let us consider the following SHP Dcc :icates for the same argument or return value of the same function
let copy1 x = assume (x<>0); 1 + copy2 (x-1)
in the original program. For example, we obtain the trivial equivalet copy2 x = assume (x=0); 0
lence relation Ecc = {P1 , . . . , P4 } × {P1 , . . . , P4 } for Ccc . The
let copy3 x = assume (x<>0); 1 + copy4 (x-1)
constraint solving algorithm in Section 4.3.2 exploits E to find genlet copy4 x = assume (x=0); 0
eral solutions for C.
let main n = assume (copy3 (copy1 n) <> n); failThus, the extended algorithm generates a pair (C, E) of Horn
The SHP corresponds to an infeasible error path where the elseclauses C for multiple paths and an equivalence relation E on
branch of copy is taken in the first and the third calls of copy, thethe predicate variables in C unlike the previous algorithm which
then-branch is taken in the second and the fourth calls of copy, andgenerates only Horn clauses for a single path. Here, the pair (C, E)
the assertion in the main function fails.
of constraints can be viewed as hierarchical constraints where C
For the SHP Dcc , we use the following type template: x : int →must be always satisfied and E should be satisfied if possible.
{ν : int | Pi (x, ν)} for each copyi. We get the following set Ccc
of constraints:
4.3.2 Extensions of Constraint Solving
x = 0 ∧ y = 0 ⇒ P2 (x, y)In this section, we extend the previous constraint solving algorithm
P2 (x − 1, y) ∧ x ̸= 0 ∧ z = 1 + y ⇒ P1 (x, z)
overviewed in Section 4.1.2. Given a pair (C, E) of Horn clauses
x = 0 ∧ y = 0 ⇒ P4 (x, y)
C and an equivalence relation E on the predicate variables in C,
P4 (x − 1, y) ∧ x ̸= 0 ∧ z = 1 + y ⇒ P3 (x, z)
the algorithm returns a substitution θ for the predicate variables in
P1 (n, x) ∧ P3 (x, y) ⇒ y = n
C such that θC is valid. A distinguishing feature of the algorithm isthat it tries to find the same solution for predicate variables related
By eliminating the other predicate variables than P3 (and withby E if possible. This enables the algorithm to obtain general
some simplification), we get the following constraints CP3 :predicates, which are more likely to constitute invariants.
x = 1 ∧ ν = 1 ⇒ P3 (x, ν)The extended constraint solving algorithm proceeds as follows:
P3 (x, ν) ⇒ (x = 1 ⇒ ν = 1)
1. Find a set S of predicate variables which are related by E
and may have the same solution in C.
Existing interpolating provers such as [4] returns the following
2. Find a candidate solution λe
x.ϕ for all predicate variable
solution for P3 (x, ν):Q ∈ S.
I(x = 1 ∧ ν = 1, ¬(x = 1 ⇒ ν = 1)) ≡ x = 1 ∧ ν = 1.
3. Substitute λe
x.ϕ for predicate variables S in C and repeat theentire procedure if the result still contains a predicate variable.
Note here that the solution is specific to the calling context ofthe particular function copy3, and cannot be used as a solution
Finding a set S of predicate variables: To find a set of predicate
for P2 and P4 . We here want to get more general solutions likevariables that may have the same solution in C, for each predicateλ(ν, x).ν = x which are more likely to constitute an invariant
variable P in C, we compute constraints CP from C by eliminatingof the function copy in the original program. For this purpose,the other predicate variables than P . For the running example Ccc ,we believe it is desirable to find the same solution (if possible)
we obtain:
for “related” predicate variables which represent (possibly differCP1 = {x = 1 ∧ ν = 1 ⇒ P1 (x, ν),ent) refinement predicates for the same argument or return value
P1 (x, ν) ⇒ (ν = 1 ⇒ x = 1)},of the same function in the original program. For the running exCP2 = {x = 0 ∧ ν = 0 ⇒ P2 (x, ν),ample Ccc , we want to get the same solution for P1 , . . . , P4 , andP2 (x, ν) ⇒ (ν = 0 ⇒ (x = −1 ∨ x = 0))},λ(ν, x).ν = x in fact satisfies this extra constraint.
CP3 = {x = 1 ∧ ν = 1 ⇒ P3 (x, ν),P3 (x, ν) ⇒ (x = 1 ⇒ ν = 1)},
4.3 Extended Method
CP4 = {x = 0 ∧ ν = 0 ⇒ P4 (x, ν),We now explain our extension of the previous method to remedy
P4 (x, ν) ⇒ (x = 0 ⇒ ν = 0)}.
the limitation discussed in Section 4.2. The extended predicate disLet {P1 , . . . , Pm } be the set of predicate variables in C. We
covery method is based on the framework of the previous method
pick an equivalence class S0 ∈ {P1 , . . . , Pm }/E (e.g., the largest
overviewed in Section 4.1, but the component for refinement typeone), and further classify S0 by using CP1 , . . . , CPm so that predinference is extended so that it can merge and generalize informaicate variables which never have the same solution are separated.
tion from multiple calling contexts of a function in multiple infeaFormally, we find S1 . . . , Sn such that:sible error paths. This enables MoCHi to infer a general refinement• S0 = S1 ∪ · · · ∪ Sn ,• ϕPi,1 ∨ · · · ∨ ϕPi,ℓ implies ϕ′Pi,1 ∧ · · · ∧ ϕ′Pii,ℓiProgram with control operations + recursive data structures

for each

CPS transformation (Section 5.2)i ∈ {1, . . . , n}, and• ϕPi,1 ∨ · · · ∨ ϕPi,ℓ ∨ ϕPj,1 ∨ · · · ∨ ϕPj,ℓ does not implyij′
ϕPi,1 ∧· · ·∧ϕ′Pi,ℓ ∧ϕ′Pj,1 ∧· · ·∧ϕ′Pj,ℓ for each i, j ∈ {1, . . . , n}ijsuch that i ̸= j.
Here, CP = {ϕP ⇒ P (ex), P (ex) ⇒ ϕ′P } and Si = {Pi,1 , . . . , Pi,ℓi }.
We then pick some S ∈ {S1 , . . . , Sn } (e.g., the largestone). For the running example Ccc , we get S = S0 = S1 ={P1 , . . . , P4 } since ϕP1 ∨ · · · ∨ ϕP4 implies ϕ′P1 ∧ · · · ∧ ϕ′P4 .
Finding a candidate solution λe
x.ϕ for S: We find a single candidate solution λe
x.ϕ for all the predicate variables Q1 , . . . , Qℓ ∈S by simultaneously solving CQ1 , . . . , CQℓ unlike the previous
method. Formally, we find ϕ such that:• ϕQ1 ∨ · · · ∨ ϕQℓ implies ϕ,• ϕ implies ϕ′Q1 ∧ · · · ∧ ϕ′Q , andℓ• FV (ϕ) ⊆ {ex}.
Here, CQi = {ϕQi ⇒ Qi (ex), Qi (ex) ⇒ ϕ′Qi }. We can compute
such a formula ϕ as an interpolant I(ϕQ1 ∨ · · · ∨ ϕQℓ , ¬(ϕ′Q1 ∧· · · ∧ ϕ′Qℓ )) but the three conditions of interpolants are not always
sufficient for our purpose to find general predicates. Actually, wewant to obtain as simple interpolant as possible with respect to thenumber of disjunctions. To this end, we propose a new heuristic
operator J that combines the interpolation I and convex hull
operators. Let us write H(ϕ) to denote the convex hull of ϕ. For
formulas ϕ1 and ϕ2 (such that ϕ1 and ϕ2 are inconsistent), the new
operator J (ϕ1 , ϕ2 ) is defined as follows:
I(H(ϕ1 ), H(ϕ2 )) (if H(ϕ1 ) ⊥ H(ϕ2 ))I(H(ϕ1 ), ϕ2 )(if ¬(H(ϕ1 ) ⊥ H(ϕ2 ))∧J (ϕ1 , ϕ2 ) =H(ϕ1 ) ⊥ ϕ2 )I(ϕ1 , ϕ2 )(otherwise)
Here, we write ϕ1 ⊥ ϕ2 to denote that ϕ1 and ϕ2 are inconsistent.
Note here that the use of the convex hull operator enables us toeliminate disjunctions in ϕ1 and ϕ2 , which are passed to an interpolating theorem prover. In the experiments reported in Section 6,
this often reduced the number of disjunctions in the output of theinterpolating prover, and hence makes the output more likely toconstitute invariants. Thus, we use the new operator J instead of I
to compute λex.J (ϕQ1 ∨· · ·∨ϕQℓ , ¬(ϕ′Q1 ∧· · ·∧ϕ′Qℓ )) as a candidate solution λe
x.ϕ for all the predicate variables Q1 , . . . , Qℓ ∈ S.
For the running example Ccc , we obtain, for example, the following
candidate solution λ(x, ν).ϕ for P1 , . . . , P4 :ϕ = J (ϕP1 ∨ · · · ∨ ϕP4 , ¬(ϕ′P1 ∧ · · · ∧ ϕ′P4 ))= I(H(x = ν = 0 ∨ x = ν = 1), ¬(ϕ′P1 ∧ · · · ∧ ϕ′P4 ))= I(0 ≤ x = ν ≤ 1, ¬(ϕ′P1 ∧ · · · ∧ ϕ′P4 ))≡ x=ν
Substituting λe
x.ϕ for S in C: We then substitute the candidate
solution λe
x.ϕ for S = {Q1 , . . . , Qℓ } in C. Note, however, that wecannot always substitute all the predicate variables in S with thecandidate solution λe
x.ϕ because Qi may depend on Qj for somei ̸= j. For example, let us consider the following constraints:
x = 0 ⇒ Q1 (x),Q1 (x) ⇒ Q2 (x + 1),

Q2 (x) ⇒ 0 ≤ x ≤ 2

From the constraints, we get:
CQ1
CQ2

=
=

{ν = 0 ⇒ Q1 (ν), Q1 (ν) ⇒ −1 ≤ ν ≤ 1},{ν = 1 ⇒ Q2 (ν), Q2 (ν) ⇒ 0 ≤ ν ≤ 2}.

Thus, we obtain, for example, J (ν = 0 ∨ ν = 1, ¬(−1 ≤ ν ≤1 ∧ 0 ≤ ν ≤ 2)) ≡ 0 ≤ ν ≤ 1 as a candidate solution forQ1 (ν) and Q2 (ν). However, [λν.0 ≤ ν ≤ 1/Q1 , λν.0 ≤ ν ≤1/Q2 ](Q1 (x) ⇒ Q2 (x + 1)) is not valid. Actually, it is only safe
to substitute λν.0 ≤ ν ≤ 1 for either Q1 or Q2 .

Program with recursive data structures
Encoding recursive data structures as functions on lists (Section 5.1.2)
Program with lists
Encoding lists as functions on integers (Section 5.1.1)
Program with integers
Verification (Our previous paper [15])Figure 10. The Verification Framework for Recursive Data Structures and Control Operators

Therefore, we find and substitute only a maximal nonempty
subset M of S for which we can safely substitute λex.ϕ (i.e.,{R 7→ λex.ϕ | R ∈ M }C is equi-satisfiable with C). For the running example Ccc , it is in fact safe to substitute the candidate solution λ(x, ν).x = ν for P1 , . . . , P4 (i.e., M = S). As a result of thesubstitution, all the predicate variables in Ccc are eliminated. Thus,
we obtain the refinement type x : int → {ν : int | x = ν} for allof copy1, . . . , copy4.

5.

Language Extensions

This section formalizes extensions of the target language of verification. Our approach is to translate a source program to a program that has no recursive data structures and no control operators,
in a sound and complete manner. Figure 10 shows the verification
framework for recursive data structures and control operators. Section 5.1 formalizes the encoding of recursive data structures, andSection 5.2 introduces the extension for control operations.
5.1 Functional Encoding of Recursive Data Structures
We first discuss encoding of lists, and then that of user-defined recursive data structures. We assume that the target language of encoding is equipped with tuples. The extensions of selective predicate abstractions and selective CPS transformation with tuples are
straightforward.
5.1.1

Functional Encoding of Lists

The idea is to encode a list into a pair of its length and a functionthat maps indices to the elements of the list. For example, the list
[2; 3; 5] is encoded into the pair (3, f ) where f (0) = 2, f (1) = 3,
and f (2) = 5. The primitive operations nil, cons, is nil, head,
and tail for lists are defined as follows.
let nil = (0, fun _ -> fail)let cons x (len,f) = (len+1,
λi. if i = 0 then x else f (i-1))
let is_nil (len,f) = len = 0
let head (len,f) = if len=0 then fail else f 0
let tail (len,f) =((if len=0 then fail else len-1), λi.f(i+1))
nil is translated into the pair of length 0 and the function thatalways fails. cons x xs is translated into the pair of its length andthe function {0 7→ x} ∪ {i 7→ f (i − 1) | i ̸= 0} where f is thefunction part of the encoding of xs. is nil just checks whether
len is 0 or not. head returns f(0), i.e. the first element of the list.
tail returns the pair of (len-1,f’) where f’(i) = f(i+1).
Note that we cannot use Church encoding for recursive data
structures, since Church encoding of data structures require recur-

sive or polymorphic types in general, which cannot be handled byhigher-order model checking.
Our approach has the following advantages. First, by encoding lists into functions over integers, we can reuse the predicate
abstraction/discovery for integers. Second, the encoding induces
a natural predicate abstraction of lists, which is general enough to
subsume various abstractions known in the literature, such as Dillig
et al.’s container abstraction [7]. With their abstraction method, alist is represented as {(v1 , P1 ), . . . , (vn , Pn )}, which means thej-th element is vi if Pi (j) holds. For example, {(0, true)} denotesthat all the elements are 0 and {(1, λi. i mod 2 = 0)} denotes thatthe even indexed elements are 1. By using our approach, the same
information can be represented as a refinement type (i : int) →{x : int | (P1 (i) → x = v1 ) ∧ · · · ∧ (Pn (i) → x = vn )}. For example, {(1, λi. i mod 2 = 0)} is represented as (i : int) →{x : int |i mod 2 = 0 → x = 1}. Moreover, our approach can deal withlist properties like “the i-th element of a list is greater than i,”which cannot be represented by the container abstraction. Thus,
our method is strictly more expressive.
5.1.2

Extension for Recursive Data Structures

We now discuss encoding of other recursive data structures. Programs with recursive data structures are translated into programswith lists by encoding recursive data structures to functions which
map paths of nodes to labels. Here, a path and a label are represented as a list of integers and an integer respectively. For example,
consider binary trees defined as follows.
type btree = Leaf | Node of btree * btree
A binary tree is encoded into a term of the type int list → int.5
For example, the tree node(leaf , node(leaf , leaf )) is encoded
into a function {[] 7→ node, [1] 7→ leaf , [2] 7→ node, [2, 1] 7→
leaf , [2, 2] 7→ leaf } where leaf and node are defined as some
integers. Here is another example.
match x with Constr1(x1, x2, ...) -> t
| Constr2(...) -> ...
The expression above is encoded to the following expression.
let Constr1 = 1 in ... let Constrn = n inmatch x nil with
Constr1 -> let x1 xs = x (cons 1 xs) in ...
let xn xs = x (cons n xs) in t’| Constr2 -> ...
Here, t’ is the encoding of t. The pattern matching on trees istranslated to that on labels, represented as integers. A subterm of atree is obtained by adding the index to the head of the path.
For recursive data types, we impose the restriction that recursive type variables cannot occur under function constructors. Thus, µα. unit + (int → int) ∗ α (which corresponds to(int → int) list) is OK, but neither µα. α → int nor µα. (int → α)
is allowed.
Let [[−]] be the encoding discussed above. The transformed
program is reduced to the same value as the original program:
Proposition 5.1 (Correctness of encoding). Let t be a term in a
program D. t −→∗D fail if and only if [[t]] −→∗D fail.
5.2

Extension for Control Operations

We can extend the framework to deal with control operations (e.g.,
exceptions and call/cc) by removing them from a program by
CPS transformation [17]. We do not support exceptions whichcarry function arguments, since the encoding of function-carrying
exceptions by CPS requires recursive types.
The following program calculates factorial and raises an exception if a negative number or zero is given.
5 Terms with this type is encoded to terms with type (int → int) → int

by the list encoding.

exception NotPos
letrec fact n = if n <= 0 then raise NotPos
else try n * fact (n - 1) with NotPos -> 1
let main n =try fact n with NotPos -> assert (n <= 0); 0
We can translate this program to an exception-free program by CPS
transformation as follows:
letrec fact n k exn =if n <= 0 then exn NotPos
else let exn’ e = match e with NotPos -> k 1 infact (n - 1) (fun r -> k (n * r))) exn’let main n k = fact n k (fun e ->match e with NotPos -> assert (n <= 0); k 0)
Once the exception is removed, we can apply our verification
method to the program.

6. Implementation and Preliminary Experiments
To evaluate the extended framework, we have implemented a prototype verifier for higher-order programs with lists and exceptions.
Our verifier uses TRecS [12, 13] as the underlying higher-ordermodel checker (for Step 3 in Figure 1), and uses CSIsat [4] for predicate discovery (in Step 5). CVC3 [2] is used for unsafety check (inStep 4) and predicate abstraction (in Step 1).
Table 1 shows the results of the experiments. The column “size”
shows the word counts of the program. The last column shows
the number of CEGAR-cycles and the running time measured. In
the last column, “C.”, “A.”, and “D.” denote the uses of selective
CPS transformation, selective predicate abstraction, and refinedpredicate discovery, respectively. The programs have been verified
correctly. The experiment was conducted on Intel Xeon 5570 CPU
with 8 MB cache and 6 GB memory. The implementation can betested and all programs are available at http://www.kb.ecei.
tohoku.ac.jp/~ryosuke/mochi/.
The programs used in the experiments are:
• “r-file” and above are the programs used in the experimentsin the previous paper [15].
• “sum intro”, “copy intro”, and “fact notpos” are the example
programs in Section 1 and Section 5.2.
• “map filter” and “risers” are examples of Ong and Ramsay’s
verification framework [19] for higher-order recursion schemewith a case construct listed at their web page http://mjolnir.
cs.ox.ac.uk/cgi-bin/horsc/recheck-horsc/input. Our
framework can verify these programs without a special treatmentof case constructs unlike in their framework.
• “search” is a program that manipulates user-defined data
structures.
• Other programs define generators of lists and functions onlists, and assert that the functions work correctly. For example,“zip” defines a function that takes two lists and returns a list ofcorresponding pairs. The function fails if the two arguments havedifferent lengths. “zip” asserts that zip xs xs never fails for all
integer lists xs.
• A program of name “xxx-e” is a buggy version of the program“xxx”.
The selective CPS transformation and the selective predicate abstraction reduced the time required for verification, and enabledverification of various programs including “a-cppr”, “zip”, and“map head filter”, which could only be verified by using both ofthem. Especially, the selective CPS transformation reduced the timerequired for higher-order model checking and the selective predicate abstraction reduced the number of CEGAR cycles as expected(recall their advantages discussed in Section 1). The refined predicate discovery (especially in combination with the selective predicate abstraction) enabled verification of not only “copy intro” butalso the list-manipulating programs “length”, “nth”, “risers”, andTable 1. Results of preliminary experiments
program
sum
mult
max
mc91
ack
a-cpprl-zipunzip
l-zipmaphorse-simplee-factr-lockr-filesum intro
copy intro
fact notpos
fold rightforall eq pair
forall leq
isnil
iter
lengthmem
nthnth0
harmonic
fold left
zip
map filter
riserssearchfold fun list
fact notpos-eharmonic-e
map filter-e
search-e

size
24
31
42
32
53
149
81
65
64
27
55
54
168
33
24
97
64
55
55
52
59
49
74
59
78
101
64
69
111
79
109
78
97
101
111
78

order
1
1
2
1
1
2
2
2
2
2
2
1
1
1
1
1
2
1
2
1
2
1
1
1
1
2
2
1
2
1
2
3
1
2
2
2

none
2, 0.125, 4.322, 0.197, 1.362, 0.43
1, 0.082, 0.136, 0.83
2, 0.173, 0.28
6, 17.54
3, 0.225, 3.463, 0.481, 0.120, 0.114, 8.10
5, 12.56

C.
2, 0.124, 53.67
5, 1.022, 0.205, 3.156, 0.442, 0.111, 0.072, 0.106, 0.3917, 27.87
2, 0.143, 0.258, 84.61
3, 0.20
7, 46.22
4, 0.703, 0.30
7, 4.20
1, 0.111, 0.162, 0.83
4, 0.91A.
1, 0.073, 0.141, 0.202, 0.18
1, 0.112, 0.141, 0.160, 0.06
2, 0.090, 0.08
10, 2.69
1, 0.072, 0.112, 0.452, 0.382, 0.362, 0.131, 0.183, 0.463, 0.26
1, 0.392, 0.394, 2.28
1, 0.090, 0.093, 2.162, 0.65“fold fun list” by finding general predicates for abstraction as discussed in Section 1. Note here that “fold fun list” is order-3 andthe other order-1 list-manipulating programs were transformed toorder-2 programs before verification by encoding lists as functions.
It is also worth noting that the columns “... & D.” show theexperimental results for the refined predicate discovery without
the feature of merging multiple infeasible paths enabled. The feature actually slowed down verification of some programs (such as“map filter”) but improved the analysis precision of MoCHi. In particular, the feature enabled us to verify the following accumulator
version of “length” in 0.36 seconds with 3 CEGAR-cycles:
let rec length acc xs = match xs with[] -> acc | _::xs’ -> length (acc+1) xs’
let rec make_list n =if n = 0 then [] else n :: make_list (n-1)
let main n = assert (length 0 (make_list n) = n)
For the success of verification, an abstraction predicate length(r) =length(acc) + length(xs) on the return value r and the arguments
acc and xs of length was essential. The predicate could only befound if the feature of merging multiple paths was enabled.

7.

Related Work

7.1

Verification of Higher-Order Programs with Recursive
Data Structures

Ong and Ramsay [19] proposed a verification method for functional
programs with recursive data structures, called Pattern Matching
Recursion Schemes (PMRS). The method cannot handle regularcycle, time [sec]C. & A.
D.
1, 0.082, 0.122, 0.134, 0.78
0, 0.08
5, 17.10
2, 0.182, 0.32
1, 0.104, 1.087, 4.412, 0.142, 0.117, 1.36
1, 0.072, 3.91
0, 0.06
1, 0.082, 0.102, 0.150, 0.076, 0.94
7, 0.92
1, 0.082, 0.183, 0.362, 0.113, 0.512, 0.221, 0.20
1, 0.192, 0.123, 0.35
1, 0.164, 1.423, 0.30
3, 0.224, 3.77
1, 0.202, 0.226, 24.16
3, 39.84
3, 0.71
1, 0.091, 0.120, 0.08
0, 0.110, 0.131, 0.18-

C. & D.
2, 0.114, 0.615, 1.182, 0.325, 0.504, 0.60
6, 0.59
2, 0.111, 0.072, 0.116, 0.392, 0.143, 0.35
3, 0.49
3, 0.222, 0.24
7, 17.83
3, 1.184, 1.00
7, 32.45
8, 15.49
1, 0.141, 0.192, 5.625, 6.00

A. & D.
1, 0.073, 0.183, 1.242, 0.401, 0.125, 1.883, 0.19
1, 0.160, 0.06
2, 0.110, 0.078, 3.19
1, 0.072, 0.142, 0.142, 1.04
2, 0.392, 0.33
2, 0.121, 0.212, 0.144, 0.614, 0.55
3, 0.28
1, 0.722, 0.79
7, 5.234, 5.468, 18.67
5, 4.65
2, 21.40
1, 0.090, 0.105, 7.65
2, 0.85

C. & A. & D.
1,
0.07
3,
0.17
0,
0.08
2,
0.39
1,
0.10
7,
2.03
2,
0.13
4,
0.23
1,
0.07
0,
0.06
2,
0.10
0,
0.08
6,
1.50
1,
0.08
2,
0.14
2,
0.12
2,
0.31
1,
0.22
1,
0.22
2,
0.12
1,
0.18
2,
0.14
4,
0.37
4,
0.42
3,
0.21
1,
0.25
2,
0.30
8,
22.17
3,
5.82
8,
9.78
8,
9.65
2,
2.74
1,
0.08
0,
0.08
0,
0.13
4,
1.50

properties (such as “a and b occur alternately”) and numericalproperties (such as “x + y ≤ z” where x, y, z are the length oflists).
Unno et al. [25] also proposed a verification method for higherorder tree processing functional programs, which is based on a verification method for higher-order multi-tree transducers [14]. Theirmethod can verify regular properties of recursive data structures
provided that certain invariant annotations are given.
There are several studies [5, 10, 11, 21, 24–28] that aim toinfer dependent types for higher-order programs with recursive
data structures. Rondon et al.’s liquid type inference [11, 21] is asemi-automated verification method that requires users to provide
templates of predicates, called logical qualifiers. The expressive
power of their method and ours is incomparable. They can deal
with “recursive dependent types”, such as int list≤ = µt. nil+ cons(x1 : int, {ν : int | x1 ≤ ν} t), which represents orderedlists of integers, while our method cannot. On the other hand, ourmethod can deal with the properties of list elements related to theirindices like “the i-th element of a list is greater than i,” while
they cannot. Unno and Kobayashi [24], and Jhala et al. [10] proposed a method for automated refinement type inference, wheretemplates of refinement types are first prepared and then constraints on unknown refinement predicates are generated. Unno andKobayashi [24] then solve the constraints by using an interpolating
theorem prover, and Jhala et al. [10] solves the constraints by a reduction to model-checking of first-order programs. Those methods
can deal with data structures such as lists and arrays as long as type

templates for the data structures are given a priori. Compared with
our “data structures as functions” approach, however, the supported
properties seem to be limited; for example, their method cannot reason about a relation between a list index and the corresponding element (like “the i-th element is greater than i”). Unlike our method,
the dependent type inference methods stated above [10, 11, 21, 24]
do not support refinement intersection types, which are necessary
for precise, context-sensitive analysis of higher-order functions.
Xi and Pfenning [26] proposed a dependently-typed language
Dependent ML. Its type system captures program properties suchas absence of array bounds errors and violations of data structure
invariants. Unlike our method, Dependent ML requires users toprovide dependent types of top-level functions.
7.2

Automated Verification of First-Order Programs with
Recursive Data Types

Chin et al. [5] proposed sized type inference. Their method infers
invariant of recursive functions by fixed-point computation. By abstracting lists as multisets, their method can deal with the inclusion
relation and the membership relation on lists. For example, their
method can verify that exists x xs returns true if and only if xs
has x as an element. The method, however, cannot properly handle
higher-order functions.
Suter et al. [23] proposed a verification method for first-orderfunctional programs that manipulate recursive data structures. Theyuse a decision procedure [22] that is complete for recursive functions that are sufficiently surjective catamorphisms. For example,
their method can verify that an insertion function preserves invariants of binary search trees, while our method cannot. On the other
hand, their method cannot deal with higher-order functions in acontext-sensitive way unlike our method.
Dillig et al. [7] proposed an automatic technique for staticallyreasoning about containers. The proposed method is based on an
abstract interpretation for containers. Their method is similar to our
method in the sense that they model containers as mappings fromlocations to values. They consider only a client-side use of specificdata structures (i.e. containers) such as primitive data structures andthose defined in a standard library. In contrast, our method candeal with user-defined data structures. Moreover, as discussed in
Section 5, our method is strictly more expressive than their method.
7.3

Path-sensitive Predicate Discovery

Beyer et al. [3] proposed a predicate discovery method for imperative programs. Like our method, theirs addresses the problem offinding general predicates in the context of a path-sensitive analysis. The method uses full-fledged programs (called path programs)
as counterexamples instead of infeasible error paths (or straightline
programs). A path program can be viewed as a set of finite paths
that are obtained by unwinding the path program. By synthesizing
invariants of a path program, their method prevents appearance of
infinite simple variations of infeasible error paths. Our method, in asense, generalizes theirs to path- and context-sensitive verificationof higher-order programs.

8.

Conclusion

We have proposed extensions and refinements to realize a scalable
software model checker for higher-order programs. We have identified the problems of the previous verification method, and proposed the optimization techniques to overcome the problems. We
have implemented a prototype verifier for higher-order programswith lists, which works well for several programs.
Acknowledgment
We would like to thank anonymous referees for useful comments. This work was partially supported by Kakenhi 24·8057 and23220001.

References[1] T. Ball and S. K. Rajamani. The SLAM project: debugging system
software via static analysis. In POPL 2002, pages 1–3, 2002.
[2] C. Barrett and C. Tinelli. CVC3. In CAV 2007, pages 298–302, 2007.
[3] D. Beyer, T. A. Henzinger, R. Majumdar, and A. Rybalchenko. Pathinvariants. In PLDI 2007, pages 300–309, June 2007.
[4] D. Beyer, D. Zufferey, and R. Majumdar. CSIsat: Interpolation for
LA+EUF. In CAV 2008, pages 304–308, 2008.
[5] W.-N. Chin, S.-C. Khoo, and D. N. Xu. Extending sized type withcollection analysis. In PEPM 2003, pages 75–84, 2003.
[6] E. M. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith.
Counterexample-guided abstraction refinement. In CAV 2000, pages
154–169, 2000.
[7] I. Dillig, T. Dillig, and A. Aiken. Precise reasoning for programs using
containers. In POPL 2011, pages 187–200, 2011.
[8] S. Graf and H. Saidi. Construction of abstract state graphs with PVS.
In CAV 1997, pages 72–83, 1997.
[9] T. A. Henzinger, R. Jhala, R. Majumdar, and G. Sutre. Lazy abstraction. In POPL 2002, pages 58–70, 2002.
[10] R. Jhala, R. Majumdar, and A. Rybalchenko. HMC: Verifying functional programs using abstract interpreters. In CAV 2011, pages 470–
485, 2011.
[11] M. Kawaguchi, P. M. Rondon, and R. Jhala. Type-based data structure
verification. In PLDI 2009, pages 304–315, 2009.
[12] N. Kobayashi. Types and higher-order recursion schemes for verification of higher-order programs. In POPL 2009, pages 416–428, 2009.
[13] N. Kobayashi. Model-checking higher-order functions. In PPDP
2009, pages 25–36, 2009.
[14] N. Kobayashi, N. Tabuchi, and H. Unno. Higher-order multiparameter tree transducers and recursion schemes for program verification. In POPL 2010, pages 495–508, 2010.
[15] N. Kobayashi, R. Sato, and H. Unno. Predicate abstraction and CEGAR for higher-order model checking. In PLDI 2011, pages 222–233,
2011.
[16] K. L. McMillan. An interpolating theorem prover. Theoretical Computer Science, 345(1):101–121, 2005.
[17] L. R. Nielsen. A selective CPS transformation. Electronic Notes in
Theoretical Computer Science, 45:311–331, 2001.
[18] C.-H. L. Ong. On model-checking trees generated by higher-orderrecursion schemes. In LICS 2006, pages 81–90, 2006.
[19] C.-H. L. Ong and S. J. Ramsay. Verifying higher-order functional
programs with pattern-matching algebraic data types. In POPL 2011,
pages 587–598, 2011.
[20] G. D. Plotkin. Call-by-name, call-by-value and the lambda-calculus.
TCS, 1(2):125–159, 1975.
[21] P. M. Rondon, M. Kawaguchi, and R. Jhala. Liquid types. In PLDI
2008, pages 159–169, 2008.
[22] P. Suter, M. Dotta, and V. Kuncak. Decision procedures for algebraic
data types with abstractions. In POPL 2010, pages 199–210, 2010.
[23] P. Suter, A. S. Köksal, and V. Kuncak. Satisfiability modulo recursive
programs. In SAS 2011, pages 298–315, 2011.
[24] H. Unno and N. Kobayashi. Dependent type inference with interpolants. In PPDP ’09, pages 277–288, 2009.
[25] H. Unno, N. Tabuchi, and N. Kobayashi. Verification of treeprocessing programs via higher-order model checking. In APLAS
2010, pages 312–327, 2010.
[26] H. Xi and F. Pfenning. Dependent types in practical programming. In
POPL 1999, pages 214–227, 1999.
[27] D. N. Xu. Hybrid contract checking via symbolic simplification. In
PEPM 2012, pages 107–116, Jan. 2012.
[28] D. N. Xu, S. Peyton Jones, and K. Claessen. Static contract checking
for haskell. In POPL 2009, pages 41–52, 2009.