Predicate Abstraction and CEGAR for Disproving Termination of Higher-Order Functional Programs

Abstract

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

These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

1 Introduction

We propose an automated method for disproving termination of higher-order functional programs (i.e., for proving that a given program does not terminate for some input). The method plays a role complementary to the automated method for proving termination of higher-order programs (i.e., for proving that a given program terminates for all inputs) [18]. Several methods have recently been proposed for proving non-termination of programs [7–9, 11, 13, 14, 19], but most of them have focused on first-order programs (or, while programs) that can be represented as finite control graphs. An exception is work on term rewriting systems (TRS) [9, 11]; higher-order programs can be encoded into term rewriting systems, but the definition of non-termination is different: TRS is non-terminating if there exists a term that has a non-terminating rewriting sequence, not necessarily the initial term.

Our approach is based on a combination of higher-order model checking [15, 21] with predicate abstraction and CEGAR (counterexample-guided abstraction refinement). Values of a base type (such as integers) are abstracted to (tuples of) Booleans by using predicates, and higher-order functions are abstracted accordingly. Higher-order model checking is then used to analyze the abstracted program. A combination of predicate abstraction and higher-order model checking has been previously proposed for verifying safety properties of higher-order programs (i.e., for proving that a program does not reach an error state in all execution paths) [16]. With respect to that work, the approach of the present paper is novel in that we combine overapproximation and underapproximation. Note that predicate abstraction [3, 12, 16] usually yields an overapproximation, i.e., an abstract program that contains a superset of possible execution paths of the original program. With such an abstraction, non-termination of the abstract program (the existence of a non-terminating path) does not imply that of the original program. To address this problem, we use both under- and overapproximations. For a deterministic computation step of the original program, we apply overapproximation but check that every branch of the overapproximation has a non-terminating path. For a non-deterministic branch of the original program (such as random number generation and an input from the environment), we apply under-approximation, and check that some branch of the underapproximation has a non-terminating path.

Figure 1 illustrates how under- and overapproximations are combined. The program considered here is of the form:

$$\begin{aligned} \mathbf {let}\;x=*\;\mathbf {in}\;\mathbf {let}\;y=x+1\;\mathbf {in}\;\mathbf {let}\;z=*\;\mathbf {in}\;\cdots . \end{aligned}$$

Here, $*$ generates a random integer. Thus, the program has the execution tree shown on the top of Fig. 1. The first and third steps are non-deterministic, while the second step (corresponding to $y=x+1$) is deterministic. Suppose that the predicates used for abstracting the values of $x,y$, and $z$ are $x>0$, $y>0$, and $0\le z<x+y$ (these predicates do not necessarily yield a good abstraction, but are sufficient for explaining the combination of under- and overapproximations). Then, the abstract program has the execution tree shown on the bottom of the figure. Due to the predicate abstraction, the infinitely many branches on the value of $x$ have been replaced by two branches $x>0$ and $\lnot x>0$. The node $\exists$ means that only one of the branches needs to have an infinite path (for the original program having a non-terminating path). The deterministic path from $x=n$ to $y=n+1$ has now been replaced by non-deterministic branches $y>0$ and $\lnot y>0$. The node $\forall$ indicates that every child of the node must have an infinite path. Below the node $x>0$, however, we do not have a node for $\lnot y>0$, as $x>0$ and $y=x+1$ imply $y>0$. The infinite branches on $z$ have been replaced by non-deterministic branches on $\lnot (0\le z<x+y)$ or $0\le z<x+y$. As is the case for $x$, the branches are marked by $\exists$, meaning that one of the branches needs to have an infinite path. Note that below the node $\lnot x>0$, we only have a branch for $\lnot (0\le z<x+y)$. This is because, when $x\le 0$, there may be no $z$ that satisfies $0\le z<x+y$; so, even if there may be an infinite execution sequence along that path, we cannot conclude that the source program is non-terminating. Thus, this part of the tree provides an under-approximation of the source program.

An abstract program is actually represented as a tree-generating program that generates an execution tree like the one shown on the bottom of Fig. 1. Higher-order model checking is then used for checking, informally speaking, that every child of each $\forall$-node has a non-terminating path, and that some child of each $\exists$-node has a non-terminating path.

Fig. 1.

Execution trees before/after abstraction

The use of overapproximation for disproving termination has also been proposed recently by Cook et al. [8]. Although their theoretical framework is general, their concrete method for automation is limited to first-order programs. They also propose a restricted form of combination of underapproximation and overapproximation, but underapproximation can be followed by overapproximation, but not vice versa.

The rest of this paper is structured as follows. Section 2 defines the language used as the target of our verification. Sections 3 and 4 describe predicate abstraction and CEGAR respectively. Section 5 reports experiments. Section 6 discusses related work and Sect. 7 concludes the paper.

2 Language

In this section, we introduce the language of source programs, used as the target of non-termination verification. It is a simply typed, call-by-value higher-order functional language. Throughout the paper, we often use the following abbreviations: $\widetilde{e}$ for a possibly empty sequence $e_1,\ldots ,e_n$, and $\left\{ e_i\right\} _{i\in \left\{ 1,\ldots ,n\right\} }$ for the set $\left\{ e_1,\ldots ,e_n\right\}$.

Fig. 2.

The syntax and operational semantics of the language

The syntax and operational semantics of the language is given in Fig. 2. The meta-variable $f_i$ ranges over a set of function names, and $x,y$ range over the set of function names and ordinary variables. The meta-variable $n$ ranges over the set of integers, and $\text {op}$ over a set of integer operations. We omit Booleans and regard a non-negative integer as true, and $0$ as false. We require that $y\,\widetilde{v}$ in the definition of $e$ is a full application, i.e., that all the necessary arguments are passed to $y$, and $y\,\widetilde{v}$ has a base type. In contrast, $y\,\widetilde{v}$ in the definition of $v$ is a partial application. Whether $y\,\widetilde{v}$ is a full or partial application is actually determined by the simple type system mentioned below.

The expression $\mathtt {let\ } x\mathtt {\,=\,} \mathtt {*} _{\mathtt{int}}\mathtt {\ in\ } e$ randomly generates an integer, binds $x$ to it, and evaluates $e$. The meanings of the other expressions should be clear. A careful reader may notice that we have only tail calls. This is for the simplicity of the presentation. Note that it does not lose generality, because we can apply the standard continuation-passing-style (CPS) transformation to guarantee that all the function calls are in this form. We assume that for every program $\{f_i\ \widetilde{x}_i = e_i\}_{i\in \{1\dots n\}}$, $\mathtt {main} \in \left\{ f_1,\ldots ,f_n\right\}$.

We assume that programs are simply-typed. The syntax of types is given by: $\tau {:}{:}{=} \mathbf {int}\mid \star \mid \tau _1\rightarrow \tau _2$. The types $\mathbf {int}$ and $\star$ describe integers and the unit value $\mathtt {(\,)}$ respectively. The type $\tau _1\rightarrow \tau _2$ describes functions from $\tau _1$ to $\tau _2$. The typing rules for expressions and programs are given in the full version [17], which are standard except that the body of each function definition can only have type $\star$. This does not lose generality since the CPS transformation guarantees this condition.

The one-step reduction relation $e_1 \longrightarrow _{P} e_2$ is defined by the rules in Fig. 2, where $[\![ a ]\!]$ stands for the value of the simple expression $a$. A program P is non-terminating if there is an infinite reduction sequence $\mathtt {main} \rightarrow _{P} e_1 \rightarrow _{P} e_2 \rightarrow _{P} \dots$.

Fig. 3.

The syntax and semantics of the target language

3 Predicate Abstraction

3.1 Target Language

The target language of predicate abstraction is a higher-order simply-typed functional language having Booleans and special tree constructors as primitives. The syntax is given in Fig. 3. We assume that for every program $\{f_i\ \widetilde{x}_i = M_i\}_{i\in \{1\dots n\}}$, $\mathtt {main} \in \left\{ f_1,\ldots ,f_n\right\}$. Each expression generates a possibly infinite tree, describing possible executions of a source program. The expression $c(M_1,\ldots ,M_k)$ generates a node labeled with $c$, having the trees generated by $M_1,\ldots ,M_k$ as its children. Here, $c$ ranges over the set $\left\{ \mathtt {end}, \mathtt {call}, \mathtt {br}_{\forall },\mathtt {br}_{\exists }\right\}$ of tree constructors. The constructors $\mathtt {end}$ and $\mathtt {call}$ have arities $0$ and $1$ respectively, while $\mathtt {br}_{\forall }$ and $\mathtt {br}_{\exists }$ may have arbitrarily many children. We just write $\mathtt {end}$ for $\mathtt {end}()$. The expression $\mathtt {let\ } x\mathtt {\,=\,} {(b_1,\ldots ,b_k)}\mathtt {\ in\ } M$ binds $x$ to the tuple $(b_1,\ldots ,b_k)$, and evaluates $M$. The expression $\mathtt {br}_{\forall }\left\{ \psi _1\rightarrow M_1,\ldots ,\psi _k\rightarrow M_k\right\}$ ($\mathtt {br}_{\exists }\left\{ \psi _1\rightarrow M_1,\ldots ,\psi _k\rightarrow M_k\right\}$, resp.) generates the node $\mathtt {br}_{\forall }$ ($\mathtt {br}_{\exists }$, resp.), and adds the tree generated by $M_i$ as a child of the node if $\psi _i$ evaluates to $\mathtt {true}$, where the order of children does not matter. The Boolean expression $\#_{i}{x}$ denotes the $i$-th element of the tuple $x$. For example, $\mathtt {let\ } x\mathtt {\,=\,} (\mathtt {true} ,\mathtt {false} )\mathtt {\ in\ } \mathtt {br}_{\forall }\{\#_{1}(x)\rightarrow \mathtt {end}, \#_{2}(x)\rightarrow \mathtt {call}(\mathtt {call}(\mathtt {end}))$, $\#_{1}(x)\vee \#_{2}(x)\rightarrow \mathtt {call}(\mathtt {end})\}$ generates the tree:

The formal semantics is given through the reduction relation $M\longrightarrow _{D}M'$, defined in Fig. 3. The tree generated by a program $D$, written $\mathbf {Tree}(D)$, is the “limit” of the trees obtained from a (possibly infinite) reduction sequence $\mathtt {main} \longrightarrow _{D}M_1 \longrightarrow _{D}M_2\longrightarrow _{D}\cdots$. For example, the program $\left\{ \mathtt {main} =\right. \left. \mathtt {call}(\mathtt {main} )\right\}$ generates an infinite (linear) tree consisting of infinitely many $\mathtt {call}$ nodes.

Intuitively, the tree generated by a program of the target language describes possible execution sequences of a source program. The property that a source program has a non-terminating execution sequence is transformed to the property of the tree that (i) every child of each $\mathtt {br}_{\forall }$ node has an infinite path, and (ii) some child of each $\mathtt {br}_{\exists }$ node has an infinite path. More formally, the set of (infinite) trees that represent the existence of a non-terminating computation is the largest set $\mathbf {NonTermTrees}$ such that for every $T\in \mathbf {NonTermTrees}$, $T$ satisfies one of the following conditions.

• 1. $T=\mathtt {call}(T')$ and $T'\in \mathbf {NonTermTrees}$

• 2. $T=\mathtt {br}_{\forall }(T_1,\ldots ,T_k)$ and $T_i\in \mathbf {NonTermTrees}$ for all $i\in \left\{ 1,\ldots ,k\right\}$.

• 3. $T=\mathtt {br}_{\exists }(T_1,\ldots ,T_k)$ and $T_i\in \mathbf {NonTermTrees}$ for some $i\in \left\{ 1,\ldots ,k\right\}$.

The property above can be expressed by MSO (the monadic second order logic; or equivalently, modal $\mu$-calculus or alternating parity tree automata); thus whether the tree generated by a program of the target language belongs to $\mathbf {NonTermTrees}$ can be decided by higher-order model checking [15, 21].

3.2 Abstraction

We now formalize predicate abstraction for transforming a source program to a program (of the target language) that generates a tree that approximately represents the possible execution sequences of the source program. Following Kobayashi et al. [16], we use abstraction types for expressing which predicate should be used for abstracting each value. The syntax of abstraction types is:

$$\begin{aligned} \begin{array}{l} \sigma \text{(abstraction } \text{ types) }\,{:}{:}{=}\,\,\star \mid \mathbf {int}[Q_1,\ldots ,Q_k] \mid {x}\mathbin {:}{\sigma _1}\rightarrow {\sigma _2}\\ Q \text{(predicates) }\,{:}{:}{=}\,\,\lambda x.\varphi \qquad \varphi \, {:}{:}{=}\,\,n_1 x_1+\cdots + n_kx_k\le n \mid \varphi _1\vee \varphi _2 \mid \lnot \varphi \end{array} \end{aligned}$$

The type $\star$ describes the unit value, and $\mathbf {int}[Q_1,\ldots ,Q_k]$ describes an integer that should be abstracted by using the predicates $Q_1,\ldots ,Q_k$. For example, given an abstraction type $\mathbf {int}[\lambda x.x\le 1, \lambda x.2x-1\le 0]$, the integer $1$ is abstracted to $(\mathtt {true} , \mathtt {false} )$. In the syntax above, we list only linear inequalities as primitive constraints, but we can include other constraints (such as those on uninterpreted function symbols) as long as the underlying theory remains decidable. The type ${x}\mathbin {:}{\sigma _1}\rightarrow {\sigma _2}$ describes a function whose argument and return value should be abstracted according to $\sigma _1$ and $\sigma _2$ respectively. In $\sigma _2$, the argument can be referred to by $x$ if $x$ has an integer type $\mathbf {int}[Q_1,\ldots ,Q_k]$. For example, ${x}\mathbin {:}{\mathbf {int}[\lambda x.x\le 0]}\rightarrow {\mathbf {int}[\lambda y.y-x\le 0]}$ describes a function from integers to integers whose argument should be abstracted using the predicate $\lambda x.x\le 0$ and whose return value should be abstracted using $\lambda y.y-x\le 0$. Thus, the successor function (defined by $f\,x=x+1$) will be abstracted to a Boolean function $\lambda b.\mathtt {false}$ (because the return value $x+1$ is always greater than $x$, no matter whether $x\le 0$ or not).

The predicate abstraction for expressions and programs is formalized using the relations $\varGamma \vdash e\mathbin {:}\sigma \leadsto {M}$ and $\vdash P\mathbin {:}\varGamma \leadsto {D}$, where $\varGamma$, called an abstraction type environment, is of the form $x_1\mathbin {:}\sigma _1,\ldots ,x_n\mathbin {:}\sigma _n$. Intuitively, $\varGamma \vdash e\mathbin {:}\sigma \leadsto {M}$ means that under the assumption that each free variable $x_i$ of $e$ is abstracted according to $\sigma _i$, the expression $e$ is abstracted to $M$ according to the abstraction type $\sigma$. In the judgment $\vdash P\mathbin {:}\varGamma \leadsto {D}$, $\varGamma$ describes how each function defined in $P$ should be abstracted.

The relations are defined by the rules in Fig. 4. Here, we consider, without loss of generality, only if-expressions of the form $\mathtt {if\ } x\mathtt {\ then\ } e_1\mathtt {\ else\ } e_2$. Also, function arguments are restricted to the syntax: $v\ {:}{:}{=}\ y\ \widetilde{v}$. (In other words, constants may not occur; note that $x\,c$ can be replaced by $\mathtt {let\ } y\mathtt {\,=\,} {c}\mathtt {\ in\ } x\,y$.) We assume that each let-expression is annotated with an abstraction type that should be used for abstracting the value of the variable. Those abstraction types, as well as those for functions are automatically inferred by the CEGAR procedure described in Sect. 4.

Fig. 4.

Predicate abstraction rules

The rule PA-Unit just replaces the unit value with $\mathtt {end}$, which represents termination. The rule PA-Sexp overapproximates the value of a simple expression $a$. Here, $\theta _{\varGamma }$ is the substitution that replaces each variable $x$ of type $\mathbf {int}[Q'_1,\ldots ,Q'_n]$ in $\varGamma$ with $(Q'_1(x),\ldots ,Q'_n(x))$. For example, if $\varGamma =x\mathbin {:}\mathbf {int}[\lambda x.x\le 0,\lambda x.x\le 2], y\mathbin {:}\mathbf {int}[\lambda y.y\le x]$, then $\theta _{\varGamma }(\#_{2}(x)\wedge \#_{1}(y))$ is $\#_{2}(x\le 0,x\le 2)\wedge \#_{1}(y\le x)$, i.e., $x\le 2\wedge y\le x$. The formula $b_i Q_i(a)$ stands for $Q_i(a)$ if $b_i=\mathtt {true}$, and $\lnot Q_i(a)$ if $b_i=\mathtt {false}$. Basically, the rule generates branches for all the possible values $(b_1,\ldots ,b_k)$ for $(Q_1(a),\ldots ,Q_k(a))$, and combines them with node $\mathtt {br}_{\forall }$ (which indicates that this branch has been obtained by an overapproximation). To eliminate impossible values, we compute a necessary condition $\psi _{(b_1,\ldots ,b_k)}$ for $(Q_1(a),\ldots ,Q_k(a))=(b_1,\ldots ,b_k)$ to hold, and guard the branch for $(b_1,\ldots ,b_k)$ with $\psi _{(b_1,\ldots ,b_k)}$. The formula $\psi _{(b_1,\ldots ,b_k)}$ can be computed by using an SMT solver, as in ordinary predicate abstraction [3, 16]. (The rule generates $2^k$ branches, leading to code explosion. This is for the sake of simplicity; the eager splitting of branches is avoided in the actual implementation.) The rule PA-If is similar: branches for the then- and else-clauses are generated, but they are guarded by necessary conditions for the branches to be chosen.

The rule PA-Rand for random number generation is a kind of dual to PA-SExp. It applies an underapproximation, and generates branches for all the possible values $(b_1,\ldots ,b_k)$ for $(Q_1(x),\ldots ,Q_k(x))$ under the node $\mathtt {br}_{\exists }$. Each branch is guarded by a sufficient condition for the existence of a value for $x$ such that $(Q_1(x),\ldots ,Q_k(x)) = (b_1,\ldots ,b_k)$, so that for each branch, there must be a corresponding execution path of the source program. The rule PA-App for applications is the same as the corresponding rule of [16]. Finally, the rule PA-Prog for programs just transforms the body of each function definition, but adds a special node $\mathtt {call}$ to keep track of function calls. Note that a program is non-terminating if and only if it makes infinitely many function calls.

Example 1

Let us consider the following program LOOP.

$$\begin{aligned} loop\ h\ x=&\mathtt {let\ } b\mathtt {\,=\,} {(x>0)}\mathtt {\ in\ } \\&\mathtt {if\ } b \mathtt {\ then\ let\ } d \mathtt {\,=\,} \mathtt {*} _{\mathtt{int}} \mathtt {\ in\ let\ } y \mathtt {\,=\,} x+d \mathtt { in } h\;y\;(loop \; app)\;\mathtt {else} \;(\,)\\ app\ m\ k =&k\;m \qquad \qquad \mathtt {main} = \mathtt {let\ } r\mathtt {\,=\,} \mathtt {*} _{\mathtt{int}} \mathtt {\ in\ } loop \; app \; r \end{aligned}$$

LOOP is non-terminating; in fact, if $\mathtt {*} _{\mathtt{int}}$ is always evaluated to $1$, then we have:

$$\begin{aligned} \mathtt {main} \longrightarrow ^* loop \, app \,1 \longrightarrow ^* app \,2\,( loop \, app ) \longrightarrow ^* loop \, app \,2 \longrightarrow ^*\cdots \end{aligned}$$

Let ${\varGamma _{\mathbf{LOOP }}}$ be an abstraction type environment:

$$\begin{aligned}&loop:(\mathbf {int}[\lambda \nu .\nu >1] \rightarrow (\mathbf {int}[\lambda \nu .\nu >1] \rightarrow \star ) \rightarrow \star ) \rightarrow \mathbf {int}[\lambda \nu .\nu >1] \rightarrow \star \\&app:\mathbf {int}[\lambda \nu .\nu >1] \rightarrow (\mathbf {int}[\lambda \nu .\nu >1] \rightarrow \star ) \rightarrow \star \\ \end{aligned}$$

By using ${\varGamma _{\mathbf{LOOP }}}$ and the following abstraction types for $b$, $d$, and $r$:

$$\begin{aligned} b\mathbin {:}\mathbf {int}[\lambda \nu .\nu \ne 0], d\mathbin {:}\mathbf {int}[\lambda \nu .x+\nu > 1], r\mathbin {:}\mathbf {int}[\lambda \nu .\nu >1], \end{aligned}$$

the program LOOP is abstracted to the following program $D_{\mathbf{LOOP }}$.

For example, $\mathtt {let\ } b:\mathbf {int}[\lambda \nu .\nu \ne 0]\mathtt {\,=\,} {x>0}\mathtt {\ in\ } e$ is transformed by PA-Sexp as follows:

where

$$\begin{aligned} \varGamma = {\varGamma _{\mathbf{LOOP }}}, h:(\mathbf {int}[\lambda \nu .\nu >1] \rightarrow (\mathbf {int}[\lambda \nu .\nu >1] \rightarrow \star ) \rightarrow \star ), x:\mathbf {int}[\lambda \nu .\nu >1]. \end{aligned}$$

Here, recall that a non-zero integer is treated as $\mathtt {true}$ in the source language; thus, $\lnot ((x>0) \ne 0)$ means $x\le 0$. Since $\mathbf {Tree}(D_{\mathbf{LOOP }}) \in \mathbf {NonTermTrees}$, we can conclude that the program LOOP is non-terminating (based on Theorem 1 below).    $\square$

The soundness of predicate abstraction is stated as follows (see the full version [17] for a proof).

Theorem 1

Suppose $\vdash P\mathbin {:}\varGamma \leadsto {D}$. If $\mathbf {Tree}(D)\in \mathbf {NonTermTrees}$, then $P$ is non-terminating.

4 Counterexample-Guided Abstraction Refinement (CEGAR)

This section describes our CEGAR procedure to refine abstraction based on a counterexample. Here, a counterexample output by a higher-order model checker is a finite subtree $T$ of $\mathbf {Tree}(D)$, obtained by removing all but one branches of each $\mathtt {br}_{\forall }$ node. Figure 5 illustrates $\mathbf {Tree}(D)$ and a corresponding counterexample (showing $\mathbf {Tree}(D)\not \in \mathbf {NonTermTrees}$). In the figure, “$\cdots$” indicates an infinite path. For each $\mathtt {br}_{\forall }$ node, a model checker picks one branch containing a finite path, preserving the branches of the other nodes ($\mathtt {br}_{\exists }$, $\mathtt {call}$, and $\mathtt {end}$).

Fig. 5.

$\mathbf {Tree}(D)$ (left) and a corresponding counterexample (right)

We analyze each path of the counterexample tree to infer new abstraction types for refining abstraction. To that end, we need to distinguish between two types of paths in the counterexample tree: one that has been introduced due to overapproximation, and the other due to underapproximation. Figure 6 illustrates the two types. For each type, the lefthand side shows the computation tree of a source program, and the righthand side shows the tree generated by the abstract program. Thick lines show a path of a counterexample tree. In the example of Type I, the computation of a source program takes the then-branch and falls into a non-terminating computation, but predicate abstraction has introduced the spurious path taking the else branch, which was detected as a part of the counterexample. In the example of Type II, a source program generates a random number and non-deterministically branches to a non-terminating computation or a terminating computation. After predicate abstraction, the two branches by the random number generation have been merged; instead, the next deterministic computation step has been split into two by an overapproximation. This situation occurs, for example, for

$$\begin{aligned} \mathtt {let\ } x\mathbin {:}\mathbf {int}[\,]\mathtt {\,=\,} \mathtt {*} _{\mathtt{int}}\mathtt {\ in\ } \mathtt {let\ } y\mathbin {:}\mathbf {int}[\lambda y.y\ne 0]\mathtt {\,=\,} {x}\mathtt {\ in\ } \mathtt {if\ } y\mathtt {\ then\ } loop()\mathtt {\ else\ } (). \end{aligned}$$

The program generated by the abstraction is

Thus, the branches at $\mathtt{{*} _{\mathtt{int}}}$ in the original program have been moved to the branches at $\mathtt {br}_{\forall }$. The classification of the paths of a counterexample into Type I or II can be performed according to the feasibility of the path, i.e., whether there is a corresponding computation path in the source program. An infeasible path is Type I, since it has been introduced by an overapproximation, and a feasible path is Type II; it has a corresponding computation path, but the two kinds of non-determinism (expressed by $\mathtt {br}_{\exists }$ and $\mathtt {br}_{\forall }$) have been confused by predicate abstraction. We need to refine the predicates (or, abstraction types) used for overapproximation for a Type I path, and those used for underapproximation for a Type II path. In the example program above, by refining the abstraction type for $x$ to $\mathbf {int}[\lambda x.x\ne 0]$, we obtain

Thus, the branches on terminating/non-terminating paths are moved to the node $\mathtt {br}_{\exists }$.

Fig. 6.

Two types of paths in a counterexample

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

4.1 Dealing with Type II Paths

Given a program P and a Type II path $\pi$, we first prepare fresh predicate variables $R_1, \dots , R_k$ (called separating predicates), and replace each expression for random number generation $\mathtt {let\ } r_i\mathtt {\,=\,} \mathtt{{*} _{\mathtt{int}}}\mathtt {\ in\ } e_i$ with:¹

$$\begin{aligned} \mathtt {let\ } r_i\mathtt {\,=\,} \mathtt{{*} _{\mathtt{int}}}\mathtt {\ in\ } \mathtt {assume} (R_i(r_i));e_i. \end{aligned}$$

Here, an expression $\mathtt {assume} (\phi );e$ evaluates to e only if $\phi$ is $\mathtt {true}$. Then, we instantiate $R_i$’s so that the following conditions hold.

• (C1) P has no longer an execution path along $\pi$.

• (C2) If the execution along $\pi$ reaches $\mathtt {let\ } r_i\mathtt {\,=\,} \mathtt{{*} _{\mathtt{int}}}\mathtt {\ in\ } \mathtt {assume} (R_i(r_i));e_i$, there is at least one value for $r_i$ such that $R_i(r_i)$ holds.

Condition C1 is for separating the path $\pi$ at $\mathtt {br}_{\exists }$ node (recall Fig. 6; the problem of a Type II path has been that terminating/non-terminating paths are merged at $\mathtt {br}_{\exists }$ node). Condition C2 ensures that the paths separated from $\pi$ are not empty. By C2, for example, an absurd assume statement like $\mathtt {assume} (\mathtt {false} )$ is excluded out. We then add the instantiations of $R_1,\ldots ,R_k$ to the abstraction types for $r_1,\ldots ,r_k$.

For the example

$$\begin{aligned} \mathtt {let\ } x\mathbin {:}\mathbf {int}[\,]\mathtt {\,=\,} \mathtt {*} _{\mathtt{int}}\mathtt {\ in\ } \mathtt {let\ } y\mathbin {:}\mathbf {int}[\lambda y.y\ne 0]\mathtt {\,=\,} {x}\mathtt {\ in\ } \mathtt {if\ } y\mathtt {\ then\ } loop()\mathtt {\ else\ } () \end{aligned}$$

discussed above, we insert an assume statement as follows.

$$\begin{aligned} \mathtt {let\ } x\mathtt {\,=\,} \mathtt {*} _{\mathtt{int}}\mathtt {\ in\ } \mathtt {assume} (R(x)); \mathtt {let\ } y\mathtt {\,=\,} {x}\mathtt {\ in\ } \mathtt {if\ } y\mathtt {\ then\ } loop()\mathtt {\ else\ } (). \end{aligned}$$

Here, the Type II path $\pi$ is the one that goes through the else-branch. Thus, a condition $R(x)$ that makes it infeasible is $x\ne 0$. As a result, $\lambda x.x\ne 0$ is added to the abstraction type for $x$.

We sketch below how to instantiate $R_1,\ldots ,R_k$. Using the technique of [16] condition (I) can be reduced to a set of non-recursive Horn clauses over predicate variables. Condition (II) is, on the other hand, reduced to constraints of the form

$$\begin{aligned} R_1(\widetilde{x}_1)\wedge \cdots \wedge R_n(\widetilde{x}_n)\wedge C\Rightarrow \exists x.R(x)\wedge C'. \end{aligned}$$

Thus, it remains to solve (non-recursive) existentially quantified Horn clauses [4]. To solve them, we first remove existential quantification by using a Skolemization-based technique similar to [4]. We prepare a linear template of Skolem function and move existential quantifiers out of universal quantifiers. For example, given

$$\begin{aligned} \forall r. \left( \exists \nu .\nu \le 1 \wedge R(\nu )\right) \wedge \forall r.\left( R(r) \wedge \lnot (r>0) \Rightarrow \mathtt {false} \right) , \end{aligned}$$

we prepare the linear template $c_0+c_1r$ and transform the constraints into:

$$\begin{aligned} \exists c_0,c_1.\forall \nu .r. \left( \nu =c_0 + c_1r \Rightarrow \nu \le 1 \wedge R(\nu )\right) \wedge \forall \left( R(r) \wedge \lnot (r>0) \Rightarrow \mathtt {false} \right) . \end{aligned}$$

We then remove predicate variables by resolution, and get:

$$\begin{aligned} \forall \nu .r. \nu =c_0 + c_1r \Rightarrow \nu \le 1 \wedge \nu >0 \end{aligned}$$

Finally, we solve constraints in the form of $\exists \widetilde{x}.\forall \widetilde{y}. \phi$ and obtain coefficients of linear templates that we introduced in the first step. We adopt the existing constraint solving technique based [24] on Farkas’ Lemma. For the running example, we obtain $c_0 = 2, c_1 = 0$ as a solution of the constraints.

Now that we have removed existential quantification, we are left with non-recursive Horn clause constraints, which can be solved by using the existing constraint solving technique [23]. For the example above, we get

$$\begin{aligned} \forall \nu .r. \left( \nu =2 \Rightarrow \nu \le 1 \wedge R(\nu )\right) \wedge \left( R(r) \wedge \lnot (r>0) \Rightarrow \bot \right) \end{aligned}$$

and obtain $R=\lambda \nu .\nu >0$ as a solution.

5 Implementation and Experiments

We have implemented a non-termination verifier for a subset of OCaml, as an extension of MoCHi [16], a software model checker for OCaml programs. We use HorSat [5] as the backend higher-order model checker, and Z3 [20] as the backend SMT solver. The web interface of our non-termination verification tool is available online [1]. We evaluated our tool by experiments on two benchmark sets: (1) test cases consisting of higher-order programs and (2) a standard benchmark set on non-termination of first-order programs [7, 19]. Both experiments were conducted on a machine with Intel Xeon E3-1225 V2 (3.20GHz, 16GB of memory) with timeout of 60 seconds. The first benchmark set and an online demo page are available from our website [1].

Table 1. The result of the first benchmark set

Table 1 shows the result of the first evaluation. The columns ‘program’, ‘cycle’, and ‘time’ show the name of each test case, the number of CEGAR cycles, and the elapsed time (in milliseconds), respectively. For foldr_nonterm, we have used a different mode for a backend constraint solver; with the default mode, our verifier has timed out. All the programs in the first benchmark set are higher-order programs; so, they cannot be directly verified by previous tools. Our tool could successfully verify all the programs to be non-terminating (except that we had to change the mode of a backend constraint solver for foldr_nonterm).

We explain below two of the programs in the first benchmark set: inf_clos and alternate. The program inf_clos is:

$$\begin{aligned} \begin{array}{l} is\_zero\ n=(n=0)\qquad \qquad succ\_app\ f\ n=f\ (n+1)\\ f\ n\ cond=\mathtt {let\ } b\mathtt {\,=\,} {cond\ n}\mathtt {\ in\ } \mathtt {if\ } b\mathtt {\ then\ } \mathtt {(\,)}\mathtt {\ else\ } f\ n\ (succ\_app\ cond)\\ \mathtt {main} =f\ \mathtt {*} _{\mathtt{int}}\ is\_zero. \end{array} \end{aligned}$$

It has the following non-terminating reduction sequence:

$$\begin{aligned} \begin{array}{l} \mathtt {main} \longrightarrow ^*f\,1\, is\_zero \longrightarrow ^*f\,1\,( succ\_app \, is\_zero ) \longrightarrow ^*f\,1\,( succ\_app ^2\, is\_zero )\\ \longrightarrow ^*f\,1\,( succ\_app ^m\, is\_zero )\longrightarrow ^*\cdots . \end{array} \end{aligned}$$

Note that $succ\_app ^m\, is\_zero \; n$ is equivalent to $n+m=0$; hence $b$ in the function $f$ always evaluates to $\mathtt {false}$ in the sequence above. For proving non-termination, we need to reason about the value of the higher-order argument cond, so the previous methods for non-termination of first-order programs are not applicable.

The following program alternate shows the strength of our underapproximation.

$$\begin{aligned}&f\ g\ h\ z = \mathtt {let\ } x\mathtt {\,=\,} \mathtt{{*} _{\mathtt{int}}}\mathtt {\ in\ } \mathtt {if\ } x>0\mathtt {\ then\ } g\ (f\ h\ g)\mathtt {\ else\ } h\ (f\ h\ g)\\&proceed\ u = u\ \mathtt {(\,)}\qquad halt\ u = \mathtt {(\,)}\qquad \mathtt {main} = f\ proceed\ halt\ \mathtt {(\,)}\end{aligned}$$

It has the following non-terminating reduction sequence:

$$\begin{aligned} \begin{array}{l} \mathtt {main} \longrightarrow ^*f\,\textit{proceed}\;\textit{halt}\,\mathtt {(\,)}\\ \longrightarrow ^*\mathtt {if\ } 1>0\mathtt {\ then\ } \textit{proceed}(f\,\textit{halt}\;\textit{proceed})\mathtt {\ else\ } \cdots \longrightarrow ^*f\,\textit{halt}\,\textit{proceed}\,\mathtt {(\,)}\\ \longrightarrow ^*\mathtt {if\ } -1>0\mathtt {\ then\ } \cdots \mathtt {\ else\ } \textit{proceed}(f\,\textit{proceed}\;\textit{halt}) \longrightarrow ^*f\,\textit{proceed}\;\textit{halt}\,\mathtt {(\,)}\\ \longrightarrow ^*\cdots . \end{array} \end{aligned}$$

Here, since the arguments $g$ and $h$ are swapped for each recursive call, the program does not terminate only if positive and negative integers are created alternately by $\mathtt {*} _{\mathtt{int}}$. Thus, the approach of Chen et al. [7] (which underapproximates a program by inserting assume statements and then uses a safety property checker to prove that the resulting program never terminates) would not be applicable. In our approach, by using the abstraction type $\mathbf {int}[\lambda x.x>0]$ for $x$, $f$ is abstracted to:

Thus, both branches of the if-expression are kept in the abstract program, and we can correctly conclude that the program is non-terminating.

For the second benchmark, we have borrowed a standard benchmark set consisting of 78 programs categorized as “known non-terminating examples” [7, 19]. (Actually, the original set consists of 81 programs, but 3 of them turned out to be terminating.) The original programs were written in the input language for T2 [2]; we have automatically converted them to OCaml programs. Our tool could verify 48 programs to be non-terminating in the time limit of 60 seconds. According to Larraz et al. [19], CPPINV [19], T2-TACAS [7], APROVE [6, 10], JULIA [22], and TNT [13] could verify 70, 51, 0, 8, and 19 programs respectively, with the same limit but under a different environment. Thus, our tool is not the best, but competitive with the state-of-the-art tools for proving non-termination of first-order programs, despite that our tool is not specialized for first-order programs. As for the comparison with T2-TACAS [7], our tool could verify 7 programs for which T2-TACAS failed, and ours failed for 10 programs that T2-TACAS could verify.

6 Related Work

Methods for disproving termination have recently been studied actively [7, 8, 13, 19]. Most of them, however, focused on programs having finite control-flow graphs with numerical data. For example, the state-of-the-art method by Larraz et al. [19] enumerates a strongly connected subgraph (SCSG), and checks whether there is a computation that is trapped in the SCSG using a SMT solver. Thus, it is not obvious how to extend those techniques to deal with recursion and higher-order functions. Note that unlike in safety property verification, we cannot soundly overapproximate the infinite control-flow graph of a higher-order program with a finite one.

Technically, the closest to our work seems to be the series of recent work by Cook et al. [7, 8]. They apply an underapproximation by inserting assume statements, and then either appeal to a safety property checker [7], or apply an overapproximation [8] to prove that the underapproximated program is non-terminating for all execution paths. A problem of their underapproximation [7] is that when an assume statement $\textit{assume}(P)$ is inserted, all the computations such that $\lnot P$ are discarded; so if $P$ is wrongly chosen, they may overlook a non-terminating computation present in the branch where $\lnot P$ holds. As in the case for alternate discussed in Sect. 5, in the presence of higher-order functions, there may be no proper way for inserting assume conditions. In contrast, with our predicate abstraction, given a predicate $P$, we basically keep both branches for $P$ and $\lnot P$, and apply an underapproximation only if the satisfiability of $P$ or $\lnot P$ is not guaranteed (recall Fig. 1). In Cook et al.’s method [8], underapproximation cannot be applied after overapproximation, whereas under- and overapproximation can be arbitrarily nested in our method. Furthermore, although the framework of Cook et al. [8] is general, their concrete method can be applied to detect only non-termination in the form of lasso for programs having finite control-flow graphs. Harris et al. [14] also combine under- and overapproximation, but in a way different from ours: they use under- and overapproximation for disproving and proving termination respectively, not both for disproving termination.

There have also been studies on non-termination of term rewriting systems (TRS). Higher-order programs can be encoded into term rewriting systems, but the resulting analysis would be too imprecise. Furthermore, as mentioned in Sect. 1, the definition of non-termination is different.

Higher-order model checking has been recently applied to program verification [15, 16]. Predicate abstraction has been used for overapproximation for the purpose of safety property verification, but the combination of under- and overapproximation is new. Kuwahara et al. [18] have proposed a method for proving termination of higher-order programs; our new method for disproving termination plays a complementary role to that method.

The constraints generated in our CEGAR phase can be regarded as special instances of “existentially quantified Horn clauses” considered by Beyene et al. [4], where only acyclic clauses are allowed. Our constraint solving algorithm is specialized for the case of acyclic clauses. Incidentally, Beyene et al. [4] used existentially quantified clauses for verifying CTL properties of programs. Since non-termination can be expressed by the CTL formula $EG \lnot terminated$, their technique can, in principle, be used for verifying non-termination. Like other methods for non-termination, however, the resulting technique seems applicable only to programs with finite control-flow graphs.

7 Conclusion

We have proposed an automated method for disproving termination of higher-order programs. The key idea was to combine under- and overapproximations by using predicate abstraction. By representing the approximation as a tree-generating higher-order program, we have reduced non-termination verification to higher-order model checking. The mixture of under- and overapproximations has also required a careful analysis of counterexamples, for determining whether and how under- or overapproximations are refined. We have implemented the proposed method and confirmed its effectiveness. Future work includes optimizations of the implementation and integration with the termination verifier [18].