Termination and Non-termination Specification Inference
Wei-Ngan Chin1
tifact ** Complete* Consi

se
eu

cu m
e

*

ll
We

st

t
en

at e dAbstract
Techniques for proving termination and non-termination of imperative programs are usually considered as orthogonal mechanisms.
In this paper, we propose a novel mechanism that analyzes andproves both program termination and non-termination at the sametime. We first introduce the concept of second-order termination
constraints and accumulate a set of relational assumptions on them
via a Hoare-style verification. We then solve these assumptions withcase analysis to determine the (conditional) termination and nontermination scenarios expressed in some specification logic form.
In contrast to current approaches, our technique can construct asummary of terminating and non-terminating behaviors for eachmethod. This enables modularity and reuse for our termination andnon-termination proving processes. We have tested our tool on sample programs from a recent termination competition, and comparedfavorably against state-of-the-art termination analyzers.
Categories and Subject Descriptors D.2.4 [Software Engineering]: Software/Program Verification; F.3.1 [Logics and Meanings
of Programs]: Specifying, Verifying and Reasoning about Programs;
F.3.2 [Logics and Meanings of Programs]: Semantics of Programming Languages—Program Analysis
General Terms Languages, Theory, Verification
Keywords Program termination and non-termination analysis; BiAbductive inference; Hoare logic.

1.

Introduction

For the last ten years, we have seen a fruitful line of research on
proving termination [2–5, 7, 11–17, 19, 26, 29, 30, 34, 37–39] andnon-termination [1, 6, 8, 24, 31, 35, 47] of imperative programs.
Although these techniques for proving program termination and nontermination are often considered separately, a termination provermight deploy its own non-termination analysis mechanism to search
for a feasible counterexample when a termination proof fails. T REX[25] is one of the first works to combine two different terminationand non-termination proving techniques to alternatively assist eachother in a whole program analysis for non-recursive programs. Nevertheless, current techniques for proving non-termination are mostly
standalone techniques to existing termination proving mechanisms.
Permission to make digital or hard copies of all or part of this work for personal orclassroom use is granted without fee provided that copies are not made or distributedfor profit or commercial advantage and that copies bear this notice and the full citationon the first page. Copyrights for components of this work owned by others than theauthor(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or
republish, to post on servers or to redistribute to lists, requires prior specific permission
and/or a fee. Request permissions from permissions@acm.org.
PLDI’15, June 13–17, 2015, Portland, OR, USA.
Copyright is held by the owner/author(s). Publication rights licensed to ACM.
ACM 978-1-4503-3468-6/15/06. . . $15.00.
http://dx.doi.org/10.1145/2737924.2737993*

PLDI *

Ar*
AECDo Ev

Department of Computer Science, National University of Singapore
2School of Computing, Teesside University{chanhle,chinwn}@comp.nus.edu.sg, s.qin@tees.ac.uk* Easy to
ed
R
nt

1

Shengchao Qin2

alu

Ton Chanh Le1

To capture the termination and non-termination behaviors ofeach program, Le et al. [33] has recently proposed an integrated
specification logic with three temporal predicates Term M, Loopand MayLoop, which denote, respectively, the scenarios for definite
program termination (with a lexicographic ranking measure M madeof a list of positive integers), definite non-termination (with an unreachable post-condition) and possible (unknown) non-termination.
However, this framework currently requires temporal specifications
to be given by programmers.
We propose in this paper a modular inference framework that cananalyze both the termination and non-termination of each method
in a program. This approach is novel in that it guides us to perform suitable case-splits on pre-conditions that lead to definite
non-termination or definite termination, where possible. If a definite
termination (or non-termination) case is not yet attained, we may
perform a further case-split via an abductive inference [36] or decide to finish with a MayLoop classification to signify an unknown
outcome. For each method, our inference mechanism incrementally constructs a summary of its termination, non-termination or
unknown behaviors, so that it can be reused in the inference of theremaining methods higher-up in the calling hierarchy.
To support termination andnon-termination inference, we
void foo (int x, int y)
introduce unknown temporal
requires Upr (x, y)pre- and post-predicates in our
ensures Upo (x, y);specification logic to capture{ if (x < 0) return;termination or non-terminationelse foo(x + y, y); }behaviors (that are to be resolved by our inference). For
Figure 1. The foo example
example, in Figure 1, the pairof unknown pre-predicate Upr (x, y) and post-predicate Upo (x, y)in the specification of method foo denotes that the termination
or non-termination status of foo is currently unknown. While thepre-predicate Upr (x, y) in the method’s precondition guides the overall inference process with suitable case-splits, the post-predicate
Upo (x, y) in its postcondition is meant to capture the reachability
or unreachability of the method’s exits. This post-predicate will
be strengthened to false in scenarios where foo is definitely nonterminating. Moreover, it can also be used to trivially determine
base-case scenarios with immediate termination property. This combined use of unknown pre- and post-predicates is novel, since itallows us to modularly analyze each method (with the help of casesplits where needed) to obtain a comprehensive summary of themethod’s termination and non-termination characteristics.
Our main contribution lies in a single modular bi-abductive analysis that automatically infers sufficient preconditions respectively
for termination and non-termination of each method in a program.
The rest of this paper is organized as follows. Section 2 introduces
the novel unknown pre/post predicates and illustrates their use forinferring termination and non-termination properties of the foo example. Section 3 summarizes the background on the termination

W
hpred ::= c(v) ≡ (∃u · ρ)
ρ ::= κ ∧ πspec ::= W(ΨPre , ΦPost )κ ::= emp | v7→d(u) | c(v) | κ1 ∗κ2ΨPre ::= W(∃u·(ρ∧θ))
π ::= b | a | π1 ∧π2 | ¬π | ∃v·π
ΦPost ::= (∃u·(ρ∧Upo (v)))
b ::= true | false | v | b1 =b2
θ ::= Term [e] | Loop |a ::= e1 =e2 | e1 <e2 | v=null
MayLoop | Upr (v)e ::= k | v | k×e | e1 +e2 | −ewhere emp denotes an empty heap; v7→d(u) specifies a heap nodeof data type d; k is a constant; u, v are variables

Figure 2. A Specification Language
and non-termination reasoning with the temporal predicates. Section
4 shows how to generate a set of relational assumptions over the
unknown temporal predicates. Section 5 introduces the inference
algorithm to resolve the unknown predicates from their relational
assumptions. Section 6 provides the experimental results. Section 7
discusses related work and Section 8 concludes our paper.

2.

Overview of Our Approach

Specification Language. Le et al. [33] proposed three temporal
predicates, Term M, Loop and MayLoop, to help reason about program termination and non-termination. For the current evaluation,
we adopt these predicates as well as a rich underlying specification
language proposed by [9] that is able to express both heap properties with separation logic (κ in Figure 2) and pure (non-heap)
properties with Presburger arithmetic (π in Figure 2). This logic
uses a fragment of separation logic with the separation conjunction∗ to denote the disjointness of heap portions and the heap predicate
hpred (Figure 2) to specify various data structures. Moreover, tosimplify the presentation, we express a specification as a pair of preand post-condition (see spec in Figure 2). In our example programs,
specifications will be written using the usual requires...ensures...
form for better readability. Specifically for termination reasoning,
we have designed the termination measure M as a (finite) list ofarithmetic expressions [e] whose order is based on the lexicographic
ordering <l ( defined below) and e:es denotes a non-empty list withe and es as its head and tail, respectively.
[] <l e:(e1 < e2 ) ∨ (e1 = e2 ∧ es1 <l es2 )e1 :es1 <l e2 :es2

To facilitate termination and non-termination inference, weallow the use of an unknown temporal pre-predicate Upr (v) anda post-predicate Upo (v) in the specification language to indicate
the unknown termination status of a program. The solutions ofthese unknown predicates would be then derived by the inference
mechanism, as shown next. Note that the inferredWresult for each
unknown pre-predicate Upr (v) will be of the form (π ∧ θ) with θranging over {Term [e], Loop, MayLoop}; while the inferred result
for each unknown
post-predicate Upo (v) will be in a guarded
V
conjunction (π ⇒ post) with post being trueWor false. Such a
guarded form is equivalent to a disjunctive form (π ∧ post) when
the set of guards are complete. These unknown temporal predicatesare expressed in pure arithmetic domain. Heap-based properties in
our logic are currently handled prior to termination analysis.
Illustrating Example. We now demonstrate how our inference
mechanism derives the preconditions for termination and nontermination of method foo in Figure 1. Initially, the termination andnon-termination behaviors of method foo are captured by a pairof unknown pre-predicate Upr (x, y) and unknown post-predicate
Upo (x, y). Like the other known temporal predicates for terminationand non-termination reasoning, these unknown predicates are partof the specification logic’s formulas and can therefore be reasoned
in a similar way via Hoare-style verification. With the help of anenhanced entailment procedure, we shall prove that the preconditionof each method call is always satisfied and the postcondition always
holds at the end of the method body.
For example, the verification conditions (VCs) encountered by
Hoare-style forward verification of method foo are:(c1 ) x<0 ∧ Upr (x, y) ` Upo (x, y)(c2 ) x≥0 ∧ x0 =x+y ∧ y0 =y ∧ Upr (x, y) ` Upr (x0 , y0 )(c3 ) x≥0 ∧ x0 =x+y ∧ y0 =y ∧ Upr (x, y) ∧ Upo (x0 , y0 ) ` Upo (x, y)
The first VC (c1 ) is obtained from the base-case scenario when the
post-condition of the foo method is being proven. The second VC(c2 ) captures the proving of precondition for the recursive call, while
the last VC (c3 ) captures the entailment proving of the postconditionof method foo in the recursive branch. These VCs capture theunknown termination behaviors of both the caller (i.e. denoted by
the pair of predicates Upr (x, y) and Upo (x, y)) and the callee (i.e.
denoted by Upr (x0 , y0 ) and Upo (x0 , y0 )).
For these unknown predicates, we attempt to derive the strongest
possible post-predicate, where possible. As we intend to capture theunreachability of each post-predicate, the strongest post-predicate
in our analysis is actually false. If our inference for falsity of postpredicates fails, we denote its possible reachability by true insteadand then attempt to infer the weakest pre-predicate, where possible.
The temporal pre-predicates are ordered by the following implication hierarchy MayLoop ⇒r Loop and MayLoop ⇒r Term [e].
Amongst them, MayLoop is considered as the strongest one, which
is analogous to false in the domain of logical specification. The
intuition is that MayLoop can be used to denote the termination
property of any program though such a use would form a rather
poor specification, which is similar to how false could be naively(and redundantly) used as the precondition for any program. On
the other hand, the Loop and Term [e] predicates are incomparable
since they denote disjoint classes of programs (i.e. definitely nonterminating vs. definitely terminating programs, respectively). Ourinference thus attempts to discover the weaker Loop and Term [e]for its unknown pre-predicate, where possible.
From the earlier VCs, we infer three relational assumptions
where unknown pre-predicate Upr (x0 , y0 ) is related inductively toan earlier pre-predicate Upr (x, y) (see (a02 )), while unknown postpredicate Upo (x, y) is either expressed in base-case form (see (a01 ))or related inductively to an earlier occurrence of the post-predicate
Upo (x0 , y0 ) (see (a03 )).
(a01 ) x<0∧true ⇒ Upo (x, y)(a02 ) x≥0 ∧ x0 =x+y ∧ y0 =y∧Upr (x, y) ⇒ Upr (x0 , y0 )(a03 ) x≥0 ∧ x0 =x+y ∧ y0 =y∧Upo (x0 , y0 ) ⇒ Upo (x, y)We derive inductive definitions for these unknown predicates,in order to give the best possible interpretations to their temporal
predicates. In the case of post-predicate, we attempt to determine its
reachability or unreachability, so that we can immediately decideon either (base-case scenario for) termination or (inductive-case scenario for) definite non-termination. From the relational assumption(a01 ), we can immediately infer a base-case scenario x<0 where thefoo method would terminate. The other two relational assumptions
occur under a different scenario x≥0 which neither indicates definite termination nor definite non-termination. From these partial
instantiations on the two unknown temporal predicates, we refinethem to the following definitions:
Upr (x, y) ≡Upo (x, y) ≡x<0 ∧ Term(x<0 ⇒ true)∨∧x≥0 ∧ U1pr (x, y)(x≥0 ⇒ U1po (x, y))where two auxiliary unknown predicates are introduced for the input
scenario x≥0. Note that Term, short for Term [ ], is used to denotebase-case termination scenario where its lexicographic ranking

measure is trivially empty. Our unknown pre-predicate is being
expressed as a disjunction on either known or unknown temporal
resource constraints, while the post-predicate is being expressed asa guarded conjunction of either reachability (true), unreachability(false) or unknown. That is the two predicates are currently known
for the input scenario x<0 but unknown for the scenario x≥0.
As the precondition is now partially known, we could refine
each (a0i ) through a substitution with the partial definition ofUpr (x, y) and Upo (x, y) to get the new relational assumptions overthe unknowns:(a02a ) x≥0 ∧ x0 =x+y ∧ y0 =y ∧ x0 <0∧U1pr (x, y) ⇒ Term
(a02b ) x≥0 ∧ x0 =x+y ∧ y0 =y ∧ x0 ≥0∧U1pr (x, y) ⇒ U1pr (x0 , y0 )(a03a ) x≥0 ∧ x0 =x+y ∧ y0 =y ∧ (x0 ≥0⇒U1po (x0 , y0 ))⇒ (x≥0⇒U1po (x, y))

The relational assumption (a02a ) describes the reachability of thebase-case condition (i.e. x0 <0), denoted by Term, under the input
scenario x≥0. We can thus attempt a termination proof by synthesizing a ranking function for x≥0 but this proof fails. We thentry a non-termination proof by examining (a03a ) on unknown postpredicate to determine a condition for unreachability. Such condition
must ensure that the base case is not reached in the next recursion,i.e. x0 ≥0, and we refer to this as potential non-termination precondition. Since x0 =x+y, the condition x+y≥0 would be a trivial
potential non-termination pre-condition. However, our inferenceengine would discover a better (or weaker) condition, namely y≥0,for definite non-termination with the help of abductive inference.
With this, a case-split with the condition y≥0 and its negation y<0
is used to refine the definitions for U1pr (x, y) and U1po (x, y) into:
U1pr (x, y) ≡U1po (x, y) ≡y≥0 ∧ U2pr (x, y)(y≥0 ⇒ U2po (x, y))∨∧y<0 ∧ U3pr (x, y)(y<0 ⇒ U3po (x, y))Consequently, the following six specialized assumptions arederived from the earlier ones (a02a ), (a02b ) and (a03 ).
(a11 ) x≥0∧x0 =x+y∧y0 =y∧x0 <0∧y≥0∧U2pr (x, y) ⇒ Term(a12 ) x≥0∧x0 =x+y∧y0 =y∧x0 ≥0∧y≥0∧U2pr (x, y) ⇒ U2pr (x0 , y0 )(a13 ) x≥0∧x0 =x+y∧y0 =y ∧ (x0 ≥0∧y0 ≥0⇒U2po (x0 , y0 ))⇒ (x≥0∧y≥0⇒U2po (x, y)),1(a4 ) x≥0∧x0 =x+y∧y0 =y∧x0 <0∧y<0∧U3pr (x, y) ⇒ Term
(a15 ) x≥0∧x0 =x+y∧y0 =y∧x0 ≥0∧y<0∧U3pr (x, y) ⇒ U3pr (x0 , y0 )(a16 ) x≥0∧x0 =x+y∧y0 =y ∧ (x0 ≥0∧y0 <0⇒U3po (x0 , y0 ))⇒ (x≥0∧y<0⇒U3po (x, y))

The first three relational assumptions, (a11 ) − (a13 ), form a groupwhich will be analyzed together for the given input scenariox≥0∧y≥0. The next three relational assumptions, (a14 ) − (a16 ),form another group for the input scenario x≥0∧y<0.
The first group of relational assumptions, (a11 ) − (a13 ), allows
us to confirm a definite non-termination scenario, since we can use(a13 ) to determine the unreachability of its post-predicate U2po (x, y).
By using the hypothesis U2po (x, y)≡false for both occurrences ofthe post-predicate U2po (x, y) in (a13 ), we can inductively determine
the falsity (or unreachability) of U2po (x, y). Note our use of inductive
reasoning here which assumes the hypothesis that U2po (x, y) is
unreachable under pre-condition x≥0∧y≥0, in order to prove it.
The second group of relational assumptions, (a14 ) − (a16 ), suggests us to prove the method’s termination under the preconditionx≥0∧y<0 first, since its base case (captured by (a14 )) is possibly
reachable under this condition. This termination scenario is confirmed, once we have derived a lexicographic ranking measure [x]that is bounded and would moreover decrease with each recursive
invocation for the pre-predicate U3pr (x, y) using (a15 ).

As a summary of our combined analyses, we have effectively
derived the following definitions for the two unknown predicates:
Upr (x, y) ≡Upo (x, y) ≡x<0∧Term ∨ x≥0∧y<0∧Term[x]∨x≥0∧y≥0∧Loop(x<0 ⇒ true) ∧ (x≥0∧y<0 ⇒ true)∧(x≥0∧y≥0 ⇒ false)

Note how the unknown temporal predicates U2pr (x, y) and U2po (x, y)are being resolved to be Loop and an unreachable false for input
scenario y≥0, respectively. In contrast, the unknown predicatesU3pr (x, y) and U3po (x, y) are being resolved to be Term [x] and areachable true state for input scenario y<0, respectively.
Using the inferred predicate definitions, we can finally construct
the following case-based specification ([20]) which fully captures
termination and non-termination behaviors for method foo.
case {
x < 0 → requires Term ensures true;x ≥ 0 → case {y < 0 → requires Term [x] ensures true;y ≥ 0 → requires Loop ensures false; }}2.1

Other Examples

Our termination and non-termination inference is completely automated. By allowing unknown temporal predicates into functionalcorrectness specifications, our inference mechanism can freely leverage on prior infrastructures to (i) handle a wider class of programs,
and to (ii) improve the accuracy of the inference results. Note thatprior safety specifications for the analyzed methods might be manually given or be automatically derived by other inference mechanisms, but they are orthogonal to our current proposal.
We list below some interesting examples to demonstrate how ourinference mechanism works with programs that already have somesafety specifications.
Nested Recursion. For examples with nested recursion, such as
the Ackermann function and the McCarthy 91 function in Figure
3, some knowledge on its output may be crucial for the inferenceof their termination and non-termination properties. Without any
specification, our inference mechanism returns incomplete summaries on the terminating and non-terminating behaviors of these
two functions. The result for the Ackermann function is:case {
m=0
m<0 ∨ n<0m>0 ∧ n≥0

→ requires Term ensures true;→ requires Loop ensures false;→ requires MayLoop ensures true; }While the inference shows that this function is terminating when
m=0 (base case) or non-terminating when m<0 ∨ n<0, it cannot
prove the termination of the function under the input scenario
m>0∧n≥0 since the value of the second argument in the lastrecursive call is unknown (or unbounded). However, with thestronger specification given in Figure 3(a), with an lower boundres ≥ n+1 on the function’s returned value, denoted by res, ourinference mechanism can replace MayLoop in scenario m>0∧n≥0
by Term [m, n] where [m, n] is a valid lexicographic ranking function.
Similarly, without specification, the inference only shows that the
McCarthy 91 function terminates in its base case when n>100.
However, with the specification given in Figure 3(b), our inference
can prove that the function terminates for all inputs.
While our termination inference mechanism does not directly
infer postconditions, it has been made to work with other automatedpostcondition inference sub-systems, such as [23, 40]. Such postcondition inference sub-systems are orthogonal to our proposal, andcan be leveraged to provide a more comprehensive solution for fully
automated termination and non-termination inference.

int Ack (int m, int n)requires true ensures res ≥ n+1;
{ if (m == 0) return n + 1;
else if (n == 0) return Ack(m − 1, 1);else return Ack(m − 1,Ack(m, n − 1)); }(a)

int Mc91 (int n)requires true
ensures n≤100∧res=91 ∨ n>100∧res=n−10;{ if (n > 100) return n − 10;else return Mc91(Mc91(n + 11)); }(b)

Figure 3. Functions with Nested Recursion: Ackermann function (a) and McCarthy 91 function (b)data node { node next; }pred lseg(root, q, n) ≡ root=q ∧ n=0∨ root7→node(p) ∗ lseg(p, q, n−1)pred cll(root, n) ≡root7→node(p) ∗ lseg(p, root, n−1)void append (node x, node y)requires lseg(x, null, n) ∧ x6=null
ensures lseg(x, y, n);requires cll(x, n) ensures true;{ if (x.next == null) x.next = y;else append(x.next, y); }Figure 4. Specification with Implementation for append method of two linked lists
Heap-Manipulating Programs. Our inference mechanism canbe readily integrated into existing verification frameworks (such as[9], or even shape inference system [32]) that reason about safety
properties of heap programs via separation logic [41]. Such an
extension can be applied to help prove the termination and nontermination of heap-manipulating programs.
Figure 4 shows the specification and implementation (for theverification) of the method append that concatenates two linked
lists x and y. With the separation conjunction ∗ and the points-to
operator 7→ of separation logic, the heap predicate lseg(root, q, n)
represents a list segment from root to q with n elements. Thispredicate can then be used in the declarations of other predicates,
such as cll(root, n) for circular lists. Using these two predicates,
we can capture two safety specifications of append in Figure 4.
In the first scenario when the input x is a null-terminating
list with size n, our inference mechanism is able to show that themethod append always terminates with the ranking function [n]. In
the second scenario where x is a circular linked list, our inference
can show that append is definitely non-terminating, after confirming(by induction) that its postcondition can be strengthened to false.
These examples highlight the modular nature of our non-terminationand termination inference mechanism, which can be built on top ofother inference mechanisms.

3.

Technical BackgroundSo far we have illustrated a unified specification logic with threeknown temporal predicates: Term [e], Loop and MayLoop. Semantically, these predicates can be defined using resource capacities(on lower and upper bounds) of execution length, i.e. Term [e] =df
RCh0, f([e])i, Loop =df RCh∞, ∞i, and MayLoop =df RCh0, ∞i.
The resource predicate RChL, Ui specifies a resource capacity witha lower bound L and an upper bound U. It is satisfied by each program state whose resource capacity (l, u) is subsumed by (L, U), i.e.
L≤l and u≤U. Note that the function f([e]) obtains a finite boundthrough an order-embedding of [e] into naturals.
Verification conditions involving these temporal predicates canbe discharged by a resource consumption entailment `t , that is used
to account for (lower and upper bound) resources that are utilizedby each code fragment. Such entailment can be used to analyze
termination or non-termination property for some given method via
resource reasoning. Given the temporal constraint θa associated withthe current program state ρ and the temporal resource constraint
θc (of some code fragment that must be executed), the entailmentρ ∧ θa `t θc I θr checks whether the execution resource requiredby constraint θc can be met by the execution resource of constraint
θa or not. If it succeeds, the entailment will return the remaining
execution resource that is denoted by residue θr .
In terms of the actual execution capacity, this consumption
entailment can be formalized by the following rule:ρ ⇒ Uc ≤Ua Lr = La −L Lc Ur = Ua −U Uc ρ ⇒ Lr ≤Urρ ∧ RChLa , Ua i `t RChLc , Uc i I RChLr , Ur i

where two subtraction operators are designed to cater to an integer
domain extended with the ∞ value (i.e. N∞ ):L1 −L L2 ≡ min{r ∈ N∞ | r + L2 ≥ L1 }U1 −U U2 ≡ max{r ∈ N∞ | r + U2 ≤ U1 }, if U1 ≥U2These two operators are essentially integer subtraction operators,
except that their results are never negative and such that ∞−L ∞ = 0
and ∞−U ∞ = ∞. They are formulated in this way to give thebest (or largest) possible lower and upper bound values to denotethe execution capacity of residue. In addition, the subtraction
Ua −U Uc requires a check for upper bound execution capacity,
namely ρ ⇒ Uc ≤Ua . This check is important to ensure that resource
consumption is within the specified upper bound, and will also
ensure that the residue is a valid resource capacity.
The resource implication operator ⇒r on execution capacity,used in the implication hierarchy of known temporal predicates, canbe defined based on the following subsumption relation:
L1 ≤L2 U2 ≤U1
RChL1 , U1 i ⇒r RChL2 , U2 i

From this definition, MayLoop is the strongest pre-predicate in
the subsumption hierarchy since it has the maximum execution capacity (0, ∞). It can subsume either Loop (with execution capacity(∞, ∞)) or Term [e] (with execution capacity (0, f([e]))) predicates. Note that the implication operator ⇒r is only weakly related
to the resource consumption entailment operator, `t , as follows:(θa ⇒r θc ) ⇒ ∃θr · θa `t θc I θr
For termination and non-termination inference, we have introduced unknown predicates Upr (v) for precondition and Upo (v) for
postcondition for each method, with Upr (v) denoting some execution capacity, and Upo (v) specifying reachability of a method with aset of formal parameters v. To support its inference, we will haveto extend the resource entailment procedure to handle entailments
between known and unknown temporal constraints. V
The most general form of temporal entailment is ρ∧ i Uipo (vi )∧θa `t θc I (θr , R), where each Uipo (vi ) is an unknown postpredicate accumulated into the program state after a recursive
method call. The temporal constraint θa in the antecedent of theentailment might be an unknown pre-predicate Upr (v) or a known
temporal predicate. The temporal constraint θc can be either an
unknown post-predicate Upo (v) or a known predicate. The residue
constraint θr denotes the residual capacity after entailment. Each
relational assumption R for the unknown temporal predicates is a
pre-requisite to ensure the validity of the entailment when either θaor θc is unknown. It is defined as below.

Prog
tdecl
field
meth
e

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

tdecl methdata c { field }tv
t ::= c | bool | int | voidt mn([ref] t v) (ΨPre , ΦPost ) {e}null | k | v | v.f | v:=e | v1 .f :=v2 |new c(v) | e1 ; e2 | t v; e | mn(v) |if v then e1 else e2 | return v
where c is a data type name; mn is a method name;k is a primitive constant; f is a field name; v is a variable

Figure 5. A Core Imperative Language
assumption R in the
D EFINITION 1. The temporal relational
V
residue of a temporal entailment ρ ∧ i Uipo (vi ) ∧ θa `t θc I (θr , R)
can be defined as follows:(i) R ≡ true, if both θa and θc are known predicates from
{Term V[e], Loop, MayLoop}.
(ii) R≡ρ∧ i Uipo (vi ) ⇒ θc , if θc is an unknown post-predicate.
(iii) R ≡ ρ∧θa ⇒ θc , otherwise.
This temporal entailment can be integrated into an entailment
system with frame Ψ ` Φ ; Ψr , to obtain a new entailment
procedure of the form Ψ ` Φ ; (Ψr , S), that also captures in
its residue the set of relational assumptions S generated by the
temporal sub-entailments. The rules to discharge entailments oflogic formulas with disjunctions are:Ψ=W

[ENT−DISJ−LHS]
V j
V∀i · (ρi ∧ j θij ) ` Φ ; (Ψir , Si )i ∃vi · (ρi ∧ j θi )SWΨ ` Φ ; ( i ∃vi · Ψir , i Si )[ENT−CONJ]Vρa ` ρc ; ρr
ρr ∧ i Uipo (vi ) ∧ θa `t θc I (θr , R)V iVρa ∧ i Upo (vi )∧θa ` ρc ∧θc ; (ρr ∧ i Uipo (vi )∧θr , {R})4.

Generating Temporal Assumptions

1: procedure solve(M)// M = {ti mn i (t v) (Uipr , Uipo ) {e} {Si , Ti } | 1≤i≤n}2:Θ ← {Uipr ≡ Uipr , Uipo ≡ Uipo | 1≤i≤n}// Initial defns for unknown pre/post predicates3:for each mni in M do4:
β ← syn_base(Si , Ti )5:Θ ← refine_base(Θ, Uipr , Uipo , β)SS
6:S ← Si ; T ← Ti ; iter ← 0
7:
S ← spec_relass(S, Θ); T ← spec_relass(T , Θ)8:
G ← reach_graph(S)// Reachability graph for unknown pre-predicates9:for each scc in G do
10:(r, Θ) ← TNT_analysis(G, scc, T , Θ)11:
if ¬r ∧ iter < MAX_ITER then iter++; goto 7
12:
if iter ≥ MAX_ITER then break13:
T ← spec_relass(T , Θ)14:
G ← graph_update(G, Θ)
15:
return finalize(Θ)

Figure 6. Overall Inference Algorithmρ∧Loop ⇒ θc and ρ∧MayLoop ⇒ θc are trivially valid for any program state ρ because the constraints Loop and MayLoop can accept
any temporal constraints in the RHS [33]. Finally, ρ∧θa ⇒ Term M istrivial if the callee n, whose termination is denoted by the temporalconstraint Term M, and the caller m are not mutually recursive.
Note that assumptions of the form ρ∧U1pr (v1 ) ⇒ U2pr (v2 ) are nottrivial for any caller m and callee n. However, when m and n are in
two different scc groups, this kind of assumptions can be avoided
if we do a bottom-up verification and inference in which the (non)termination of the callee n is inferred and the unknown U2pr (v2 ) is
instantiated before the caller m is processed.
For each method declaration, we collect a set of relational
assumptions S during the verification of its body, and another setof relational assumptions T at the method’s exit points via theentailment for proving the post-condition, as shown below:

In this section, we show how our new entailment procedure is incorporated into Hoare logic to generate a set of relation assumptions
over the unknown temporal constraints.

[TNT−METH]` {ΨPre } e {Ψ, S} Ψ ` ΦPost ; (Ψr , T )t0 mn(t v) (ΨPre , ΦPost ) {e} {S, T }Language. To formalize this task, we provide a core language(Figure 5) with usual constructs, such as data structure declaration
tdecl , method declaration meth, method call, assignment. This corelanguage does not include the while-loop construct, as it assumes anautomatic translation of loops into tail-recursive methods. For int
type, we assume the use of arbitrary precision integers.
A method declaration consists of a specification with pre- andpost-condition and its body. Primitive/library methods do not havea body and must have their specifications (including termination)
pre-declared. For termination and non-termination inference, a pairof unknown pre- and post-predicate are automatically added into thespecification of each method whose termination status is unknown.

The termination and non-termination inference engine is invokedwhen a whole group of mutually recursive methods are verified andtheir sets of relational assumptions are collected, as shown in therule [TNT−INF] below.

Hoare rules. To support inference, Hoare judgment is formalizedas ` {ΨPre } e {ΦPost , S}, where S is a generated set of temporal
assumptions. For illustration, we show the rule for method call:This section is devoted to the solve procedure used to infer thedefinitions for the unknown pre/post-predicates, based on the set of
relational assumptions generated by Hoare-style verification. The
overall algorithm is shown in Figure 6.
In this algorithm, Θ is used to store the set of definitions inferred
thus far for the unknown temporal predicates. Since a key ideaof our inference mechanism is case analysis that incrementally
separates the terminating and non-terminating behaviors of theanalyzed methods, the definition for each unknown predicate might
be split into multiple scenarios, for which termination is either
known or unknown.

[TNT−CALL]t0 mn(t v) (ΨPre , ΦPost ) {e} ∈ ProgΨ ` ΨPre ; (Φ, S1 ) Ψr = Φ ∗ ΦPost S2 = filter(S1 )` {Ψ} mn(v) {Ψr , S2 }To facilitate the termination inference, at method calls, we collect
only nontrivial assumptions of unknown temporal constraints. We
list below trivial relational assumptions, which will be removed by
the function filter as shown in the rule [TNT−CALL].
Firstly, the relational assumption ρ∧θa ⇒ θc is trivial for any θaand θc if the context ρ is unsatisfiable. Secondly, the assumptions[TNT−INF]
Mscc = {t0i mn i (ti vi ) (Uipr (vi ), Uipo (vi )) {e} {Si , Ti } | 1≤i≤n}
Mscc
solve(Mscc )The solve procedure infers definitions for unknown temporal
predicates and will be depicted in detail next.

5.

Inferring Termination and Non-Termination

D EFINITION 2 (Unknown Temporal Predicates). During the inference process, the definitions for a pair of unknown pre-predicate

Upr (v) and post-predicate Upo (v) are of the form
Upr (v) ≡Wii (πi ∧ θpr ) and Upo (v) ≡Vthe method, as follows:Wρ =W {(ρi /{v}) | ρi ∧Upr (v) ⇒ θci ∈ S}
% = {(βj /{v}) | βj ∧true ⇒ Upo (v) ∈ T }i
i (πi ⇒ θpo )iwhere each θpris either a known or unknown pre-predicate andiθpo is either true, false or an unknown post-predicate. The setof guards {π1 , . . . , πn } must be (1) feasible, i.e. ∀i · SAT(πi ), (2)exclusive, i.e. ∀i, j·i6=j ⇒ UNSAT(πi ∧πj ), and (3) exhaustive, i.e.
π1 ∨π2 ∨. . .∨πn ≡ true.

syn_base(S, T ) = % ∧ ¬ρwhere ρ/{v} ≡ ∃(FV(ρ)−{v}) · ρ. Using our running example, wehave S = {a02 } and T = {a01 , a03 }:(a01 ) x<0∧true ⇒ Upo (x, y)

The initial form of each unknown predicate is the predicate itself
with guard condition true, e.g. Upr (v) ≡ true∧Upr (v). At the endiiof the analysis, all θprand θpobecome known.
The inference deals with two groups of temporal relational
assumptions collected by rule [TNT−METH], namely
1. Pre-assumptions S collected when proving preconditions at
method calls. They can be used to infer (i) ranking functions fortermination proving, and (ii) temporal reachability graph thatguides our search for proving termination vs. non-termination.
2. Post-assumptions T collected when proving postconditions contain information about unknown post-predicates. They can beused to infer (i) termination base cases, (ii) inductive unreachability to prove non-termination or (iii) new conditions for thecase analysis.
The algorithm in Figure 6 first derives the base case of each analyzed method (line 4), and then refines the definitions of unknown
temporal predicates in Θ with these newly inferred cases (line 5).
After updating the set of relational assumptions (line 7), our algorithm (re-)builds the temporal reachability graph G from the latest
S (line 8).
For each scc of the graph G in the bottom-up topological order,
the analysis attempts to prove either termination or non-terminationor to infer new cases for case-splitting and then updates the set
Θ with the inferred result (line 10). If every unknown temporal
predicate corresponding to the current scc is resolved into known
predicates, the inference continues with the next sccs after updating
the post-assumptions in T (line 13) and the graph G (line 14) with
the new inferred known predicates. Otherwise, it restarts the corealgorithm (line 11) with the updated Θ, whose elements have beenrefined into new sub-cases.
The algorithm halts when every unknown predicate has been resolved or the number of iterations reaches the maximum MAX_ITER
pre-set by users. In the latter case, the remaining unknown predicates in Θ will be marked as MayLoop by an auxiliary procedure
finalize. Next we will explain each inference step in some detail.
5.1

Inferring Base Case Termination

Identifying the conditions for base-case termination is an importantfirst step before any other analyses. Formally:
D EFINITION 3 (Base Case Pre-Condition). Each base case termination precondition of a method must satisfy the following three
conditions:(i) Its method’s exit is reachable from it.
(ii) No mutually recursive method call is met in executions startingfrom this pre-condition.
(iii) All other method calls encountered from this pre-condition
must have been proven to terminate.
While a syntactic-based approach that identifies base-case termination from its control-flow may be sufficient, we propose asemantics-based approach which infers a method’s base case precondition from the two sets of assumptions S and T collected from(a02 ) x≥0 ∧ x0 =x+y ∧ y0 =y∧Upr (x, y) ⇒ Upr (x0 , y0 )(a03 ) x≥0 ∧ x0 =x+y ∧ y0 =y ∧ true∧Upo (x0 , y0 ) ⇒ Upo (x, y),Each post-assumption βj ∧true ⇒ Upo (v) ∈ T , whose antecedent does not contain any unknown post-predicate, capture a potential base-case termination condition. Due to over-approximation,
the actual base-case condition (overW the method’s parameters v) mustbe formed by such conditions ( βj ), conjoined with the negationof contexts (¬ρ) for the recursive calls. By identifying the base-casecondition in {a01 } and conditions for recursive pre-assumption in{a02 }, we can precisely infer syn_base(S, T ) = x<0∧¬(x≥0).
With the inferred base case β = syn_base(S, T ) (line 4),
we can now invoke the procedure refine_base (line 5) to refine(or specialize) the unknown predicates Upr (v) and Upo (v), before
updating their definitions in Θ (via the operator ⊕) as shown below.
W
W µi ≡ ¬β∆pr = (Upr (v) ≡ (µi ∧ Uipr (v)) ∨ (β ∧ Term))V∆po = (Upo (v) ≡ (µi ⇒ Uipo (v)))
S iiΩ = {Upr (v) ≡ Upr (v), Uipo (v) ≡ Uipo (v)}refine_base(Θ, Upr (v), Upo (v), β) = Θ ⊕ ({∆pr , ∆po } ∪ Ω)

Since the method’s termination status in the remaining conditionµ = ¬β is unknown. In the new definitions of Upr (v) and Upo (v),each pair of fresh predicates Uipr (v) and Uipo (v) is associated witha disjunct µi in the disjunctive normal form of µ. For our running
example, this refinement leads to:Upr (x, y) ≡Upo (x, y) ≡x<0 ∧ Termx<0 ⇒ true∨∧x≥0 ∧ U1pr (x, y)x≥0 ⇒ U1po (x, y)

After the unknown predicates have been updated with base-casetermination conditions, we transform the sets of relation assumptions
by using the procedure spec_relass (line 7) described next.
5.2

Specializing Relational Assumptions

Whenever some unknown predicates in Θ receive new definitions,
our inference algorithm will update its sets of relational assumptions
with the procedure spec_relass. Its first parameter is a set of relational assumptions. Its second parameter Θ contains the definitionsof unknown predicates.
For each relational assumption with unknown predicates, the procedure spec_relass finds the current definitions of these unknown
predicates in Θ and substitutes them directly into the assumption.
As the definition of each unknown predicate consists of exclusiveand complete guards, we can further split each substituted assumptions into multiple specialized assumptions. We show below just one
example where spec_relass is called with a new pre-assumption
with two unknown predicates.
W
W
2j
1i
U2pr (v2 )≡ m
U1pr (v1 )≡ ni=1 (ρ1i ∧θpr ) ∈ Θ
j=1 (ρ2j ∧θpr ) ∈ Θ
2j1i
C = {ρ∧ρ1i ∧ρ2j ∧θpr ⇒ θpr | 1≤i≤n, 1≤j≤m}
spec_relass({ρ∧U1pr (v1 ) ⇒ U2pr (v2 )} ∪ S, Θ) =C ∪ spec_relass(S, Θ)For our running example, the relational assumption (a02 ) was
specialized by its earlier partial definition into two more specialized
assumptions: (a02a ) and (a02b ).

16: procedure TNT_analysis(G, scc, T , Θ)17:r ← true18:
O ← scc_succ(scc, G)
19:
if O = {} then20:
if scc has one node Upr without cyclic edge then21:
Upo ← the post-pred corresponding to Upr22:Θ ← Θ ⊕ {Upr ≡ Term, Upo ≡ true})23:
else (r, Θ) ← prove_NonTerm(scc, T , Θ)24:else if ∀θ ∈ O · θ ≡ Term [e] then25:(r, Θ) ← prove_Term(G, scc, Θ)26:
if ¬r then (r, Θ) ← prove_NonTerm(scc, T , Θ)27:else (r, Θ) ← prove_NonTerm(scc, T , Θ)28:
return (r, Θ)

29: procedure prove_Term(G, scc, Θ)30:C ← {gen(e) | e≡(Uipr , ρ, Ujpr )∈G(E) ∧ Uipr , Ujpr ∈scc}31:
Γ ← syn_rank(C)32:
if Γ 6= {} then33:
D ← subst_rank(scc, Γ)34:
return (true, Θ ⊕ D)
35:
else return (false, Θ)Figure 8. Procedure for Proving Termination over a scc

Figure 7. Core TNT Inference Algorithm
5.3

Resolving Temporal Reachability Graph

The core of our inference algorithm (in Figure 6) incrementally resolves the unknown predicates present in the (specialized) relational
pre-assumptions. If its attempt fails, it would also derive conditions
for the next case analysis. This core algorithm uses a reachability
graph G, constructed from pre-predicates in S, to guide its proof
search. Formally:
D EFINITION 4 (Temporal Reachability Graph). Given a set of preassumptions S, a temporal reachability graph G = (V, E) isconstructed from a set of vertices V and a set of labeled edges
E, as follows. For each pre-assumption ρ∧θa ⇒ θc ∈ S, we add
two vertices θa and θc into V and an edge (θa , ρ, θc ) from θa to θclabeled by ρ into E.
G1

G2

ρ(a02b )U1pr

ρ(a02a )Termρ(a12 )

ρ(a15 )

U2pr

U3pr

ρ(a14 )Term

For example, the two graphs G1 and G2 are built for the inferenceof the running example. G1 is constructed from pre-assumptions(a02a ) and (a02b ) obtained after base case inference. The edges of G1
are labeled by ρ(a02a ) and ρ(a02b ), the contexts in (a02a ) and (a02b )resp., e.g. ρ(a02b ) ≡ (x≥0∧x0 =x+y∧y0 =y∧x0 ≥0). The self-loop
edge on node U1pr denotes the case when the latest values of program
variables (i.e. x0 ≥0), are still in the same loop condition as theirinitial values (x≥0). The edge from U1pr to Term indicates the basecase is reached when x0 <0. Similarly, the graph G2 is constructedfrom pre-assumptions (a14 ), (a15 ) and (a12 ) after a new case splity≥0 and y<0 has been inferred.
Our core algorithm firstly partitions G into strongly connectedcomponents (scc), (e.g. dashed boxes in G1 and G2 ), whereby
each unknown temporal predicate denotes an unknown behavior.
Moreover, this unknown predicate is mutually dependent on theother predicates in the same scc. Using a bottom-up approach, theinference mechanism processes each scc in a topologically sorted
order. With this approach, termination and non-termination proofs
for phase-change programs [14] and that for mutual recursion areeasily supported.
D EFINITION 5 (scc’s successors). Given a graph G, the outside
successors of a scc in G is the set of all successors of any vertex inthis scc but excluding the scc itself,
scc_succ(scc, G) =[{succ(v, G) | v ∈ scc} \ scc

where succ(v, G) returns all successors of the vertex v.

Our core algorithm, named TNT_analysis, for manipulatingeach scc is outlined in Figure 7. After this analysis, if all vertices inthe scc are resolved as known temporal predicates, our procedure
returns the result r=true. Otherwise, it returns r=false to allow
inference mechanism to restart for the next iteration (from line 7
in Figure 6). Moreover, upon termination of this procedure, some
unknown pre- and post-predicates in store Θ, are updated with their
new definitions.
Our procedure (Figure 7) uses the set O of the scc’s successors to determine whether termination proof (by sub-procedure
prove_Term), or non-termination proof (by prove_NonTerm),
should be applied to resolve the unknown temporal predicates.
Specifically, when the scc has only one unknown node Upr without
any cyclic edge and successor (line 20), we resolve the unknown
pre-predicate Upr ≡ Term and its corresponding post-predicate
Upo ≡ true for trivial termination (line 22). Moreover, when the set
O is nonempty, the procedure invokes prove_Term with ranking
function synthesis only if every element of O is a known Term [e]predicate (line 24-25).
For the running example, the procedure applies termination
proofs for the left scc in G1 and the middle scc in G2 . For theleft scc in G2 , it applies a non-termination proof directly. In the next
sub-sections, we present the sub-procedures for proving terminationand non-termination over a scc.
5.4

Inferring Ranking Function

For proving termination on a scc, we implement the procedure
prove_Term (sketched in Figure 8) to find a linear ranking function
for each unknown pre-predicate in this scc by using a constraintbased technique [22, 23, 38, 42] with Farkas’ lemma [43].
Initially, we create a unique ranking function template for each
unknown pre-predicate Upr (v1 , .., vn ) ∈ scc by the procedure
gen_rank, defined as
gen_rank(Upr (v1 , . . . , vn )) = c0 +Pn

i=1 ci vi

where c0 , c1 , . . . , cn are unknown coefficients of the ranking function. Next, we generate a set of constraints over these ranking functions from every edge in G that connects two nodes in the scc(line 30). That is, given an edge e ≡ (Uipr (vi ), ρ, Ujpr (vj )) ∈ G(E)s.t. Uipr (vi ), Ujpr (vj ) ∈ scc, the constraint generated from it isri (vi )=gen_rank(Uipr (vi ))rj (vj )=gen_rank(Ujpr (vj ))gen(e) = ∀vi , vj · ρ ⇒ (ri (vi ) > rj (vj ) ∧ ri (vi ) ≥ 0)This constraint indicates that the ranking function ri (vi ) is bounded
and decreasing across a (mutually) recursive method call under thecall context ρ. For example, the constraint generated from the middle
scc in G2 is∀x, y · x≥0∧x0 =x+y∧y0 =y∧x0 ≥0∧y<0 ⇒r(x, y)>r(x0 , y0 ) ∧ r(x, y)≥0which is then solved by syn_rank to obtain the ranking functionr(x, y) = x. The method syn_rank (line 31) solves the generated
constraints by applying Farkas’ lemma on them to obtain another setof constraints over their unknown coefficients, which can be solved
by a nonlinear solver, such as [28], to get the actual values of these36: procedure prove_NonTerm(scc, T , Θ)37:
for each Uipr ∈ scc do
38:
Ti ← filter_rel(T , Uipr )S
39:
Ci ← {abd_inf(t) | t ∈ Ti }V40:r ← i (Ci 6= {} ∧ ∀c ∈ Ci · (c ≡ true))41:
if r then D ← {Uipr ≡ Loop, Uipo ≡ false | Uipr ∈scc}
S
42:
else D ← i subst_unk(Ci , Uipr , Uipo )43:

return (r, Θ ⊕ D)

Figure 9. Proc. for Proving Non-Termination over a scc
unknowns. The result is a substitution Γ which maps each unknown
coefficient to its actual value.
If the ranking function synthesis succeeds, we update each unknown pre-predicate in this scc into Term with an actual ranking function (line 34 in Figure 8). Otherwise, we prove nontermination on this scc (line 26 in Figure 7). The ranking function for a pre-predicate can be obtained by applying the substitution Γ to its ranking function template, as shown below. Note that
subst_rank({}, Γ) = {}.
r = Γ(gen_rank(Upr (v))) Upr (v) ≡ Term [r] Upo (v) ≡ true
subst_rank({Upr (v)} ∪ U , Γ) ={Upr (v), Upo (v)} ∪ subst_rank(U , Γ)We also support the synthesis of lexicographic ranking functions,details are omitted for simplicity of presentation.
5.5

Inferring Inductive Unreachability

Procedure prove_NonTerm(scc, T , Θ) finds non-termination ona scc by unreachability of its post-predicates in T . For eachUpr (v)∈scc, the method filter_rel(T , Upr ) selects a set of postassumptions Ts ⊆ T such that their RHS post-predicate is thecorresponding Upo (v). The general form of such post-assumptions
is either:
1. ρ∧true ⇒ (µ⇒Upo (v)), orVV
2. ρ∧ (ηi ⇒false) ∧ (µj ⇒Ujpo (vj )) ⇒ (µ⇒Upo (v)).
These post-assumptions capture possible non-termination of its
method due to predicate Upo (v) being unknown, under the conditionρ ∧ µ where the context ρ is satisfiable. The first post-assumption
describes a base-case scenario. In order to ensure unreachability of
its post-predicate, we must check that ρ ∧ µ is unsatisfiable. The
second post-assumption shows that we can meet a non-terminating
method call (with the postcondition false) if the condition ηi issatisfied by ρ∧µ. In addition, we can meet a (mutually) recursive
call whose termination is unknown if µj is satisfied, and thus therespective pre-predicate of Ujpo (vj ) also belongs to the analyzed
scc. We call the conditions ηi , µj and µ potential non-termination
conditions as they could lead to an actual non-termination.
By induction, we prove that a caller is definitely non-terminating
under a condition µ, assuming that one of its callee is definitely
non-terminating under the same condition. Given a set of postassumptions Ts , we prove that if each unknown post-predicate intheir LHS is false then every unknown post-predicate in their RHS
is also false. This is done by the procedure abd_inf (line 39).
− For t ≡ ρ∧true ⇒ (µ⇒Upo (v)), Upo (v) ≡ false if and only ifρ∧µ is unsatisfiable. So the proof succeeds and abd_inf(t)returns {true} if ` ρ∧µ⇒false.
V
V− For t ≡ ρ∧ (ηi ⇒false)∧ (µj ⇒Ujpo (vj ))⇒(µ⇒Upo (v)), givenjthat ∀jW· Upo (vWj ) ≡ false, we have Upo (v) ≡ false if and only ifρ∧µ⇒ ηi ∨ µj , this means that under the precondition µ, atleast one of the callees’ non-termination conditions is satisfied,so that the caller is also non-terminating.WThe W
proof succeeds
and abd_inf(t) returns {true} if ` ρ∧µ⇒ ηi ∨ µj .

If the proof succeeds for all pre-predicates in scc (signified
by r in line 40), we mark the unknown termination status asdefinitely non-terminating. This procedure thus refines, where
possible, each unknown pre-predicate as Upr (v) ≡ Loop and its
post-predicate as Upo (v) ≡ false (line 41) and updates Θ before
returning (true, Θ).
For our running example, (a01 ) and (a03 ) from T would cause
prove_NonTerm(scc, T , Θ) to return false, but provide an abductive condition y≥0 that facilitates case-splitting (see next subsection). In contrast, (a13 ) would be used to show that U2po (x, y)
is inductively false (or unreachable).
5.6

Case-Splitting

If non-termination proving fails, the method abd_inf abductively
infers new sub-conditions from the failed proof to refine the potential
non-termination condition by case-split.
In the case t ≡ ρ∧true ⇒ (µ⇒Upo (v)), if the proof fails, i.e.
0 ρ ∧ µ ⇒ false, abd_inf(t) simply returns {} as any condition thatmakes the entailment to hold would contradict with the antecedent
ρ∧µ.
V
V
j
If t ≡ ρ∧ (ηi ⇒false)∧ W(µj ⇒U
W po (vj )) ⇒ (µ⇒Upo (v)), andthe proof fails, i.e. 0 ρ∧µ⇒ ηi ∨ µj , abd_inf(t) returns a setof conditions Ct such that: for each βk ∈ {ηi }∪{µj } s.t. ρ∧µ∧βk issatisfiable, there exists αk ∈Ct such that (i) ρ∧µ∧αk is satisfiableand (ii) ` ρ∧µ∧αk ⇒βk . That is, if the potential non-termination
condition µ of the caller is strengthened by αk then the (potential)
non-termination condition βk of a callee is satisfied.
For each condition βk , the solution αk ≡ βk is a trivial but the
weakest solution for αk . For a more effective case-split, we aim toderive a stronger abductive condition αk . By the same constraintbased approach used for thePranking function synthesis, we assume the template αk ≡ c0 + n
i=1 ci vi ≥0, where v1 , .., vn ≡v andc0 , .., cn are unknown coefficients. We might solve these unknown
coefficients with additional optimal constraints, e.g. the number ofzero-coefficients is maximum, so that we can obtain a better solution
with minimum number of program variables.
Given a set of collective abductive conditions C, the procedure
subst_unk (line 42) refines the pair of (Upr (v), Upo (v)) with these
new sub-cases for the update of Θ.
split(C) = {µj }m
j=1 µm+1 = ¬µ1 ∧ . . . ∧ ¬µm
VW∆1 =(Upo (v)≡ (µj ⇒Ujpo (v))) ∆2 =(Upr (v)≡ (µj ∧Ujpr (v)))
S j
j
j
j
Ω = {Upr (v) ≡ Upr (v), Upo (v) ≡ Upo (v)}subst_unk(C, Upr (v), Upo (v)) = {∆1 , ∆2 } ∪ ΩAs the conditions in C might be overlapping, we use the function
split defined below to partition these conditions into
W the newW setof mutually exclusive conditions {µj }mC ≡ {µj }.
j=1 such that
We also add into the new set the condition µm+1 = ¬µ1 ∧. . .∧¬µm ,if it is satisfiable, to cover the missing case, so that {µj }m+1
j=1 iscomplete. Note split({}) = {}.
C2 =split(C1 ) C3 ={ci | ci ∈C2 ∧UNSAT(cV i ∧c1 )}C4 = {ci | ci ∈C2 ∧SAT(ci ∧c1 )} c = c1 ∧ {¬ci | ci ∈C4 }
C5 = {ci ∧c1 | ci ∈C4 } ∪ {ci ∧¬c1 | ci ∈C4 ∧SAT(ci ∧¬c1 )}split({c1 }∪C1 ) = if SAT(c) then {c} ∪ C3 ∪ C5 else C3 ∪ C5

6.

Experiments

We have implemented the proposed inference mechanism on topof H IP T NT [33], an existing verification system that can verify
both termination and non-termination specifications given by users.
The new inference system H IP TNT+ and this paper’s artifact areavailable for both online use and download at
http://loris-7.ddns.comp.nus.edu.sg/~project/hiptnt/plus/.

Benchmark
AProVEU LTIMATE
H IP TNT+

craftedcrafted-lit
numeric
memory-alloca
Total
Y N U T/O Time Y N U T/O Time Y N U T/O Time Y N U T/O TimeY N U T/O Time
20 0 15 4 373.1 106 0 23 21 2122.1 68 0 0 0 859.0 69 0 7 5 2475.9 263 0 45 30 5830.0
21 15 1 2 331.0 113 17 14 6 1704.1 56 0 9 3 508.8 37 6 8 30 2659.0 227 38 32 41 5202.8
19 13 7 0 35.1 115 20 15 0 114.5 66 0 2 0 35.3 67 6 8 0 123.6 267 39 32 0 308.4

Figure 10. Termination Outcomes on SV-COMP’15’s Benchmarks
Total
Y N U T/O TimeT2 (rev. 051de80) 161 30 28 2 729.0
H IP TNT+
170 30 21 0 204.3

Figure 11. Comparison on Loop-based Integer Programs
To evaluate our approach, we compare our tool against state-ofthe-art systems, i.e. T2 [7], U LTIMATE [26] and AProVE [21]. The
last tool is the recent winner for several categories of problems in
the annual Termination Competition 2014 (TermCOMP’14) [46]and the Termination category in the Competition on Software
Verification 2015 (SV-COMP’15) [45]. We made our preliminary
comparison based on a set of numerical and pointer-based C
programs selected from four benchmarks used for the Termination
category of the SV-COMP’15. These benchmarks were largely
contributed by the teams of AProVE and U LTIMATE. We haveexcluded 61 programs with arrays and strings from the total 399
programs in 4 benchmarks, since these two aspects1 have not yet
been handled by our specification inference and verification system.
In addition, we made a comparison with T2 for only 221 loopbased integer programs from the first 3 benchmarks because the tool
llvm2KITTeL [18] (which translates C programs into T2’s format)
cannot properly handle pointers and recursive methods. For AProVE
and U LTIMATE, we used their SV-COMP’15 versions, which aredescribed in [44] and [27], respectively. The experiments were
performed on an Ubuntu 12.04 machine with the AMD Opteron6172 (2.1GHz) processor and 64GB of RAM.
In Figure 10 and 11, we report the number of programs whose
main methods’ termination or non-termination were proven successfully in columns labeled by Y (for termination) or N (for nontermination), respectively. The columns U (i.e. unknown) show thenumber of programs in which the tools cannot decide whether they
are definitely terminating or non-terminating. The number of unsuccessful cases in which the tools give no answer after a timeout isprovided in the columns T/O. As in the TermCOMP’14 competition,
we set a wall-clock timeout of 300 seconds for the proving process on each program. Finally, the last column in each benchmark
presents the total time (excluding timeouts) each tool took to prove
the termination and non-termination of the whole benchmark. In
this evaluation, we only report the wall-clock time instead of theconsumed CPU time of all the verifier’s processes because CPU
time of tools executing jobs in parallel, such as AProVE, would bemuch higher otherwise. Our tool’s timing covers memory safety
analysis and post-condition inference, where required.
The overall result shows that our H IP TNT+ can efficiently(without any timeout) infer more (non-)termination properties thanthe other tools. Note that all answers (specifications inferred) thatwere returned by our tool have been successfully re-verified2 byan underlying automated verification system. Thus, our tool does
not have any false positive nor negative for this set of benchmarks.
For the other analyzers, we check their answers and found that T2
initially had five unsound outcomes which were subsequently fixed3 .
1 These are orthogonal to termination and non-termination reasoning.
2 The re-verification is optional but useful for testing whether an un-certified

program analyzer is returning sound results or not.
3 These problems have been fixed at commit 051de80 at https://github.
com/mmjb/T2 after we reported them to the developers of T2.

7.

Related Work

Over the last decade, there has been a large body of work on proving
program termination. Most of these termination provers, such as
T ERMINATOR [12] and its successor T2 [7, 16], A RMC [39], TAN[29] and U LTIMATE [26], either show that a program terminates forall (given) inputs or return a counterexample to termination upon the
failure of termination proofs. However, due to the incompletenessof termination-based techniques, these provers cannot guaranteethat every returned counterexample (from failed termination proofs)
leads to a definitely non-terminating execution. Thus, each toolmight deploy a separate non-termination proving technique to provethat the counterexample is feasible. Also, each such counterexample
is only an under-approximation of its program execution, so that it
does not capture the wider scenarios for non-terminating behaviorsof the analyzed program.
We have also seen much related work on proving program nontermination, e.g. [1, 6, 8, 24, 31, 35, 47]. Non-termination provers,
such as T NT [24] and I NVEL [47], attempt to disprove program
termination by searching for some initial configurations that act
as witnesses for non-termination. To find a wider class of nontermination bugs, these approaches attempt to discover sufficient preconditions for non-termination. Nevertheless, since non-termination
proving techniques are also incomplete, the analyzed program is
not guaranteed to terminate under the complement of the inferredpre-condition for non-termination.
The dual problem of conditional termination, first addressed in[14], identifies initial configurations that ensure termination. In [14],such termination preconditions are derived from potential ranking
functions, which are bounded but not decreasing. Later, the toolsof F LATA [4] and ACABAR [19] infer the sufficient precondition
for termination from (the negation on over-approximation of) the
set of initial states from which the program might not terminate.
However, F LATA differs from ACABAR by limiting itself to classesof loops with restricted forms in which the precise non-termination
conditions are definable.

8.

Conclusion

We have proposed a modular inference framework for program termination and non-termination. By incorporating unknown pre/postpredicates into specification logic for termination reasoning, ourproposed framework employs a Hoare-style forward verification
to collect a set of relational assumptions to help soundly discover
termination and non-termination properties. Our technique analyzes
program termination and non-termination at the same time, and constructs a summary of these behaviors for each method. This enables
better modularity and reuse for our proving processes. Furthermore,
it is integrated with a verification system allowing us to use partial
specification and to re-check our inference outcome. As seen in
the experiments over SV-COMP’15 benchmarks, our tool compares
favorably against current state-of-the-art termination analyzers.
We shall now discuss two current limitations of our tool. Firstly,
our tool handles non-deterministic inputs by identifying conditional
statements that directly depend on non-deterministic values. Each
such non-deterministic conditional is marked as non-terminating ifeither of its two branches is non-terminating. This works for mostexamples, but is less general than the proposal in [8]. Secondly,
while we support lexicographic linear ranking functions (LLRF) inour termination reasoning, we cannot handle programs that criticallydepend on Ramsey’s theorem [10, 37] or those that are based onsize-change principles [34] but do not have LLRF counterpart. It
would be interesting to explore future extensions to our specification
logic to better support non-determinism and these other kinds oftermination proofs.
Acknowledgements: We thank the reviewers for their insightful
suggestions. We are grateful to Long H. Pham, Quang-Trung Ta,
Quang Loc Le, Andreea Costea and Zhuohong Cai for their help
in preparing H IP TNT+ for the SV-COMP 2015 competition. This
work is supported by the MoE Tier-2 grant MOE2013-T2-2-146.

References[1] M. F. Atig, A. Bouajjani, M. Emmi, and A. Lal. Detecting Fair Nontermination in Multithreaded Programs. In CAV, 2012.
[2] J. Berdine, B. Cook, D. Distefano, and P. W. O’Hearn. Automatic
Termination Proofs for Programs with Shape-Shifting Heaps. In CAV,
2006.
[3] J. Berdine, A. Chawdhary, B. Cook, D. Distefano, and P. W. O’Hearn.
Variance analyses from invariance analyses. In POPL, 2007.
[4] M. Bozga, R. Iosif, and F. Konečný. Deciding Conditional Termination.
In TACAS, 2012.
[5] A. R. Bradley, Z. Manna, and H. B. Sipma. The Polyranking Principle.
In ICALP, 2005.
[6] M. Brockschmidt, T. Ströder, C. Otto, and J. Giesl. AutomatedDetection of Non-Termination and NullPointerExceptions for Java
Bytecode. In FoVeOOS, 2011.
[7] M. Brockschmidt, B. Cook, and C. Fuhs. Better termination proving
through cooperation. In CAV, 2013.
[8] H.-Y. Chen, B. Cook, C. Fuhs, K. Nimkar, and P. O’Hearn. Proving
nontermination via safety. In TACAS, 2014.
[9] W.-N. Chin, C. David, H. H. Nguyen, and S. Qin. Automatedverification of shape, size and bag properties via user-defined predicatesin separation logic. Science of Computer Programming, 77(9), 2012.
[10] M. Codish, S. Genaim, M. Bruynooghe, J. Gallagher, and W. Vanhoof.
One loop at a time. In Intl. Workshop on Termination (WST), 2003.
[11] B. Cook, A. Podelski, and A. Rybalchenko. Abstraction refinement for
termination. In SAS, 2005.
[12] B. Cook, A. Podelski, and A. Rybalchenko. Termination proofs for
systems code. In PLDI, 2006.
[13] B. Cook, A. Podelski, and A. Rybalchenko. Proving thread termination.
In PLDI, 2007.
[14] B. Cook, S. Gulwani, T. Lev-Ami, A. Rybalchenko, and M. Sagiv.
Proving conditional termination. In CAV, 2008.
[15] B. Cook, D. Kroening, P. Rümmer, and C. M. Wintersteiger. Ranking
Function Synthesis for Bit-Vector Relations. In TACAS, 2010.
[16] B. Cook, A. See, and F. Zuleger. Ramsey vs. Lexicographic Termination
Proving. In TACAS, 2013.
[17] P. Cousot. Proving Program Invariance and Termination by Parametric
Abstraction, Lagrangian Relaxation and Semidefinite Programming. In
VMCAI, 2005.
[18] S. Falke, D. Kapur, and C. Sinz. Termination Analysis of C Programs
Using Compiler Intermediate Languages. In RTA, 2011.
[19] P. Ganty and S. Genaim. Proving termination starting from the end. In
CAV, 2013.
[20] C. Gherghina, C. David, S. Qin, and W.-N. Chin. Structured specifications for better verification of heap-manipulating programs. In FM,
2011.
[21] J. Giesl, M. Brockschmidt, F. Emmes, F. Frohn, C. Fuhs, C. Otto,
M. Plücker, P. Schneider-Kamp, T. Ströder, S. Swiderski, and R. Thie-mann. Proving Termination of Programs Automatically with AProVE.
In IJCAR, 2014.
[22] S. Grebenshchikov, N. P. Lopes, C. Popeea, and A. Rybalchenko.
Synthesizing software verifiers from proof rules. In PLDI, 2012.
[23] S. Gulwani, S. Srivastava, and R. Venkatesan. Program Analysis As
Constraint Solving. In PLDI, 2008.
[24] A. Gupta, T. A. Henzinger, R. Majumdar, A. Rybalchenko, and R.-G.
Xu. Proving non-termination. In POPL, 2008.
[25] W. R. Harris, A. Lal, A. V. Nori, and S. K. Rajamani. Alternation for
Termination. In SAS, 2010.
[26] M. Heizmann, J. Hoenicke, and A. Podelski. Termination Analysis by
Learning Terminating Programs. In CAV, 2014.
[27] M. Heizmann, D. Dietsch, J. Leike, B. Musa, and A. Podelski. Ultimate
Automizer with Array Interpolation (Competition Contribution). In
TACAS, 2015.
[28] D. Jovanovic and L. M. de Moura. Solving non-linear arithmetic. In
IJCAR, 2012.
[29] D. Kroening, N. Sharygina, A. Tsitovich, and C. M. Wintersteiger.
Termination Analysis with Compositional Transition Invariants. In
CAV, 2010.
[30] D. Larraz, A. Oliveras, E. Rodriguez-Carbonell, and A. Rubio. Proving
termination of imperative programs using Max-SMT. In FMCAD,
2013.
[31] D. Larraz, K. Nimkar, A. Oliveras, E. Rodriguez-Carbonell, andA. Rubio. Proving Non-termination Using Max-SMT. In CAV, 2014.
[32] Q. L. Le, C. Gherghina, S. Qin, and W.-N. Chin. Shape Analysis via
Second-Order Bi-Abduction. In CAV, 2014.
[33] T. C. Le, C. Gherghina, A. Hobor, and W.-N. Chin. A resource-based
logic for termination and non-termination proofs. In ICFEM, 2014.
[34] C. S. Lee, N. D. Jones, and A. M. Ben-Amram. The size-change
principle for program termination. In POPL, 2001.
[35] É. Payet and F. Spoto. Experiments with Non-Termination Analysis
for Java Bytecode. Electr. Notes Theor. Comput. Sci., 253(5), 2009.
[36] C. S. Peirce. Collected papers of Charles Sanders Peirce. Harvard
University Press., 1958.
[37] A. Podelski and A. Rybalchenko. Transition Invariants. In LICS, 2004.
[38] A. Podelski and A. Rybalchenko. A Complete Method for the Synthesisof Linear Ranking Functions. In VMCAI, 2004.
[39] A. Podelski and A. Rybalchenko. ARMC: The Logical Choice forSoftware Model Checking with Abstraction Refinement. In PADL,
2007.
[40] C. Popeea and W.-N. Chin. Inferring Disjunctive Postconditions. In
ASIAN, 2006.
[41] J. Reynolds. Separation Logic: A Logic for Shared Mutable Data
Structures. In LICS, 2002.
[42] A. Rybalchenko. Constraint Solving for Program Verification: Theory
and Practice by Example. In CAV, 2010.
[43] A. Schrijver. Theory of Linear and Integer Programming. John Wiley& Sons, New York, 1986.
[44] T. Ströder, C. Aschermann, F. Frohn, J. Hensel, and J. Giesl. AProVE:
Termination and Memory Safety of C Programs (Competition Contribution). In TACAS, 2015.
[45] SV-COMP. The Competition on Software Verification. http://sv-comp.
sosy-lab.org/2015/, 2015.
The Annual International Termination Competi[46] TermCOMP.
tion. http://termination-portal.org/wiki/Termination_Competition_
2014/, 2014.
[47] H. Velroyen and P. Rümmer. Non-termination checking for imperative
programs. In TAP, 2008.