Temporal Verification of Higher-Order Functional Programs
Akihiro Murase ∗Tachio Terauchi

Naoki Kobayashi

Nagoya University, Japanmurase@sqlab.jp

JAIST, Japanterauchi@jaist.ac.jp

University of Tokyo, Japankoba@is.s.u-tokyo.ac.jp

Ryosuke Sato

Hiroshi Unno

University of Tokyo, Japanryosuke@kb.is.s.u-tokyo.ac.jp

University of Tsukuba, Japanuhiro@cs.tsukuba.ac.jp

Abstract
We present an automated approach to verifying arbitrary omegaregular properties of higher-order functional programs. Previous
automated methods proposed for this class of programs could only
handle safety properties or termination, and our approach is the firstto be able to verify arbitrary omega-regular liveness properties.
Our approach is automata-theoretic, and extends our recent
work on binary-reachability-based approach to automated termination verification of higher-order functional programs to fair termination published in ESOP 2014. In that work, we have shown thatchecking disjunctive well-foundedness of (the transitive closureof) the “calling relation” is sound and complete for termination.
The extension to fair termination is tricky, however, because thestraightforward extension that checks disjunctive well-foundednessof the fair calling relation turns out to be unsound, as we shall show
in the paper. Roughly, our solution is to check fairness on the transition relation instead of the calling relation, and propagate the information to determine when it is necessary and sufficient to checkfor disjunctive well-foundedness on the calling relation. We provethat our approach is sound and complete. We have implemented a
prototype of our approach, and confirmed that it is able to automatically verify liveness properties of some non-trivial higher-orderprograms.
Categories and Subject Descriptors D.2.4 [Software Engineering]: Software/Program Verification—Formal methods, Modelchecking; F.3.1 [Logics and Meaning of Programs]: Specifying
and Verifying and Reasoning about Programs—Assertions, Invariants, Mechanical verfication; F.3.2 [Logics and Meaning of Programs]: Semantics of Programming Languages—Program analysis; F.4.1 [Mathematical Logic and Formal Languages]: Mathematical Logic—Temporal logic
General Terms

Algorithms, Languages, Theory, Verification∗ Author’s current affiliation: Toshiba Solutions, Japan

Keywords Automatic Verification, Temporal Properties, HigherOrder Programs, Automata-Theoretic Verification, CEGAR, Binary Reachability Analysis

1. Introduction
Recent years have witnessed a significant progress in techniques
for automatically verifying higher-order functional (or, procedural)programs. Besides the purely theoretical interests, the progress ismotivated in part by the desire to verify real world programs that
contain higher-order functions (e.g., programs written in functional
languages such as OCaml [13, 17, 27, 32–34] and Haskell [36, 37]),
and also in part by the observation that higher-order functions
can be used to (often concisely) model advanced programming
language features, such as recursive data structures, exceptions, andcontinuations, thus turning the verifiers for higher-order functional
programs into verifiers for programs containing such features [28].
For the case the data is finite and the program is well-typed,
Ong and others [9, 16, 21–23] have presented algorithms for verifying arbitrary modal-µ temporal properties of higher-order functional programs. However, for the infinite data case, the current
state-of-the-art methods are limited to either only safety properties [13, 17, 27, 32–34, 36, 37] or termination [10, 15, 20, 29].
This is in stark contrast to imperative programs which have appropriated effective automated techniques for verifying an expressive
range of temporal properties [2–5]. To rectify the situation, this paper presents the first approach to automatically verifying arbitraryω-regular temporal properties of (possibly untyped) infinite data
higher-order functional programs. (Recall that an ω-regular property is a set of infinite words recognized by a Büchi automaton, andincludes any property expressible by linear temporal logic.) Next,
we give an informal overview of our approach.
1.1 Informal Overview
Our approach follows the automata-theoretic framework [35], andreduces the temporal property verification to verifying that the
program has no infinite fair execution traces (i.e., fair termination).
To verify fair termination for higher-order functional programs, webuild on our recent work [20] on (plain) termination verification
for higher-order functional programs. Next, we briefly overview themain ideas of [20]. We abbreviate a sequence w1 , . . . , wk to we andwrite |w|e for the length of the sequence w
e below.
The approach taken in [20] adopts the binary reachability analysis (BRA) method that was originally proposed by Cook et al. fortermination verification of imperative programs [6]. Recall that abinary relation is said to be disjunctively well-founded if it is a finite union of well-founded relations. Let Trans P be the transition

relation of a program P (i.e., (e, e′ ) ∈ Trans P if and only if e
and e′ are states occurring in an execution of P such that there isa transition from e to e′ ). P is terminating if and only if Trans +P
is disjunctively well-founded [26] (we write R+ for the transitive
closure of the binary relation R), and [6] presents an automatic
method, the BRA approach, which checks the latter by an iterative
reduction to plain reachability verification problems.
As remarked in previous literature on BRA [6, 20], advantagesof the BRA approach over the other approaches to termination
verification are that termination arguments can be flexibly adjusted
for each program, and that precise flow information can be taken
into account in the plain reachability verification phase. The latteradvantage is particularly important since the termination property
often depends on safety properties.
Whereas BRA for imperative programs checks disjunctive wellfoundedness of the transitive closure of the transition relation, thekey idea in [20] is to check that of the calling relation. Moreformally, a calling relation Call P is the set of pairs (f w,e gev)
where f w
e and g ve are total applications that occur in an executionof P such that the call g ve is made from f w.
e 1 A key result provedin [20] is that P is terminating if and only if Call +P is disjunctively
well-founded. (We underscore that the calling relation is over theactual calls that happen in the program execution, and not “static”
call sites that appear in the program text.)
In principle, checking disjunctive well-foundedness of (the transitive closure of) the transition relation is sound and complete fortermination even for higher-order functional programs (i.e., themethod proposed by [6, 26] is language agnostic because any program can be considered a transition system). The advantage of using the calling relation instead of the transition relation is that it
avoids the need to explicitly reason about the change in the calling
context (i.e., the call stack). For example, recall the definition of the
Ackermann function:ac m n = if m = 0 then n + 1
else if n = 0 then ac (m − 1) 1
else ac (m − 1) (ac m (n − 1))
Let P be a program that calls ac with some non-negative arguments. P is terminating, and there is a simple termination argument (i.e., disjunctively well-founded relation containing the transitive closure of the calling relation) sufficient to prove termination:
D1 ∪ D2 where
D1 = {(ac m n, ac m′ n′ ) | m > m′ ∧ m′ ≥ 0}
D2 = {(ac m n, ac m′ n′ ) | n > n′ ∧ n′ ≥ 0}
Indeed, Call +P ⊆ D1 ∪ D2 because any (transitive) recursive callto ac either decreases on the first argument or the second argument.
However, the transition relation of the program is quite complex, as
seen below in the transition sequence given m, n > 0.
ac m n → ac (m − 1) (ac m (n − 1))→ ac (m − 1) (ac (m − 1) (ac m (n − 2)))..
.
→ ac (m − 1) (ac (m − 1) (. . . , (ac m 0) . . .))→ ac (m − 1) (ac (m − 1) (. . . , (ac (m − 1) 1) . . .))..
.
Consequently, the required termination argument also becomes
more complex. In general, the complexity comes from the need toreason about changes in the calling context (e.g., a program terminates because the number of pending callers on the call stack
decreases), and hence avoiding such a reasoning by using the call1 We assume that the program is lambda-lifted [14] so that all function
definitions occur (mutually recursively) at the top level.

fn
f0

f1
f0

f1
f0

..
.

Figure 1. The graph of Call Pex .
ing relation instead of the transition relation is crucial to practicalverification.2
We remark that the above example is only first-order, andthat things become even more intricate when we move to higherorder. A contribution of [20] shows that checking disjunctive wellfoundedness on the transitive closure of the calling relation is soundand complete even in the presence of higher-order functions.
Extending to Fair Termination. In this work, we extend the approach of [20] to fair termination. Recall that an infinite sequence
π is said to be fair with respect to a Streett fairness constraint
C = {(p1 , q1 ), (p2 , q2 ), . . . , (pn , qn )} if for each (pi , qi ) ∈ C,
either pi is true for only finitely many elements of π or qi is true
for infinitely many elements of π. P is said to be fair terminating
under C if P has no infinite execution trace that is fair with respect
to C.
We call a finite sequence ̟ fair with respect to C if for each(pi , qi ) ∈ C, either pi is false for all elements of ̟ or qi is true
for some element of ̟. For a binary relation R, let RfairC (+) ={(̟(1), ̟(|̟|)) | ̟ ∈ paths (R) ∧ ̟ is fair wrt. C} where
paths(R) = {̟ | ∀i.1 ≤ i < |̟| ⇒ (̟(i), ̟(i + 1)) ∈ R}.
Intuitively, RfairC (+) is the subset of R+ that only considers thesequences of transitions that are fair with respect to C. Using a
result in a paper by Pneuli et al. [24], Cook et al. [2] have shown
fair (+)
that P is fair terminating under C if and only if Trans P C
fairC (+)
(i.e., Rwith R = Trans P ) is disjunctively well-founded.
The latter result is then used to obtain a BRA approach to soundand complete automatic fair-termination verification of imperative
programs.
Knowing the result for the plain termination case shown by [20],one may be lead to believe that the result of [2] can be applied
directly to obtain the following scheme for checking fair termination of higher-order functional programs: check disjunctive wellfoundedness of fair sequences of calling relations. That is, checkfair (+)
that Call P C
is disjunctively well-founded. However, perhaps
somewhat surprisingly, the approach turns out to be unsound.3 To
see this, consider the program Pex that starts by calling the following function f with a positive argument:f x = if x ≤ 0 then ()else (f 0); (f 1)
Let C = {(true, f 0)}, that is, f is called with the argument
0 infinitely often in an execution that is fair with respect to C.
Clearly, Pex is not fair terminating under C since any executionof Pex is non-terminating and contains infinitely many calls to
2 In fact, the set of functional programs that can be proved terminatingby disjunctive well-foundedness on the transitive closure of the calling
relation is strictly larger than the set that can be proved by that of thetransition relation, for a class of termination arguments such as linear
ranking functions [1, 38].
3 For simplicity, this section restricts state predicates to function applications. Section 2 introduces more general events that can be used to express
arbitrary ω-regular temporal properties of program states. A similar issue
applies in that setting.

fair (+)

is disjunctively
f with the argument 0. Nonetheless, Call PexC
well-founded. Indeed, it can be seen from Figure 1 which shows
the graph of Call Pex (i.e., Pex ’s call tree [20]) that any infinite
path in Call Pex is unfair with respect to C.
The solution we propose in this paper is to decide when atransition sequence is fair by inspecting the transition relation,and use that information to decide when we should check for
disjunctive well-foundedness of the calling relation. More formally,let →P be the one-step transition of P and RP be the set of states
reachable from an initial state of P . Note that we have:+ ′′Trans +
P = {(e, e ) | e ∈ RP ∧ e →P e }fairC (+)
fair (+) ′′Trans P= {(e, e ) | e ∈ RP ∧ e →P C
e}+′Call P = {(f w,
e gev ) | E[f w]e ∈ RP ∧ f we →+e]
P E [g v∧ arity(f ) = |w|e ∧ arity(g) = |ev |}where E and E ′ are evaluation contexts. Let the relation ⊲C
P bedefined as follows.
fair (+)⊲Ce g ve) | E[f w]e ∈ RP ∧ f w
e →P CE ′ [g ve]
P = {(f w,∧ arity(f ) = |w|e ∧ arity(g) = |e
v |}

+
+
That is, ⊲C
P is the above characterization of Call P but with →P
fairC (+)
replaced by →P. The main result of the paper (Theorem 3.1)
shows that P is fair terminating under C if and only if ⊲C
P is disjunctively well-founded. Thus, the verification method we propose
in this paper checks for the disjunctive well-foundedness of ⊲C
P . Aswith the work on plain termination which checks the disjunctive
well-foundedness of Call +P [20], an important advantage of thisapproach is that it avoids the explicit reasoning about changes in
the calling context.
As an example, recall the program Pex from above. Let C ={(true, f 0)} again. Recall that Pex is not fair terminating under C.
Indeed, ⊲C
Pex is not disjunctively well-founded because there is an
infinite sequence:CC
f n ⊲CPex f 1 ⊲Pex f 1 ⊲Pex . . .
+This follows because f 1 →+Pex (f 0); (f 1) and (f 0); (f 1) →Pex
fairC (+)
f 1.
f 1, and therefore f 1 →Pex
As a fair terminating example, consider Pex again, but this timewith respect to the fairness constraint C ′ = {(f 0, false)}. That is, f
is called with 0 only finitely often in a trace fair with respect to C ′ .
Pex is fair terminating under C ′ , because any infinite execution ofPex is unfair, i.e., it contains infinitely many f 0 calls. We can show′
C′that ⊲C
Pex is disjunctively well-founded. In fact, ⊲Pex = ∅ because
fairC ′ (+)
fairC ′ (+)
f n 6→Pexf i and f 1 6→Pexf i for i ∈ {0, 1}.
As also done in [20], we take advantage of the fact that disjunctive well-foundedness of a calling relation can be checked perfunction basis. That is, let f1 , . . . , fn be the functions defined in
P . Then, ⊲C
P is disjunctively well-founded if and only if for eachfi , RECP,C (fi ) = {(w,e ve) | fi we ⊲Ce} is disjunctively wellP fi v
founded.

Overall Flow of Verification. As in previous work on plain or fairtermination verification via BRA [2, 6, 20], we solve the disjunctive
well-foundedness checking problem in a counterexample-guided
manner. That is, we start with some candidate termination argument (i.e., disjunctively well-founded relation) D. Then, we checkif the candidate is an actual termination argument (i.e., whether
RECP,C (fi ) ⊆ D holds) by a reduction to reachability checking,and if not, we update the candidate via a counterexample analysis
and repeat.
Figure 2 shows the overview of the overall verification process.
Step 1 is a program transformation that reduces the candidate
termination argument checking problem soundly and completely
to reachability checking, and is a key technical contribution of

Program: P
Fairness Constraint: C

RECP,C (f ) is disjunctively well-founded
Safe

Step 1: Program
Transformation(Section 4)⌈P ⌉f,D,C

Step 2: Reachability
Checking [17, 32, 34]
Counterexample

Candidate D

Step 3: Termination
Argument Inference [20]Fail
P may not fair terminate under C

Figure 2. Overview of the verification process.
the paper. The step builds a transformed program ⌈P ⌉f,D,C thatis assertion safe if and only if RECP,C (f ) ⊆ D (Theorem 4.1).
The program transformation adopts ideas from those proposed in
the previous work [2, 20]. Namely, it uses the idea from [2] todetect when a sequence of transitions is fair, and uses the ideafrom [20] to check that the calling relation over such sequences
is contained in the candidate D. Section 4 describes the formal
details of the program transformation. The reachability checking(Step 2) is standard, and we refer to the previous work [17, 32,
34] for details. We use the approach proposed in [20] for the
candidate termination argument inference (Step 3), and we givea brief overview of the process below. We have implemented a
prototype of our verification method, and we show that it is able
to verify non-trivial liveness properties of higher-order functional
programs.
In summary, our contributions are: (i) The first sound and complete approach to verification of arbitrary ω-regular properties of
infinite data higher-order functional programs. Our approach combines and extends ideas from previous work on plain termination
verification for high-order functional programs [20] and fair termination verification for imperative programs [2] in a non-trivial
way. (ii) Experiments with a prototype implementation to show theeffectiveness of our approach.
On Soundness and Completeness. As in previous work on BRA,
the soundness and completeness of our approach are relative to thesoundness and completeness of the backend reachability checking
and candidate termination argument inference. More precisely, ourapproach is sound if the reachability checking is sound and only
disjunctively well-founded relations are inferred as candidate termination arguments, and it is complete if the reachability checking
is complete and the candidate termination argument inference always infers some relation given a spurious counterexample.
We note that the relative soundness and completeness are thanks
to the fact that the BRA approach reduces the problem of verifying(plain or fair) termination to that of verifying plain reachability
without any loss of precision. As remarked before, this is importantfor verification in practice as termination properties often dependon safety properties.
Termination Argument Inference. We give a brief overview of
the termination argument inference process. A counterexample returned by the reachability checker (cf. Step 2 of Figure 2) is a pathof the transformed program ⌈P ⌉f,D,C from the initial state to an
assertion error. That is, it is a finite sequence of (symbolic) executions ̟ of ⌈P ⌉f,D,C such that {(w,e ve) | J̟K(w,e ev )} 6⊆ D where

J̟K is the strongest post condition of ̟. (We refer to a previous
work [17] for details on how counterexamples can be generated ina reachability checker for higher-order functional programs.)
By the soundness of the program transformation (Theorem 4.1),
this implies that{(w,e ev ) | J̟K(w,e ve)} ⊆ RECP,C (f ) 6⊆ D

assuming that the reachability checker is sound. Then, via a
constraint-based ranking function inference method [7, 25], we
infer a disjunctively well-founded relation D′ such that {(w,e ve) |J̟K(w,e ve)} ⊆ D′ . If no such a relation is found,4 then we halt theverification process by outputting “P may not fair terminate underC”. Otherwise, we obtain D ∪ D′ as the updated candidate termination argument to be given to Step 1 of Figure 2, and continue theverification process.
As also observed in [20], higher-order functional programs
sometimes require termination arguments that are over function
values. However, the ranking function inference methods are typically restricted to first-order values (e.g., only inferring linear ranking functions over integers). Hence, to handle such a case, [20] proposes an approach where first-order implicit parameters are added
to the (transformed) program so that higher-order termination arguments can be expressed as those over the implicit parameters. The
technique can be adopted straightforwardly to this work’s setting
to handle higher-order termination arguments.
Disproving Fair Termination. As in previous work on plain orfair termination verification via BRA [2, 6, 20], our method is notsuited for disproving fair termination, i.e., for showing that there
is an infinite fair execution sequence. (Assuming the reachability
checker and the termination argument inference are complete), ourmethod is able to prove simple cases of fair non-termination, suchasfair (+)

f 1 →PexC

fair (+)

f 1 →PexC

fair (+)

f 1 →PexC··· ,because in this case, RECP,C (f ) contains (1, 1). Our method cannot, however, detect a non-looping non-termination, likefair (+)

f 1 →PexC

fair (+)

f 2 →PexC

fair (+)

f 3 →PexC··· .

Given a program that contains such a non-looping infinite execution sequence, the counterexample-guided refinement loop of Figure 2 would diverge (assuming the reachability checker is soundand complete and the termination argument inference is complete).
For disproving fair termination of higher-order programs, we can
extend the recently proposed method for disproving plain termination of higher-order programs [19]. We will discuss it in a separate
paper, since the method is quite different from and orthogonal tothe one discussed in the present paper.
Paper Organization. The rest of the paper is organized as follows.
We discuss related work next. Section 2 presents the target programming language and relevant preliminary concepts. Sections 3
and 4 contain the formal details of the reduction from fair termination to reachability checking which is the main technical contribution of the paper. Section 3 formalizes the characterization of fairtermination for higher-order functional programs as checking disjunctive well-foundedness of ⊲C
P (i.e., checking RECP,C (f ) is disjunctively well-founded for every f in P ) , and Section 4 describes
the program transformation that reduces the problem of checking
if RECP,C (f ) is contained in the given candidate termination argument to reachability checking. Section 5 reports on a preliminary
4 This occurs either when RECv, ve) for some ev, or when aP,C (f ) ∋ (edisjunctively well-founded relation D ′ does exist but is not found due tothe incompleteness of the ranking function inference. In the former case,
we can actually conclude that P does not fair terminate.

e ::= v | event A | rand() | v1 op v2 | v1 v2| if v then e1 else e2 | let x = e1 in e2
v ::= c | x | hx v1 · · · vk i
Figure 3. Source language: syntax
implementation and experiment results, and Section 6 concludes
the paper.
1.2 Related WorkTo our knowledge, this paper is the first to propose a sound andcomplete approach to automatically verifying arbitrary ω-regularproperties of infinite data higher-order functional programs. As remarked before, previous work on automated methods for higherorder functional programs are limited to (typed) finite data programs [9, 16, 21–23], or termination [10, 15, 20, 29] and safety
properties [13, 17, 27, 32–34, 36, 37] for infinite data programs.
A notable exception to the above is the work by Skalka etal. [30, 31] that proposes a type-and-effect system for verifying arbitrary ω-regular properties of higher-order functional programs. In
their approach, a type-and-effect system is used as a static analysis to obtain a sound finite-state abstraction of the program. Then,a model checker (for finite state systems) is used to check the abstraction against the given temporal property. Because of the overapproximation, the approach is incomplete and somewhat imprecise. In particular, any recursive call will be abstracted as an unbounded loop which makes it difficult to be used for deducing nontrivial liveness properties.
Related to Skalka et al.’s work is the recent work by Hofmann
and Chen [11] that proposes a similar type-and-effect system. Theirwork shows a close correspondence between the type-and-effectsystem and automata theoretic concepts, and shows that the system
is sound and complete for ω-regular property verification of simple finite data first-order functional programs without conditional
branches. It is unclear if the system can be extended to higher-orderfunctions (the paper briefly sketches such an extension) or infinitedata.
In a recent work [18], Koskinen and Terauchi have proposed aframework for verifying arbitrary ω-regular properties of infinite
data higher-order functional programs in a compositional manner.
However, their paper does not discuss automation, and moreover,
the approach requires an external “oracle” verifier to deduce nontrivial liveness properties (the approach is sound and complete relative to the soundness and completeness of the oracles). Our work
is complementary to theirs in the sense that the verifier proposed
here can be put to use as an oracle in their framework.

2. Source Language
The sets of expressions and values, ranged over by e and v respectively, are defined by the grammar shown in Figure 3. Here,c ranges over the set of constants (including integers and the unit
value ⋆), op ranges over the set of binary operators, and x overthe set of variables. We write true and false for 1 and 0 respectively. We write JopK for the semantics of the operator op. The
value hx v1 · · · vk i expresses a function closure; it occurs only
at run-time. We write [v1 /x1 , . . . , vi /xi ]e for the capture-avoiding
parallel substitution of v1 , . . . , vi for x1 , . . . , xi in e.
In the formal syntax of expressions above, we restrict the positions where effectful expressions may occur. For readability, we
often write (especially in examples) if e0 then e1 else e2 forlet x = e0 in if x then e1 else e2 , and f e1 · · · en forlet x1 = e1 in · · · let xn = en in f x1 · · · xn , etc. We also
write e1 ; e2 for let x = e1 in e2 when x does not occur in e2 .

A

(E-E V)E[event A] −→P E[⋆]
n : an integer{(A1 , B1 ), . . . , (An , Bn )}.
(E-R AND)ǫE[rand()] −→P E[n]v1 JopK v2 = v(E-O P)ǫ

E[v1 op v2 ] −→P E[v]
ǫE[f ] −→P E[hf i](E-C LOS 0)i < arity(f )ǫE[hf v1 · · · vi−1 ivi ] −→P E[hf v1 · · · vi i]
f x1 · · · xi = e ∈ D

i = arity(f )ǫE[hf v1 · · · vi−1 ivi ] −→P E[[v1 /x1 , . . . , vi /xi ]e]A (Streett) fairness constraint C is a set of event pairs:(E-C LOS 1)(E-C ALL)n 6= 0ǫE[if n then e1 else e2 ] −→P E[e1 ]ǫE[if 0 then e1 else e2 ] −→P E[e2 ]ǫE[let x = v in e] −→P E[[v/x]e](E-I F T)(E-I F F)(E-L ET)

Figure 4. Source language: reduction relation

Intuitively, it describes the fairness constraint that if Ai occurs
infinitely often, Bi must also happen infinitely often.
Remark 2.1 Usually, a fairness constraint is of the form{(p1 , q1 ), . . . , (pn , qn )}where pi , qi are sets of states, meaning “whenever one of the statesin pi is visited infinitely often, one of the states in qi must also be
visited infinitely often.” In our language, a single event Ap can beused to express the property that one of the states in p is visited;
hence, a fairness constraint has been defined above as a set of pairsof events, rather than as a set of pairs of “sets of” events.
Definition 2.1 Let C be {(A1 , B1 ), . . . , (An , Bn )}, and σ be apossibly infinite sequence of events. We write σ |= C when, forevery i ∈ {1, . . . , n}, if Ai occurs infinitely often in σ, so does
Bi .
Definition 2.2 Let C be {(A1 , B1 ), . . . , (An , Bn )}. A program P
is fair terminating under C if, for every infinite reduction sequence
ℓ

ℓ

ℓ

3
2
1
→
→
main ⋆ −→P ··· ,
P e2 −
P e1 −A program P is a set of function definitions of the form:
f x1 · · · xk = e.
We write arity(f ) for the number of formal parameters, i.e., k. We
assume that P contains the definition of the special “main” function
main that takes a unit value and (if terminates) returns a unit value.
The set of evaluation contexts, ranged over by E, is given by:
E ::= [ ] | let x = E in e.
ℓ

The labeled reduction relation e −→P e′ , where ℓ is either an
event or an empty sequence ǫ, is defined by the rules shown in
Figure 4. We often omit P and ǫ in the reduction relation.
ℓ1ℓ1 ···ℓn ∗ℓn
We write −−−−→P for the relational composition −→P · · · −→P .
Let σ = ℓ1 ℓ2 ℓ3 · · · be a possibly infinite sequence of labels. We
σ ∗write e −→P if there exists a (possibly infinite) sequence of expressions e1 , e2 , . . . such that
ℓ

ℓ

ℓ

3
2
1
→
→
e −→
P ···
P e2 −
P e1 −

with σ = ℓ1 ℓ2 ℓ3 · · ·.
Example 2.1 The example on the function f in Section 1 is expressed as the following program Pex :f x = if x < 0 then ⋆ else
if x = 0 then event A else (f 0); (f 1)
main y = let x = rand() in f xHere, we have inserted event A to capture the event that f 0 iscalled.
✷Example 2.2 Let Prep be the program consisting of the following
function definitions.
repeat g = let x = rand() in g x; repeat g
f x = if x > 0 then f (x − 1) else event A
main y = repeat f
The program repeatedly calls f with a random integer value as anargument. Since each call of f eventually raises an event A, theprogram never terminates and raises A infinitely often.
✷ℓ1 ℓ2 ℓ3 · · · |= C does not hold.
In other words, a program is fair terminating if there is no infinite
fair reduction sequence.
Vardi [35] has shown that verification of arbitrary ω-regular
temporal properties can be reduced to that of fair termination. We
give below some examples of reductions. Here we assume thatthe body of every function definition starts with event Call,so that every infinite reduction sequence contains infinitely may
occurrences of the event Call. Assume also that a special event
Never never occurs in programs.
• Let C be {(A, Never)}. Then a program P is fair terminating

under C if and only if A occurs infinitely often in any nonterminating run of P . Indeed, if P is fair terminating, then thefairness constraint C must be violated by any infinite run of the
program, which implies that A must occur infinitely often. To
see the converse, we consider the contraposition. Suppose thatthe program is not fair terminating, i.e., there is a fair, infinite
σ ∗reduction sequence main ⋆ −→P . Then σ |= C, which implies
that either (i) A occurs only finitely often or (ii) both A and
Never occurs infinitely often. The latter cannot be the case by
the assumption on Never; hence A occurs only finitely often.
• Let C be {(A, Never), (Call, B)}. Then a program P is fairterminating under C if and only if, for every infinite run of P ,if B occurs infinitely often, so does A. To see why, notice that
C is violated just if either (A, Never) or (Call, B) is violated.
Since Never never happens and Call occurs infinitely often,(A, Never) being violated means that A occurs infinitely often,and (Call, B) being violated means that B occurs only finitely
often.
• Let P ′ be the program obtained from a program P by replacing

event Call with:
if flag then event CallA else event Call.
Here, flag is a state variable (which is added as an additional parameter of each function) that expresses whether
A has happened before. Then, P ′ is fair terminating under{(CallA , Never)} if and only if A occurs eventually in every
infinite run of P .

• Let P ′ be the program obtained from a program P by replacing

the definition of the main function: main x = e withmain x = e; loop ⋆loop x = event Never; loop x
Then P ′ is fair terminating under {(Call, Never)} if and only
if P never terminates.
Remark 2.2 In general, given the program P and the ω-regular
temporal property φ to be verified, the automata-theoretic approach [35] builds an ω-automaton A¬φ that recognizes the complement of φ, and verifies that the product program P×A¬φ has no
infinite runs. This is a fair-termination problem because the fairness
constraint from A¬φ is carried over to the product program.
Note that the use of Streett fairness constraints in our work
stipulates that A¬φ is represented by a Streett automaton. Streettautomata are preferred over Büchi automata in our setting because
a non-deterministic Büchi automaton is required to express an ωregular property in general which complicates our approach.
Remark 2.3 Our source language is untyped. Therefore, a program
evaluation may get stuck, and we consider a reduction sequencethat ends with a stuck expression as terminating. Our approach issound and complete even for untyped languages. But, our implementation currently supports only the typed subset because it uses
a higher-order program model checker for a typed language [17] as
the backend reachability checker.

3. Fair Termination Verification via (Fair) Binary
Reachability
This section reduces the verification of fair termination to that ofa binary reachability problem. Our notion of binary reachability,
which we call fair binary reachability, is an extension of the one
we proposed for plain termination verification [20]. Unlike in thestandard binary reachability for imperative programs [26], we track
only the relationship between the arguments of function calls in thecalling relation (cf. Section 1.1).
Definition 3.1 Let σ be a sequence of events, and let C ={(A1 , B1 ), . . . , (An , Bn )} be a fairness constraint. We write
σ |=fin C if, for every i ∈ {1, . . . , n}, either (i) Ai does notoccur in σ or (ii) Bi occurs in σ.
Definition 3.2 Let P be a program, f a function defined in P ,and C a fairness constraint. We write f ve ⊲C
e if there exP gw
σ1 ∗ist σ1 , σ2 , E1 , E2 such that: (i) main ⋆ −→e (ii)P E1 [f w],
σ2 +
E
[g
v
e
],
(iii)
σ
|=
C,
and
(iv)
arity(f
)
= |w|
e
fw
e −→
2
2
fin
P
and arity(g) = |ev |. We write RECP,C (f ) for the set{(w,e ve) | f w
e ⊲C
e},
P f v

disjunctively well-founded relation Df for each function f , andshow that RECP,C (f ) ⊆ Df . We call the problem of proving
RECP,C (f ) ⊆ Df a fair binary reachability problem. How to solve
the fair binary reachability problem is discussed in Section 4.
Example 3.1 Recall Example 2.2. To check that Prep raises events
A infinitely often, it suffices to verify
RECP,C (f ) ⊆ Df
RECP,C (repeat ) ⊆ Drepeat
RECP,C (main) ⊆ Dmain
for C = {(A, Never)}, Df = {(m, n) | m > n ≥ 0}, andDrepeat = Dmain = ∅. Note that RECP,C (repeat ) = ∅ because,σ ∗whenever repeat f −→ E[repeat f ], σ contains A, so that
σ 6|= C.
✷The rest of this section is devoted to the proof of Theorem 3.1,
which is divided into Theorems 3.2 and 3.3 below.
Theorem 3.2 (Soundness) If RECP,C (f ) is well-founded for every
function f in P , then P is fair terminating.
Proof The proof is by contradiction. Suppose that RECP,C (f ) is
well-founded for every function f in P , but P is not fair terminating, i.e., there exists an infinite reduction sequence π that is fair.
Since π is an infinite sequence, there must be a function f such that
π can be decomposed to:σ

Theorem 3.1 A program P is fair terminating under C, if andonly if, RECP,C (f ) is well-founded (i.e., there is no infinite chain
ve0 RECP,C (f ) ve1 RECP,C (f ) ve2 RECP,C (f ) ve3 · · ·) for every function f defined in P .
Since the relation RECP,C (f ) is transitive, RECP,C (f ) is wellfounded if and only if RECP,C (f ) is disjunctively well-founded(i.e., is a finite union of well-founded relations) [26]. Thus, toshow that P is fair terminating under C, it suffices to pick a

σ

∗

σ

∗

σ

∗

i
ei+1 ] [20].
where ei = E1 [· · · Ei [f vei ] · · · ] and f vei −→P Ei+1 [f v
Let C = C1 ∪ C2 , where (i) each event in {A | (A, B) ∈ C1 }occurs only finitely often, and (ii) each event in {A | (A, B) ∈ C2 }occurs infinitely often in π. Let Pi and Qi be {A | (A, B) ∈Ci } and {B | (A, B) ∈ Ci } respectively. As π is fair, there
exists k such that, in σk σk+1 · · ·, no event in P1 occurs and every
event in Q2 occurs infinitely often. Now, let us define n1 , n2 , . . .
inductively by: (i) n1 = k, and (ii) ni+1 is the least j > ni suchthat every event in Q2 occurs in σni σni +1 · · · σj−1 . Then, we havean infinite sequence:en3 ⊲Cen2 ⊲Cf ven1 ⊲C
P ··· .
P fv
P fv

This contradicts the assumption that RECP,C (f ) is well-founded. ✷Theorem 3.3 (Completeness) If P is fair terminating, then forevery function f , RECP,C (f ) is well-founded.
Proof The proof is by contradiction. Suppose that RECP,C (f )is not well-founded for some f . Then there must be an infinite
sequence
e3 ⊲C
e2 ⊲C
f ve1 ⊲C
P ··· .
P fv
P fv

and call it a fair recursion relation.

The following is the key theorem for our verification method.

∗

2
1
0
main −→
P e1 −→P e2 −→P · · ·σ∗0
By the definition of ⊲C
P , there exist E1 , E2 , . . . where main ⋆ −→Pσi ∗E1 [f ve1 ] and f vei −→P Ei+1 [f vei+1 ] with σi |=fin C for everyi ≥ 1. Thus, we have an infinite reduction sequence π:

σ

∗

σ

∗

σ

∗

0
1
2
main ⋆ −→e1 ] −→
e2 ]] −→P E1 [f v
P E1 [E2 [f vP,

where for each σi (i ≥ 1), B occurs if A occurs for every (A, B) ∈C. Suppose that (A, B) ∈ C and A occurs infinitely often inπ. Then, there exist infinitely many i’s such that A occurs in σi .
But then B also occurs for each of such i’s. Thus, B also occurs
infinitely often. This implies that π is an infinite fair reduction
sequence, hence a contradiction.
✷

4. From Fair Binary Reachability to Reachability
This section describes a method for reducing a fair binary reachability problem to a plain reachability problem via program transformation; the latter problem can be solved by an off-the-shelf reachability checker for functional programs [27, 28].
4.1 Transformation
The transformation is an extension of that by [20] proposed for a
reduction from (plain) binary reachability to reachability. To ease
the exposition, we define the following terminology. Let π be apossibly infinite reduction sequence from main ⋆. Let us write π(i)for the ith element of π. That is,
ℓ

ℓ

1
2
main ⋆ = π(1) −→→P π(2) −P ···for some ℓ1 , ℓ2 , . . . . For total applications f w
e and f ve (i.e.,arity(f ) = |w|
e = |ev |) occurring in π, we say that f w
e is
an ancestor call of f ve in π if π(i1 ) = E1 [f w]e and π(i2 ) =E1 [E2 [f ve]] for some i1 < i2 , E1 and E2 . We omit the reduction
sequence π and simply say that f w
e is an ancestor call of f ev whenit is clear from the context. Note that f w
e is an ancestor call of f ev
in some π if and only if (f w,e fev ) ∈ Call +P (cf. Section 1.1). The
terminology is adopted from [20], and expresses the fact that f weoccurs as an ancestor node of f e
v in the call tree of π.
As in [20], to check RECP,C (f ) ⊆ Df , the arguments w
e of
an ancestor call to f is passed around as an auxiliary argument ofeach function, and when f is called with a new argument ve, we
assert that Df (w,e ev ) holds. A further twist is required, however.
We also need to keep information about the set σ of events thathave occurred since the ancestor call of f , and pass it around as
another auxiliary argument. When f is called with a new argument
ve, we assert Df (w,e ve) only if σ |=fin C holds.
We first explain the transformation informally, by using the
program in Example 2.2. Let Df be {(x′ , x) | x′ > x ≥ 0} and C
be {(A, Never)}. To check that RECPrep ,C (f ) ⊆ Df , we transform
Prep to the following program.
repeat s w g = let x = rand() inlet (s′ , ) = g s w x in repeat s′ w g
f s w x = assert(s = false ⇒ w > x ≥ 0);
let (s, w) =if rand() then (false, x) else (s, w) in
if x > 0 then f s w (x − 1) else (true, ⋆)main s w y = repeat s w f
Here, we have added two arguments s and w before each of theoriginal function argument. The argument w holds the value ofthe argument of an ancestor call to f , and s is a Boolean flagthat expresses whether the event A has occurred since the ancestor
call f w. The return value of each function call is now a pairconsisting of the flag and the original value. At the beginning of
the body of function f , it is asserted that if an event A has notoccurred, w > x ≥ 0 (i.e., Df (w, x)) must hold. If the assertion
fails, the program is aborted. Otherwise, the pair (s, w) is nondeterministically kept or updated to (false, x); in the latter case,the relationship between the present call and a future call to f
is checked. Thanks to this non-determinism, whenever there is aσ ∗recursive call f w −→Prep E[f v] in the original program (where
the second call is not necessarily directly called from the first one),the transformed program asserts that w > v ≥ 0 if σ |=fin C.
Therefore, RECPrep ,C (f ) ⊆ Df if and only if the assertion in
main false ⊥ ⋆ never fails. Here, assume that ⊥ is a special
value that satisfies ⊥ > n for any integer n.
There are some important subtleties to note about the transformation. First, while we maintain and pass around two types of auxiliary information (i.e., arguments to f and the event information),
the two are passed in different ways. Specifically, the event infor-

mation is passed through the sequential flow of the program execution. This requires each function to return the event information
as an auxiliary output so that the caller is able to use the information in the subsequent computation. For example, in the bodyof repeat , the event information returned by g s w x is bound tos′ and fed to the subsequent recursive call repeat s′ w g. By contrast, the argument information is only passed from the ancestor
call to its descendants. Therefore, for example, the past arguments
to f passed in the two calls that happen in the body of repeat areboth w: g s w x and repeat s′ w g. This is done so that detecting thefairness of a transition sequence is done by inspecting the sequential flow of the execution sequence, while checking for disjunctive
well-foundedness is done on the calling relation over such a sequence.
Secondly, the transformation passes the auxiliary information at
every function application site. This is needed because it is impossible in general to statically decide which indirect function application is a total application, or which is a call to the target function(f in the example above). We note that it is possible to soundly
eliminate some of the redundancy via a static analysis, and weuse such an optimization in our implementation. However, it is in
general impossible to completely decide a priori which function
is called in what context. The strength of our approach is that the
program transformation delegates such tasks to the backend reachability checker which would reason about such difficult reachability
queries if they are needed to prove the goal.
We now formalize the transformation. The target language is
obtained by extending the source language as follows.
e ::= · · · | fail | let (x1 , . . . , xk ) = e1 in e2
v ::= · · · | (v1 , . . . , vk ) | ⊥Here, fail aborts the program, and the special value ⊥ is used as
the initial value for the argument of an ancestor call to f . We write
assert(e) for let x = e in if x then ⋆ else fail.
The evaluation contexts and the labeled reduction relation areextended by:
E ::= · · · | let (x1 , . . . , xk ) = E in e
E[let (x1 , . . . , xk ) = (v1 , . . . , vk ) in e]ǫ−→P E[[v1 /x1 , . . . , vk /xk ]e]ǫ

E[fail] −→P fail
We remark that we have defined fail to be non-terminating. Thisis done for the technical reason of simplifying the statement ofTheorem 4.1. Since the labels for reductions are not important in
the target language, we omit them below.
We define the transformation in a top-down manner. A program
P = {f1 x
e1 = e1 , . . . , fn x
en = en } is transformed to:[⌈fi x
ei = ei ⌉f,D,C .
⌈P ⌉f,D,C =i∈{1,...,n}Here, each function definition g x1 · · · xk = e is translated tothe set ⌈g x1 · · · xk = e⌉f,D,C of function definitions, given by:⌈g x1 · · · xk = e⌉f,D,C ={ g s w x1 = (s, g (1) x1 ),g (1) x1 s w x2 = (s, g (2) x1 x2 ),··· ,g (k−1) x1 · · · xk−1 s w xk = e′ }As in the transformation of Prep explained above, we add two auxiliary arguments s and w before each argument. As in the example,
w is the value of the argument of an ancestor call to f (which isactually a tuple, since f may take more than one argument), and s,⌈v⌉s,w,C = (s, ⌈v⌉V )⌈rand()⌉s,w,C = (s, rand())⌈event A⌉s,w,C = (s{A := true}, ⋆)⌈v1 op v2 ⌉s,w,C = (s, v1 op v2 )⌈v1 v2 ⌉s,w,C = ⌈v1 ⌉V s w ⌈v2 ⌉V⌈if v then e1 else e2 ⌉s,w,C= if v then ⌈e1 ⌉s,w,C else ⌈e2 ⌉s,w,C⌈let x = e1 in e2 ⌉s,w,C= let (s′ , x) = ⌈e1 ⌉s,w,C in ⌈e2 ⌉s′ ,w,C⌈c⌉V = c⌈x⌉V = x⌈hf v1 · · · vk i⌉V = hf (k) ⌈v1 ⌉V · · · ⌈vk ⌉V i
Figure 5. The transformation of expressions and values.
called an event history, keeps information about the events that haveoccurred since the call f w. If C = {(A1 , B1 ), . . . , (An , Bn )},then s is a nested tuple of the form:((p1 , q1 ), . . . , (pn , qn ))where pi (qi , resp.) is a Boolean that expresses whether Ai (Bi ,resp.) has occurred.
Since each partial application of g should return a pair consisting of an event history and a closure, we have prepared auxiliary
functions g (1) , . . . , g (k−1) . The body e′ of g (k−1) is:
assert(fairs ⇒ D# (wk , (x1 , . . . , xk )));let (s, w) =if rand() then (sinit , (x1 , . . . , xk )) else (s, w) in⌈e⌉s,w,Cfrom fair binary reachability to plain reachability is sound andcomplete.
Theorem 4.1 (Correctness of the transformation)
Suppose ⌈P ⌉f,D = P ′ . Then, RECP,C (f ) 6⊆ D if and only ifmain sinit ⊥ ⋆ −→∗P ′ fail.
The rest of this section is devoted to the proof of the theorem
above, which is divided into the following two sub-theorems:
Theorem 4.2 (Soundness of the transformation)
Suppose ⌈P ⌉f,D = P ′ and RECP,C (f ) 6⊆ D. Then, if RECP,C (f ) 6⊆
D then main sinit ⊥ ⋆ −→∗P ′ fail.
Theorem 4.3 (Completeness of the transformation)
Suppose ⌈P ⌉f,D = P ′ . Then, if main sinit ⊥ ⋆ −→∗P ′ fail then
RECP,C (f ) 6⊆ D.
4.2 Proof of Soundness (Theorem 4.2)
The soundness follows from the following properties: (i) each reduction of an expression e in the source program is simulated by
the reductions of the corresponding expression ⌈e⌉s,w of the transformed program (Lemma 4.6), and (ii) the argument of an ancestor call of f is correctly recorded in the transformed program(Lemma 4.7).
We first prepare some definitions and auxiliary lemmas. We
extend the transformation to contexts by:⌈[ ]⌉w = [ ]⌈let x = E in e⌉w = let (s, x) = ⌈E⌉w in ⌈e⌉s,w

if g = f , and ⌈e⌉s,w,C otherwise (where the transformation⌈e⌉s,w,C for expressions is given later). Here, fairs denotes theexpression

Lemma 4.4 If E is a context for the source language, then ⌈E⌉w
is a context for the target language. Furthermore, ⌈E[e]⌉s,w =⌈E⌉w [⌈e⌉s,w ] holds.

let ((p1 , q1 ), . . . , (pn , qn )) = s in(p1 ⇒ q1 ) && · · · && (pn ⇒ qn ),Proof This follows by a straightforward induction on the structure of E.
✷

and sinit denotes the value((false, false), . . . , (false, false)).

Lemma 4.5 ⌈[v/x]e⌉s,w = [⌈v⌉V /x]⌈e⌉s,w .

D# (w, v) is an expression such that D# (w, v) evaluates to true if(i) w = (⌈w1 ⌉V , . . . , ⌈wk ⌉V ) and v = (⌈v1 ⌉V , . . . , ⌈vk ⌉V ) with((w1 , . . . , wk ), (v1 , . . . , vk )) ∈ D or (ii) w = ⊥, and evaluates
to false otherwise.5 In the definition of e′ above, s contains
information about the sequence σ of events that have occurred sincean ancestor call to f , and fairs expresses whether σ |=fin C
holds.
The transformations of expressions and values, denoted by⌈·⌉s,w,C and ⌈·⌉V respectively, are defined as shown in Figure 5.
Note that, after the transformation, an expression returns a pairconsisting of an updated event history and the value. On the thirdline, s{A := true} is an expression for updating the event history by replacing the elements corresponding to A with true.
More precisely, if C = {(A1,1 , A2,1 ), . . . , (A1,n , A2,n )}, thens{A := true} is:

Proof This follows by a straightforward induction on the structure of e.
✷let ((p1,1 , p2,1 ), . . . , (p1,n , p2,n )) = s in((p′1,1 , p′2,1 ), . . . , (p′1,n , p′2,n ))Proof The proof proceeds by a case analysis on the rule used forℓderiving e1 −→P e2 . We discuss only the main cases; the other cases
are straightforward.

where p′i,j is true if Ai,j = A and pi,j otherwise.
In the following, we fix the fairness constraint C and omit itin the transformation notation (e.g., we write ⌈P ⌉f,D instead of⌈P ⌉f,D,C ). The following theorems guarantee that our reduction
5 Therefore, if v contains a closure, the target language needs to have an
expressive power to inspect the contents of the closure; we can realize it bychoosing an appropriate representation of a closure.

Let σ be a finite sequence of events and s be an event history.
We define σ(s) by:ǫ(s) = s

A · σ(s) = σ(Js{A := true}K)

where Js{A := true}K is the value of the expression s{A :=true}. We write D0 for the “trivial” relation such that (ev, w)e ∈ D0for all ve and w.
e The following is the main lemma, which states that
reductions of a source program can be simulated by those of thetransformed program.
ℓLemma 4.6 Let P ′ be ⌈P ⌉f,D0 , If e1 −→P e2 , then ⌈e1 ⌉s,w −→∗P ′⌈e2 ⌉ℓ(s),w .

• Case E-E V: In this case, e1 = E[event A] and e2 = E[⋆] withℓ = A. By Lemma 4.4 and the definition of the transformation,
we have:⌈e1 ⌉s,w = ⌈E⌉w [(s{A := true}, ⋆)]⌈e2 ⌉ℓ(s),w = ⌈E⌉w [(ℓ(s), ⋆)]Thus, we have ⌈e1 ⌉s,w −→∗P ′ ⌈e2 ⌉ℓ(s),w as required.

• Case E-C LOS: In this case, e1 = E[hg v1 · · · vi−1 ivi ] ande2 = E[hg v1 · · · vi i] with ℓ = ǫ and i < arity(g). By
Lemma 4.4 and the definition of the transformation, we have:⌈e1 ⌉s,w = ⌈E⌉w [hg (i−1) ⌈v1 ⌉V · · · ⌈vi−1 ⌉V i s w ⌈vi ⌉V ]⌈e2 ⌉ℓ(s),w = ⌈E⌉w [(ℓ(s), hg (i) ⌈v1 ⌉V · · · ⌈vi ⌉V i)]⌈e1 ⌉s,w →− P ′ ⌈E⌉w [(s, g (i) ⌈v1 ⌉V · · · ⌈vi ⌉V )]→∗P ′ ⌈E⌉w [(s, hg (i) ⌈v1 ⌉V · · · ⌈vi ⌉V i)].
−Since ℓ(s) = s, we have ⌈e1 ⌉s,w −→P ′ ⌈e2 ⌉ℓ(s),w as required.
• Case E-C ALL: In this case, e1 = E[hg v1 · · · vi−1 i vi ] ande2 = E[[v1 /x1 , . . . , vi /xi ]e] with g x1 · · · xi = e ∈ P andℓ = ǫ. If g 6= f , then we have:⌈e1 ⌉s,w = ⌈E⌉w [hg (i−1) ⌈v1 ⌉V · · · ⌈vi−1 ⌉V is w ⌈vi ⌉V ]→+−P ′ ⌈E⌉w [[⌈v1 ⌉V /x1 , . . . , ⌈vi ⌉V /xi ]⌈e⌉s,w ]= ⌈E⌉w [⌈[⌈v1 ⌉V /x1 , . . . , ⌈vi ⌉V /xi ]e⌉s,w ]= ⌈e2 ⌉s,w = ⌈e2 ⌉ℓ(s),w⌈e1 ⌉s,w = ⌈E⌉w [hg (i−1) ⌈v1 ⌉V · · · ⌈vi−1 ⌉V is w ⌈vi ⌉V ]]→+−⌈E⌉w [assert(fairs ⇒ D0# (w, ⌈v⌉V )); · · · ]P′+→P ′ ⌈E⌉w [let (s, w) =−]if rand() then · · · else (s, w) in [⌈v⌉x]⌈e⌉s,w ]
V /e
+
]
/e
x
]⌈e⌉
]
→P ′ ⌈E⌉w [[⌈v⌉−Vs,w= ⌈e2 ⌉s,w = ⌈e2 ⌉ℓ(s),w ,✷The following lemma guarantees that whenever there is a callf v1 · · · vk in a source program, the argument (v1 , . . . , vk ) iscorrectly recorded in some reduction sequence of the transformed
program.
Lemma 4.7 Suppose f x1 · · · xk = e ∈ P and ⌈P ⌉f,D0 = P ′ .
Then,⌈hf v1 · · · vk−1 ivk ⌉s,w −→∗P ′ ⌈[v1 /x1 , . . . , vk /xk ]e⌉sinit ,w′′with w = (⌈v1 ⌉V , . . . , ⌈vk ⌉V ).
Proof This follows immediately from the definition of the transformation and Lemma 4.5.
✷
Proof of Theorem 4.2 Let ⌈P ⌉f,D = P ′ and f w1 · · · wk ⊲CP
f v1 · · · vk with ((w1 , . . . , wk ), (v1 , . . . , vk )) 6∈ D. Let P ′′ be′′C⌈P ⌉f,D0 = P By the definition of f w1 · · · wk ⊲P f v1 · · · vk ,we haveσ∗

By Lemmas 4.6 and 4.7, we have:main sinit ⊥ ⋆→∗P ′′ ⌈E1 [hf w1 · · · wk−1 iwk ]⌉σ1 (sinit ),⊥−= E1′ [⌈hf w1 · · · wk−1 iwk ⌉σ1 (sinit ),⊥ ]→∗P ′′ E1′ [⌈[w1 /x1 , . . . , wk /xk ]e⌉sinit ,(w1′ ,...,wk′ ) ]−→∗P ′′ E1′ [⌈E2 [hf v1 · · · vk−1 ivk ]⌉σ2 (sinit ),(w1′ ,...,wk′ ) ]−= E1′ [E2′ [⌈hf v1 · · · vk−1 ivk ⌉σ2 (sinit ),(w1′ ,...,wk′ ) ]]where wi′ = ⌈wi ⌉V , E1′ = ⌈E1 ⌉⊥ , and E2′ = ⌈E2 ⌉(w1′ ,...,wk′ ) .

⌈hf v1 · · · vk−1 ivk ⌉σ2 (sinit ),(w1′ ,...,wk′ )′= hf (k−1) v1′ · · · vk−1
i sinit (w1′ , . . . , wk′ ) vk′→∗P ′ E3 [assert(fairσ2 (sinit ) ⇒ D# (w−e′ , ev ′ ))]∗→P ′ fail−Here, we′ = (w1′ , . . . , wk′ ) and ve′ = (v1′ , . . . , vk′ ) with vi′ = ⌈vi ⌉V .
Note that fairσ2 (sinit ) evaluates to true by the condition σ2 |=fin
C, and D# ((w1′ , . . . , wk′ ), (v1′ , . . . , vk′ )) evaluates to false by theassumption ((w1 , . . . , wk ), (v1 , . . . , vk )) 6∈ D.
✷
4.3 Proof of Completeness (Theorem 4.3)

by Lemma 4.5 and the definition of the transformation.
If g = f , then we have1
main ⋆ −→P E1 [hf w1 · · · wk−1 iwk ]ǫ
hf w1 · · · wk−1 iwk −→P [w1 /x1 , . . . , wk /xk ]e
σ2 ∗−→P E2 [hf v1 · · · vk−1 ivk ]f x1 · · · xk = e ∈ P
σ2 |=fin C

main sinit ⊥ ⋆→∗P ′ E1′ [E2′ [⌈hf v1 · · · vk−1 ivk ⌉σ2 (sinit ),(w1′ ,...,wk′ ) ]].
−Note that the only difference between P ′′ and P ′ is that P ′ hasstronger assertion conditions; thus, reductions under P ′ may have
only more possibilities to fail. In the latter case, we have

By inspection of the reduction rules, we haveas required.

Thus, we have either main sinit ⊥ ⋆ −→∗P ′ fail, or

The completeness follows from the property that reductions of
the transformed program can be simulated by those of the source
program, as stated in Lemma 4.8 below. The statement is a little
more complex than the converse (Lemma 4.6), due to the nondeterminism in auxiliary reduction steps of the transformed program.
We call an expression e an instruction if e matches the lefthandside of a reduction rule in Section 2 with E = [ ].
Lemma 4.8 Suppose ⌈P ⌉f,D = P ′ . If e1 is an instruction andℓ′⌈e1 ⌉s,w −→+→P e 2P ′ e , then there exist e2 and ℓ such that e1 −+′and either (i) e −→P ′ ⌈e2 ⌉s′ ,w′ is obtained without using the∗′′′ →P ′ e .
rule for function calls, or (ii) ⌈e1 ⌉s,w −→+P ′ ⌈e2 ⌉s ,w −Furthermore, either (iii) s′ = ℓ(s) and w′ = w, or (iv) s′ = sinit
and w′ = (⌈v1 ⌉V , . . . , ⌈vk ⌉V ) with e1 = hf v1 · · · vk−1 ivk .
Proof The proof proceeds by induction on the length of the reduc′tion sequence ⌈e1 ⌉s,w −→+P ′ e , with a case analysis on the shapeof e1 . We discuss only the main cases; the other cases are straightforward.
• Case e1 = event A: In this case, we have⌈e1 ⌉s,w = (s{A := true}, ⋆).
Thus, the result holds for e2 = ⋆ and ℓ = A.
• Case e1 = hg v1 · · · vi−1 ivi : In this case, we have⌈e1 ⌉s,w = hg (i−1) ⌈v1 ⌉V · · · ⌈vi−1 ⌉V i s w ⌈vi ⌉V .
If i < arity(g), then the result holds for e2 = hg v1 · · · vi iand ℓ = ǫ.
If i = arity(g) and g 6= f with g x1 · · · xi = e ∈ P , thenthe result holds for e2 = [v1 /x1 , . . . , vn /xn ]e and ℓ = ǫ.
If i = arity(g) and g = f with g x1 · · · xi = e ∈ P , thesequence ⌈e1 ⌉s,w −→+e′ must be a prefix or postfix of theP′
reduction sequence ⌈e1 ⌉s,w −→+⌈[v1 /x1 , . . . , vn /xn ]e⌉s,w
P′or ⌈e1 ⌉s,w −
→+
⌈[v
/x
,
.
.
.
, vn /xn ]e⌉sinit ,(⌈v1 ⌉V ,...,⌈vk ⌉V ) .
1
1P′
Thus, the result holds also for e2 = [v1 /x1 , . . . , vn /xn ]e andℓ = ǫ.
✷
The following lemma guarantees that if w is recorded in thetarget program as the argument of an ancestor call for f , f has
indeed been called with w before.
Lemma 4.9 Suppose ⌈P ⌉f,D = P ′ . If ⌈e1 ⌉s,w −→∗P ′ E[⌈e2 ⌉s′ ,w′ ]with w 6= w′ and e2 is a function application, then• ⌈e1 ⌉s,w −→∗P ′ E1 [⌈hf v1 · · · vk−1 ivk ⌉s′′ ,w′′ ] and• ⌈hf v1 · · · vk−1 ivk ⌉s′′ ,w′′ ] −→∗P ′ E2 [⌈e2 ⌉s′ ,w′ ]with E = E1 [E2 ] and w′ = (⌈v1 ⌉V , . . . , ⌈vk ⌉V ).
Proof This follows by induction on the length of the reduction sequence ⌈e1 ⌉s,w −→∗P ′ E[⌈e2 ⌉s′ ,w′ ]. We first note that′′′′⌈e1 ⌉s,w −
→+
E[⌈e
⌉
2
′
s ,w ], since w 6= w . Since w 6= w , ⌈e1 ⌉s,w
P′
must be reducible. So, e1 can be decomposed to E3 [e1 ] where e′1 isan instruction. By the assumption ⌈e1 ⌉s,w −→∗P ′ E[⌈e2 ⌉s′ ,w′ ], wehave one of the following cases.
→∗P ′ E[⌈e2 ⌉s′ ,w′ ].
(a) ⌈e′1 ⌉s,w −→+P ′ (s1 , v) with ⌈E3 ⌉w [v] −′′(b) ⌈e′1 ⌉s,w −→+P ′ E4 [⌈e2 ⌉s ,w ] with E = ⌈E3 ⌉w [E4 ].

In case (a), by repeated applications of Lemma 4.8, it follows
that v = ⌈v1 ⌉V for some v1 . Thus, we have ⌈E3 [v]⌉s1 ,w −→∗P ′E[⌈e2 ⌉s′ ,w′ ], and the required property follows from the induction
hypothesis.
In case (b), by Lemma 4.8, there exist e′2 , s′′ , w′′ such that′→∗P ′ E4 [⌈e2 ⌉s′ ,w′ ];⌈e1 ⌉s,w −→+⌈e′2 ⌉s′′ ,w′′ and ⌈e′2 ⌉s′′ ,w′′ −P′
notice that case (i) of Lemma 4.8 does not hold, since e2 is anapplication. If the condition (iv) of Lemma 4.8 holds and w′′ = w′ ,then we have the required condition. Otherwise, we can apply the
induction hypothesis to get the required result.
✷
Proof of Theorem 4.3 Suppose ⌈P ⌉f,D = P ′ andmain sinit ⊥ ⋆ −→∗P ′ fail. Then, by Lemma 4.9, we have:main sinit ⊥ ⋆′→∗P ′ E1′ [hf (k−1) w1′ · · · wk−1−
is w′′ wk′ ]∗′′′→P ′ E1 [[w1 /x1 , . . . , wk /xk ]⌈e⌉sinit ,(w1′ ,...,wk′ ) ]−′→∗P ′ E1′ [E2′ [hf (k−1) v1′ · · · vk−1−is′ (w1′ , . . . , wk′ ) vk′ ]]→∗ truefairs′ −D# ((w1′ , . . . , wk′ ), v1′ , . . . , vk′ ) −→∗ false
Note that the only place where the translated program may fail isthe expression:
assert(fairs ⇒ D# (wk , (x1 , . . . , xk ))).
By induction on the length of the reduction sequence and Lemma 4.8,
it must be the case that:σ∗1main ⋆ −→P E1 [hf w1 · · · wk−1 iwk ]σ2 ∗hf w1 · · · wk−1 iwk −→P E2 [hf v1 · · · vk−1 ivk ]′⌈wi ⌉V = wi⌈vi ⌉V = vi′s′ = σ2 (sinit )→∗ true and s′ = σ2 (sinit ), we have
By the conditions fairs′ −σ2 ∗σ2 |=fin C. Together with the condition hf w1 · · · wk−1 iwk −→PCE2 [hf v1 · · · vk−1 ivk ], we have f w1 · · · wk ⊲P f v1 · · · vk .
By the conditions D# ((w1′ , . . . , wk′ ), v1′ , . . . , vk′ ) −→∗ false,⌈wi ⌉V = wi′ , and ⌈vi ⌉V = vi′ , we have((w1 , . . . , wk ), (v1 , . . . , vk )) 6∈ D.
Thus, we have the required result.

✷

5. Implementation and Experiments
We have implemented a prototype of our fair-termination verification method for a subset of OCaml. We use MoCHi [17] as thebackend reachability checker, and Z3 [8] as a constraint solver for
ranking function inference. As described in Section 1.1 Termination Argument Inference (and [20]), we use the implicit parameter
technique to obtain higher-order termination arguments.
We have tested our tool on examples from this paper, and benchmark programs taken from previous work on temporal property
verification for functional programs [11, 18, 21]. We translate theprogramintro
repeatclosurehofmann-1 [11, 12]
hofmann-2 [11, 12]
koskinen-1 [18]koskinen-2 [18]koskinen-3-1 [18]koskinen-3-2 [18]koskinen-3-3 [18]koskinen-4 [18]lester [21]cycle1
3
4
6
2
3
7
5
6
4
6
10
8

cycle2
14
12
18
4
8
27
16
17
14
23
35
36

time
11.492
2.276
9.76
0.232
1.032
43.344
3.412
2.752
2.216
4.964
132.552
38.356

Table 1. The experiment results.

programs to OCaml, and we translate the property to fair termination (for ones from [18, 21] where the properties are given as temporal logic formulas or automaton inclusion problems). We haveconducted the experiments on a machine with Intel Core i7-3930K(3.20 GHz, 16 GB of memory), with timeout of 600 seconds. The
web interface of the implementation and the benchmarks used in
the experiments are available on the web.6
Table 1 summarizes the experiment results. The column “program” shows the names of the programs. The columns “cycle1” and“cycle2” show the number of counterexample-guided refinement(CEGAR) iterations. MoCHi [17] itself uses CEGAR internally,and “cycle2” is the cumulative count of MoCHi’s internal CEGAR
iterations over the course of the verification process, whereas “cycle1” shows only the number of the outer CEGAR iterations (i.e.,
the number of times candidate termination arguments are inferred– cf. Figure 2). The column “time” shows the running time in seconds.
All of the benchmarks are fair terminating. We remark thatnone of them can be verified by the previous automatic methods.
This is because the methods for imperative programs [10, 15, 20,
29] cannot handle functions, and the methods for higher-orderfunctional programs cannot handle infinite data [16, 21–23] or
can only handle safety properties [13, 17, 27, 32–34, 36, 37] or
termination [10, 15, 20, 29]. As we describe below, the benchmarks
from the previous literature [11, 18, 21] are either verified manuallyor verified after a manual finite-data abstraction in the respective
works. Our work is the first fully automatic approach that is able toverify these instances.
We describe the benchmarks. The benchmark intro is Pex
from Section 1.1 with the fairness constraint C ′ = {(f 0, false)}.
The benchmark repeat is the one from Example 2.2. The benchmark closure is the program below with the fairness constraint
C = {(A, Never)}.
const x y = x
finish x = event A; finish x
f g = let n = g ⋆ in
if n > 0 then f (const (n − 1)) else finish ⋆main x = let n = rand() in f (const n)
The benchmark is an example where a higher-order termination argument (i.e., disjunctive well-founded relation over function values) is required for verification. It is interesting to note that theother benchmarks, including the ones from the previous literature, can be verified with only first-order termination argument (buthigher-order reasoning is required at the rest of the verification pro6 http://www-kb.is.s.u-tokyo.ac.jp/~ ryosuke/fair_termination/

cess even in the other benchmarks – such as when checking thereachability against the transformed program).
The benchmarks hofmann-1 and hofmann-2 are from a recent
work by Hofmann and Chen [11]. Specifically, hofmann-1 (resp.
hofmann-2) is the first (resp. second) example from Appendix Aof the extended technical report [12] (hofmann-2 also appears as
an example in Section 5.4 of [11]). Their paper shows how thesebenchmarks can be verified manually in their framework, but it
does not show how to automate the process.
The benchmarks koskinen-xxx’s are from a recent paper by
Koskinen and Terauchi [18]. They are taken from Figure 10 of thepaper where koskinen-1 is R EDUCE , koskinen-2 is RUMBLE ,koskinen-3-x’s are RUMBLE , and koskinen-4 is A LTERNATEI NEVITABILITY. Their paper presents the temporal properties to beverified as temporal logic formulas, and we have translated them
to fair termination for our experiments in the manner describedin Section 2. We note that RUMBLE is translated into (the conjunction of) three sub-problems: koskinen-3-1, koskinen-3-2
and koskinen-3-3. During the experiments, we have actually discovered a bug in A LTERNATE I NEVITABILITY in their paper, andthe result presented here is for a version with the bug corrected.
As with the work by Hofmann and Chen, their paper shows how
these benchmarks can be verified manually in their framework, but
it does not show how to automate the process.
The benchmark lester is the example from Appendix H.1of the paper by Lester et al. [21]. Their verification method can
only handle finite data, simply-typed higher-order functional programs, so they used Church numerals to represent natural numbers,
and manually translated a loop over integers into an iteration overChurch numerals. The version we verify in the experiments directly
uses integers. Also, their paper presents the temporal property to
be verified as a temporal logic formula and an automaton inclusion problem, and we have translated it to fair termination for our
experiments in the manner described in Section 2.
As seen in Table 1, the results show that our implementation
successfully verifies all of the benchmarks. The implementation
is able to verify the benchmarks quite quickly, except for intro,
koskinen-1, koskinen-4, and lester. The performance bottleneck appears to be the backend reachability checker MoCHi [17]which is taking a rather long time to verify the reachability problems generated in the verification of these benchmarks. In particular, the benchmarks koskinen-1, koskinen-4, and lester, after
the CPS / HORS (higher-order recursion scheme) translation done
within MoCHi, produce large reachability verification instances.
For intro, the HORS model checker within MoCHi seems to be
the main bottleneck, and we leave for future work to analyze why
the HORS model checker underperforms on the recursion schemes
generated in this benchmark. We remark that this is not a fundamental limitation with our fair-termination verification approach,and we expect further advances in reachability verification to allow
our approach to verify instances like these more quickly.

6. Conclusion
We have presented an automatic approach to temporal property verification of higher-order functional programs. Previous automatedapproaches to this class of programs could only handle finite data
programs or only safety properties or plain termination, and ourwork is the first to be able verify arbitrary ω-regular properties of
infinite data high-order functional programs. Our approach combines and extends the techniques from the recent work on binaryreachability based approaches to plain termination verification ofhigher-order functional programs [20] and fair termination verification of imperative programs [2], and reduces the temporal property
verification problem soundly and completely to fair binary reachability verification problems over calling relations. A key contri-

bution of our approach includes the novel program transformationthat correctly tracks the calling relation and the event occurrence
information through the higher-order control flow.

Acknowledgments
We thank the anonymous reviewers for useful comments. This
work was partially supported by MEXT Kakenhi 26330082, 25280023,
15H05706, 23220001, 25730035, and 25280020, and JSPS Coreto-Core Program (A. Advanced Research Networks).

References[1] A. M. Ben-Amram. General size-change termination and lexicographic descent. In T. Æ. Mogensen, D. A. Schmidt, and I. H. Sudborough, editors, The Essence of Computation, Complexity, Analysis,
Transformation. Essays Dedicated to Neil D. Jones [on occasion of his
60th birthday], volume 2566 of Lecture Notes in Computer Science,
pages 3–17. Springer, 2002.
[2] B. Cook, A. Gotsman, A. Podelski, A. Rybalchenko, and M. Y. Vardi.
Proving that programs eventually do something good. In M. Hofmann
and M. Felleisen, editors, Proceedings of the 34th ACM SIGPLANSIGACT Symposium on Principles of Programming Languages, POPL
2007, Nice, France, January 17-19, 2007, pages 265–276. ACM,
2007.
[3] B. Cook and E. Koskinen. Making prophecies with decision predicates. In T. Ball and M. Sagiv, editors, Proceedings of the 38th ACM
SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2011, Austin, TX, USA, January 26-28, 2011, pages
399–410. ACM, 2011.
[4] B. Cook and E. Koskinen. Reasoning about nondeterminism in programs. In H. Boehm and C. Flanagan, editors, ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI
’13, Seattle, WA, USA, June 16-19, 2013, pages 219–230. ACM, 2013.
[5] B. Cook, E. Koskinen, and M. Y. Vardi. Temporal property verification as a program analysis task. In G. Gopalakrishnan and S. Qadeer,
editors, Computer Aided Verification - 23rd International Conference,
CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings, volume 6806 of Lecture Notes in Computer Science, pages 333–348.
Springer, 2011.
[6] B. Cook, A. Podelski, and A. Rybalchenko. Termination proofs for
systems code. In M. I. Schwartzbach and T. Ball, editors, Proceedingsof the ACM SIGPLAN 2006 Conference on Programming Language
Design and Implementation, Ottawa, Ontario, Canada, June 11-14,
2006, pages 415–426. ACM, 2006.
[7] B. Cook, A. See, and F. Zuleger. Ramsey vs. lexicographic termination
proving. In TACAS, volume 7795 of Lecture Notes in Computer
Science, pages 47–61. Springer, 2013.
[8] L. M. de Moura and N. Bjørner. Z3: An efficient SMT solver. In
TACAS, volume 4963 of Lecture Notes in Computer Science, pages
337–340. Springer, 2008.
[9] K. Fujima, S. Ito, and N. Kobayashi. Practical alternating parity
tree automata model checking of higher-order recursion schemes. In
C. Shan, editor, Programming Languages and Systems - 11th Asian
Symposium, APLAS 2013, Melbourne, VIC, Australia, December 911, 2013. Proceedings, volume 8301 of Lecture Notes in Computer
Science, pages 17–32. Springer, 2013.
[10] J. Giesl, M. Raffelsieper, P. Schneider-Kamp, S. Swiderski, and
R. Thiemann. Automated termination proofs for Haskell by term
rewriting. ACM Trans. Prog. Lang. Syst., 33(2):7:1–7:39, Feb. 2011.
[11] M. Hofmann and W. Chen. Abstract interpretation from Büchi automata. In T. A. Henzinger and D. Miller, editors, Joint Meeting of theTwenty-Third EACSL Annual Conference on Computer Science Logic(CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logicin Computer Science (LICS), CSL-LICS ’14, Vienna, Austria, July 14- 18, 2014, pages 51:1–51:10. ACM, 2014.
[12] M. Hofmann and W. Chen. Büchi types for infinite traces and liveness.
CoRR, abs/1401.5107, 2014.

[13] R. Jhala, R. Majumdar, and A. Rybalchenko. HMC: verifying functional programs using abstract interpreters. In G. Gopalakrishnan and
S. Qadeer, editors, Computer Aided Verification - 23rd International
Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings, volume 6806 of Lecture Notes in Computer Science, pages
470–485. Springer, 2011.
[14] T. Johnsson. Lambda lifting: Treansforming programs to recursive
equations. In FPCA, pages 190–203, 1985.
[15] N. D. Jones and N. Bohr. Call-by-value termination in the untyped
lambda-calculus. Logical Methods in Computer Science, 4(1), 2008.
[16] N. Kobayashi and C. L. Ong. A type system equivalent to the modal
mu-calculus model checking of higher-order recursion schemes. In
Proceedings of the 24th Annual IEEE Symposium on Logic in Computer Science, LICS 2009, 11-14 August 2009, Los Angeles, CA, USA,pages 179–188. IEEE Computer Society, 2009.
[17] N. Kobayashi, R. Sato, and H. Unno. Predicate abstraction and CEGAR for higher-order model checking. In M. W. Hall and D. A.
Padua, editors, Proceedings of the 32nd ACM SIGPLAN Conference
on Programming Language Design and Implementation, PLDI 2011,
San Jose, CA, USA, June 4-8, 2011, pages 222–233. ACM, 2011.
[18] E. Koskinen and T. Terauchi. Local temporal reasoning. In T. A.
Henzinger and D. Miller, editors, Joint Meeting of the Twenty-ThirdEACSL Annual Conference on Computer Science Logic (CSL) and theTwenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer
Science (LICS), CSL-LICS ’14, Vienna, Austria, July 14 - 18, 2014,
pages 59:1–59:10. ACM, 2014.
[19] T. Kuwahara, R. Sato, H. Unno, and N. Kobayashi. Predicate abstraction and CEGAR for disproving termination of higher-order functional
programs. In D. Kroening and C. S. Pasareanu, editors, Computer
Aided Verification - 27th International Conference, CAV 2015, San
Francisco, CA, USA, July 18-24, 2015, Proceedings, Part II, volume9207 of Lecture Notes in Computer Science, pages 287–303. Springer,
2015.
[20] T. Kuwahara, T. Terauchi, H. Unno, and N. Kobayashi. Automatic termination verification for higher-order functional programs. In Z. Shao,
editor, Programming Languages and Systems - 23rd European Symposium on Programming, ESOP 2014, Held as Part of the European Joint
Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014, Proceedings, volume 8410 of Lecture
Notes in Computer Science, pages 392–411. Springer, 2014.
[21] M. M. Lester, R. P. Neatherway, C.-H. L. Ong, and S. J. Ramsay. Model checking liveness properties of higher-order functional
programs. URL https://mjolnir.comlab.ox.ac.uk/papers/
thors.pdf, 2011.
[22] R. P. Neatherway and C. L. Ong. TravMC2: higher-order model checking for alternating parity tree automata. In N. Rungta and O. Tkachuk,
editors, 2014 International Symposium on Model Checking of Software, SPIN 2014, Proceedings, San Jose, CA, USA, July 21-23, 2014,
pages 129–132. ACM, 2014.
[23] C. L. Ong. On model-checking trees generated by higher-order recursion schemes. In 21th IEEE Symposium on Logic in Computer Science (LICS 2006), 12-15 August 2006, Seattle, WA, USA, Proceedings,
pages 81–90. IEEE Computer Society, 2006.
[24] A. Pnueli, A. Podelski, and A. Rybalchenko. Separating fairness
and well-foundedness for the analysis of fair discrete systems. In
N. Halbwachs and L. D. Zuck, editors, Tools and Algorithms for theConstruction and Analysis of Systems, 11th International Conference,
TACAS 2005, Held as Part of the Joint European Conferences on

Theory and Practice of Software, ETAPS 2005, Edinburgh, UK, April
4-8, 2005, Proceedings, volume 3440 of Lecture Notes in Computer
Science, pages 124–139. Springer, 2005.
[25] A. Podelski and A. Rybalchenko. A complete method for the synthesisof linear ranking functions. In VMCAI, volume 2937 of Lecture Notes
in Computer Science, pages 239–251. Springer, 2004.
[26] A. Podelski and A. Rybalchenko. Transition invariants. In 19th
IEEE Symposium on Logic in Computer Science (LICS 2004), 14-17
July 2004, Turku, Finland, Proceedings, pages 32–41. IEEE Computer
Society, 2004.
[27] P. M. Rondon, M. Kawaguchi, and R. Jhala. Liquid types. In R. Gupta
and S. P. Amarasinghe, editors, Proceedings of the ACM SIGPLAN
2008 Conference on Programming Language Design and Implementation, Tucson, AZ, USA, June 7-13, 2008, pages 159–169. ACM, 2008.
[28] R. Sato, H. Unno, and N. Kobayashi. Towards a scalable softwaremodel checker for higher-order programs. In E. Albert and S. Mu,
editors, Proceedings of the ACM SIGPLAN 2013 Workshop on Partial
Evaluation and Program Manipulation, PEPM 2013, Rome, Italy,
January 21-22, 2013, pages 53–62. ACM, 2013.
[29] D. Sereni. Termination analysis of higher-order functional programs.
PhD thesis, Magdalen College, 2006.
[30] C. Skalka and S. F. Smith. History effects and verification. In W. Chin,
editor, Programming Languages and Systems: Second Asian Symposium, APLAS 2004, Taipei, Taiwan, November 4-6, 2004. Proceedings,
volume 3302 of Lecture Notes in Computer Science, pages 107–128.
Springer, 2004.
[31] C. Skalka, S. F. Smith, and D. V. Horn. Types and trace effects ofhigher order programs. J. Funct. Program., 18(2):179–249, 2008.
[32] T. Terauchi. Dependent types from counterexamples. In M. V.
Hermenegildo and J. Palsberg, editors, Proceedings of the 37th ACM
SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2010, Madrid, Spain, January 17-23, 2010, pages 119–130. ACM, 2010.
[33] H. Unno and N. Kobayashi. Dependent type inference with interpolants. In A. Porto and F. J. López-Fraguas, editors, Proceedings ofthe 11th International ACM SIGPLAN Conference on Principles andPractice of Declarative Programming, September 7-9, 2009, Coimbra,
Portugal, pages 277–288. ACM, 2009.
[34] H. Unno, T. Terauchi, and N. Kobayashi. Automating relatively complete verification of higher-order functional programs. In R. Giacobazzi and R. Cousot, editors, The 40th Annual ACM SIGPLANSIGACT Symposium on Principles of Programming Languages, POPL
’13, Rome, Italy - January 23 - 25, 2013, pages 75–86. ACM, 2013.
[35] M. Y. Vardi. Verification of concurrent programs: The automatatheoretic framework. Ann. Pure Appl. Logic, 51(1-2):79–98, 1991.
[36] N. Vazou, E. L. Seidel, and R. Jhala. LiquidHaskell: experience withrefinement types in the real world. In W. Swierstra, editor, Proceedings of the 2014 ACM SIGPLAN symposium on Haskell, Gothenburg,
Sweden, September 4-5, 2014, pages 39–51. ACM, 2014.
[37] N. Vazou, E. L. Seidel, R. Jhala, D. Vytiniotis, and S. L. P. Jones. Refinement types for Haskell. In J. Jeuring and M. M. T. Chakravarty,
editors, Proceedings of the 19th ACM SIGPLAN international conference on Functional programming, Gothenburg, Sweden, September
1-3, 2014, pages 269–282. ACM, 2014.
[38] K. Yokoyama. Ramsey’s theorem and termination analysis. In JAISTRCSV-Logic Workshop, 2014. http://www.jaist.ac.jp/rcsv/
event/20141030-eventws/yokoyama.pdf.