Eventual Linear Ranking Functions

Roberto Bagnara

BUGSENG (http://bugseng.com) Dipartimento di Matematica e Informatica

Università di Parma, Italy

bagnara@cs.unipr.it Fred Mesnard

LIM Université de la Réunion, France

frederic.mesnard@univ-reunion.fr

ABSTRACT

Program termination is a hot research topic in program analysis. The last few years have witnessed the development of termination analyzers for programming languages such as C and Java with remarkable precision and performance. These systems are largely based on techniques and tools coming from the field of declarative constraint programming. In this paper, we first recall an algorithm based on Farkas’ Lemma for discovering linear ranking functions proving termination of a certain class of loops. Then we propose an extension of this method for showing the existence of eventual linear ranking functions, i.e., linear functions that become ranking functions after a finite unrolling of the loop. We show correctness and completeness of this algorithm.

Keywords

termination analysis, ranking function, eventual linear ranking function.

1. INTRODUCTION

Program termination is a hot research topic in program analysis. The last few years have witnessed the development of termination analyzers for mainstream programming languages such as C [16] and Java [1, 21, 24] with remarkable precision and performance. These systems are largely based on techniques and tools coming from the field of declarative constraint programming.

Beyond the specificities of the targeted programming languages and after several abstractions (see, e.g., [24]), termination analysis of entire programs boils down to termination analysis of individual loops. Various categories of loops have been identified: for the purposes of this paper we focus on single-path linear constraint (SLC) loops [9].

We first recall some notions and notations. For n ∈ ℕ, we denote by ℚ^{n} the n-dimensional vector space on the field of rational numbers ℚ.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(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. PPDP ’13, September 16 – 18 2013, Madrid, Spain Copyright is held by the owner/author(s). Publication rights licensed to ACM. Copyright 2013 ACM 978-1-4503-2154-9/13/09 ...$15.00

http://dx.doi.org/10.1145/2505879.2505884 .

A vector v ∈ ℚ^{n} can be also interpreted as a matrix in ℚ^{n×1} and manipulated accordingly using the usual definitions for addition, multiplication (both by a scalar and by another matrix), and transposition, denoted by v^{T}. For each i = 1, … n, v_{i} denotes the i-th component of the (column) vector v = (v_{1}, …, v_{n})^{T} ∈ ℚ^{n}. The scalar product of v, w ∈ ℚ^{n}, denoted ⟨v, w⟩, is the rational number

v^{T}w = ∑_{i=1}^{n} v_{i}w_{i}.

Now, an SLC loop over n variables x_{1}, …, x_{n} has the form

while (B x ≤ b) do A (\begin{matrix}x \\ x′ \end{matrix}) ≤ c

where x = (x_{1}, …, x_{n})^{T} and x′ = (x′_{1}, …, x′_{n})^{T} are column vectors of variables, B ∈ ℤ^{p×n} is an integer matrix, b ∈ ℤ^{p}, A ∈ ℤ^{q×2n} and c ∈ ℤ^{q}. Such a loop can be conveniently written as a constraint logic programming rule:

p(x) ← Bx ≤ b, A (\begin{matrix}x \\ x′ \end{matrix}) ≤ c, p(x′).

When variables take their values in ℤ (resp., ℚ), we call such loops integer (resp., rational) loops. They model a computation that starts from a point x; if B x ≤ b is false, the loop terminates; otherwise, a new point x′ is chosen that satisfies

A (\begin{matrix}x \\ x′ \end{matrix}) ≤ c

and iteration continues replacing the values of x by the corresponding ones of x′.

Loop termination can always be ensured by a ranking function ρ, a function from ℤ^{n} or ℚ^{n} to a well-founded set. As the range of ρ is well-founded, the computation terminates. To the best of our knowledge, decidability of universal termination of SLC loops (i.e., from any starting point and for any choice of the next point at each iteration) is an open question. Some sub-classes have been shown to be decidable [12, 15, 25]. For instance, Braverman proves that termination of loops where the body is a deterministic assignment x′ := Ax is decidable when the variables range over ℚ. The problem is open for the non-deterministic case, as stated in his paper. On the other hand, various generalizations have been shown to be undecidable [11].

A way to investigate loop termination is to restrict the class of the considered ranking functions. In the following section, we recall a well-known technique for computing linear ranking functions for rational SLC loops.

In Section 3 we present the main contribution of the paper, namely the definition of eventual linear ranking functions: these are linear functions that become ranking functions after a finite unrolling of the loop.^{1} We shall see that the number of unrolling is not pre-defined, but depends on the data processed by the loop. Section 3 presents complete decision procedures for the existence of eventual linear ranking functions of SLC loops. The presentation is gradual and illustrates the algorithms by means of constraint logic programming (CLP) technology and dialogues with real CLP tools. Section 4 discusses related work and a preliminary experimentation conducted on the benchmarks proposed in two very recent papers. Section 5 concludes the paper.

2. LINEAR RANKING FUNCTIONS

We first define the notion of linear (resp., affine) ranking function for an SLC loop.

Definition 2.1. Let C be the SLC loop

p(x) ← c(x, x′), p(x′)

where p is an n-ary relation symbol. A linear (resp., affine) ranking function ρ for C is a linear (resp., affine) map from ℚ^{n} to ℚ such that

∀x, x′ : c(x, x′) ⟹ ρ(x) ≥ 1 + ρ(x′) ∧ ρ(x) ≥ 0.

In words, the continuation of the iteration, i.e., c(x, x′), entails that ρ stays positive and strictly decreases by at least 1 for each iteration. We point out that if c(x, x′) is not satisfiable, the loop ends immediately and any linear function is a ranking function. In the paper, we assume that c(x, x′) is satisfiable.

Remark 2.2. Definition 2.1 might seem too restrictive when working with rational numbers as one might prefer to replace the decrease by 1 by a decrease by ε, a fixed positive quantity. Actually, by multiplying such an ε-decrease ranking function by 1/ε, we see that the two definitions are equivalent with respect to the existence of a ranking function.

Remark 2.3. Although the class of affine ranking functions subsumes the class of linear ranking functions, any decision procedure for the existence of linear ranking functions can be extended to a decision procedure for the existence of affine ranking functions. To see this, note that an affine ranking function for

p(x) ← c(x, x′), p(x′)

is a linear ranking function for

p(x, y) ← c(x, x′), y = 1, y′ = 1, p(x′, y′),

where y is distinct from the variables in x.

In this section, we focus on linear ranking functions for SLC loops. After the presentation of a formulation of Farkas’ Lemma we consider the problem of verifying linear ranking functions, and then the detection of such ranking functions.

1A preliminary version of this work, in French, was presented in [2].

2.1 Farkas’ Lemma

A linear inequation I over rational numbers is a logical consequence of a finite satisfiable conjunction S of linear inequations when I is a linear positive combination of the inequations of S. More formally, let S be

\{ \begin{matrix}a_{1,1}x_{1} & + & ⋯ & + & a_{1,n}x_{n} & + & b_{1} & ≥ & 0 \\ ⋯ & + & ⋯ & + & ⋯ & + & ⋯ & ≥ & 0 \\ a_{m,1}x_{1} & + & ⋯ & + & a_{m,n}x_{n} & + & b_{m} & ≥ & 0. \end{matrix}

and suppose that S has at least one solution. Farkas’ Lemma states the equivalence of

∀x_{1}, …, x_{n} : S ⟹ (c_{1}x_{1} + ⋯ + c_{n}x_{n} + d ≥ 0)

and

∃λ_{1} ≥ 0, …, λ_{m} ≥ 0 .

(d ≥ ∑_{i=1}^{m} λ_{i}b_{i}) ∧ ⋀_{j=1}^{n}(c_{j} = ∑_{i=1}^{m} λ_{i}a_{i,j}).

2.2 Verification

Given an SLC loop C and a linear function ρ, we can easily check whether ρ is a ranking function for C by testing the unsatisfiability of

c(x, x′) ∧ ρ(x) < 1 + ρ(x′)

or

c(x, x′) ∧ ρ(x) < 0.

This test has polynomial complexity and can be done with a complete rational solver such as , e.g., CLP(ℚ) [20].

Example 2.4. For the SLC loop C:

p(x, y) ← x ≥ 0, y′ ≤ y − 1, x′ ≤ x + y, y ≤ −1, p(x′, y′)

the linear function ρ(x, y) = x is a ranking function, as proved by the following SICStus Prolog session.

                                                        ?- use_module(library(clpq)).
                                                        % library(clpq) compiled
                                                        true.
                                                        ?- {X >= 0, Y1 =< Y - 1, X1 =< X + Y, Y =< -1,
                                                            X < 1 + X1}.
                                                        false.
                                                        ?- {X >= 0, Y1 =< Y - 1, X1 =< X + Y, Y =< -1,
                                                            X < 0}.
                                                        false.
                                                        ?-

2.3 Detection

Given an SLC loop, we would like to know whether it admits a linear ranking function ρ. This problem, which has been studied in depth [5, 6, 22, 23], is decidable in polynomial time.

Let us consider Example 2.4 and formally ask whether there exists a ranking function of the form ρ(x, y) = ax+by:

∃a, b . ∀x, y, x′, y′ : \{ \begin{matrix}x & ≥ 0, & x′ & ≤ x + y, \\ y & ≤ −1, & y′ & ≤ y − 1 \end{matrix}\}

⟹ \{ \begin{matrix}ax + by & ≥ 1 + ax′ + by′, \\ ax + by & ≥ 0. \end{matrix} (1)

This formulation of the problem is executable by quantifier elimination on a symbolic computation system like Reduce [19]:

1: load_package redlog;
2: rlset r;
3: F:=ex({a,b},all({x,y,x1,y1},
  (x>=0 and y1<=y-1 and x1<=x+y and y<= -1)
  impl
  (a*x+b*y>=1+a*x1+b*y1 and a*x+b*y>=0)));
4: rlqe F;

Statement 1 loads the quantifier elimination module. Statement 2 defines ℝ as the domain of discourse. Statement 3 initializes formula F. Statement 4 runs quantifier elimination over F and returns an equivalent formula, true in this case. Hence, formula F is true and there exists at least one linear ranking function. We can now determine the coefficients of function ρ as follows:

5: G:=all({x,y,x1,y1},
  (x>=0 and y1<=y-1 and x1<=x+y and y<= -1)
  impl
  (a*x+b*y>=1+a*x1+b*y1 and a*x+b*y>=0));
6: rlqe G;

We obtain

a^{2} − ab ≥ 0 ∧ a − b ≠ 0 ∧ a > 0 ∧ b = 0

∧ (a^{2}b − ab^{2} ≤ 0 ∨ a^{2} − ab = 0 ∨ a^{2} − 2ab − a + b^{2} + b ≥ 0)

∧ (a^{2} − ab = 0 ∨ a^{2} − 2ab − a + b^{2}b ≥ 0),

and all values for a and b satisfying the above formula, such as a = 1 and b = 0, are equally good. Unfortunately, the complexity of the algorithms involved will prevent us from systematically obtaining such a result within acceptable time and memory bounds.

We now recall the most famous algorithm for this problem [22].^{2} Considering a and b as parameters of the problem, we can apply Farkas’ Lemma. For the strict decrease of the ranking function we have

∀x, y, x′, y′ : \{ \begin{matrix}x & ≥ 0, & x′ & ≤ x + y, \\ y & ≤ −1, & y′ & ≤ y − 1 \end{matrix}\}

⟹ ax + by ≥ 1 + ax′ + by′. (2)

Application of Farkas’ Lemma to this problem can be depicted as follows:

λ_{1} : 1x + 0y + 0x′ + 0y′ + 0 ≥ 0
λ_{2} : 1x + 1y − 1x′ + 0y′ + 0 ≥ 0
λ_{3} : 0x + 1y + 0x′ − 1y′ − 1 ≥ 0
λ_{4} : 0x − 1y + 0x′ + 0y′ − 1 ≥ 0

⟹

ax + by − ax′ − by′ − 1 ≥ 0

We know that formula (2) is equivalent to the existence of four non-negative rational numbers λ_{1}, …, λ_{4} such that:

\{ \begin{matrix}a & = λ_{1} + λ_{2}, & −a & = −λ_{2}, \\ b & = λ_{2} + λ_{3} − λ_{4}, & −b & = −λ_{3}, & −1 & ≥ −λ_{3} − λ_{4}. \end{matrix}

(3)

2See also [5, 6].

The positivity of the ranking function, that is,

∀x, y, x′, y′ : \{ \begin{matrix}x & ≥ 0 & x′ & ≤ x + y \\ y & ≤ −1 & y′ & ≤ y − 1 \end{matrix}\}

⟹ ax + by ≥ 0 (4)

can be written as

λ′_{1} : 1x + 0y + 0x′ + 0y′ + 0 ≥ 0
λ′_{2} : 1x + 1y − 1x′ + 0y′ + 0 ≥ 0
λ′_{3} : 0x + 1y + 0x′ − 1y′ − 1 ≥ 0
λ′_{4} : 0x − 1y + 0x′ + 0y′ − 1 ≥ 0

⟹

ax + by + 0x′ + 0y′ + 0 ≥ 0.

By Farkas’ Lemma, formula (4) is equivalent to the existence of four other non-negative rational numbers λ′_{1}, …, λ′_{4} such that:

\{ \begin{matrix}a & = λ′_{1} + λ′_{2}, & 0 & = −λ′_{2}, \\ b & = λ′_{2} + λ′_{3} − λ′_{4}, & 0 & = −λ′_{3}, \\ & & 0 & ≥ −λ′_{3} − λ′_{4}. \end{matrix}  (5)

Summarizing, by Farkas Lemma, formula (1) is equivalent to the conjunction of formulas (3) and (5):

∃a, b . ∃λ_{1}, …, λ_{4}, λ′_{1}, …, λ′_{4} ≥ 0 .

\{ \begin{matrix}a & = λ_{1} + λ_{2}, & −a & = −λ_{2}, \\ b & = λ_{2} + λ_{3} − λ_{4}, & −b & = −λ_{3}, \\ a & = λ′_{1} + λ′_{2}, & 0 & = −λ′_{2}, \\ b & = λ′_{2} + λ′_{3} − λ′_{4}, & 0 & = −λ′_{3}, \\ −1 & ≥ −λ_{3} − λ_{4}, & 0 & ≥ −λ′_{3} − λ′_{4}. \end{matrix} (6)

In theory, the problem of the existence of a linear ranking function is polynomial. Since computing one solution (that is, values for a and b) is not harder than determining its existence, a “witness” function, which would constitute a termination certificate, can also be computed in polynomial time.

The space of all linear ranking functions as defined in Definition 2.1, described by parameters a and b, can be obtained by elimination of λ_{i} and λ′_{i} from (6) using, e.g., the algorithm of Fourier-Motzkin. For example the SICStus Prolog program

                                                        fm(A, B) :-
                                                           {L1 >= 0, L2 >= 0, L3 >= 0, L4 >= 0,
                                                            LP1 >= 0, LP2 >= 0, LP3 >= 0, LP4 >= 0,
                                                            A = L1 + L2, B = L2 + L3 - L4,
                                                            A = L2, B = L3, 1 =< L3 + L4,
                                                            A = LP1 + LP2, B = LP2 + LP3 - LP4,
                                                            0 = LP2, 0 = LP3, 0 =< LP3 + LP4}.

can be queried as follows:

                                                        | ?- fm(A, B).
                                                        B = 0, {A >= 1}.
                                                        | ?-

It can be shown that the computed answer is equivalent to the (significantly more involved) condition generated by Reduce.

3. EVENTUAL LINEAR RANKING FUNC-TIONS

In the previous section we have illustrated a method to decide the existence of a linear ranking function for a rational SLC loop, something that implies termination of the loop. Of course, the method cannot decide termination in all cases.

Example 3.1. The loop

p(x, y) ← x ≥ 0, y′ ≤ y − 1, x′ ≤ x + y, p(x′, y′)

does not admit a linear ranking function.

Can we conclude that such loop does not always terminate? No, because it may admit a non-linear ranking function.

In this section we will extend the previous method so as to detect eventual linear ranking functions, that is, linear functions that behave as ranking functions after a finite number of executions of the loop body. Suppose that the considered SLC loop is always given with a linear function f(x, y) that increases at each iteration of the loop in the following sense:

Definition 3.2. Let C be the SLC loop

p(x) ← c(x, x′), p(x′).

A function f(x) is increasing for C if it is linear and satisfies: ∀x, x′ : c(x, x′) ⟹ f(x′) ≥ 1 + f(x).

Example 3.3. Since y decreases by at least 1 at each iteration, the function f(x, y) = −y is increasing for the loop of Example 3.1.

Remark 3.4. The generalization to affine functions is useless. Moreover, as we are merely interested in the existence of an increasing function, the value of the increase (1 or ε > 0) is irrelevant.

We can now give the definition which is central to our paper.

Definition 3.5. Let C be the rational SLC loop in clausal form

p(x) ← c(x, x′), p(x′),

where p is an n-ary relation; let also f(x) be a linear increasing function for C. An eventual linear ranking function ρ for (C, f) is a linear map of ℚ^{n} to ℚ such that

∃k . ∀x, x′ : (c(x, x′) ∧ f(x) ≥ k)

⟹ (ρ(x) ≥ 1 + ρ(x′) ∧ ρ(x) ≥ 0).

For comparison with Definition 2.1, remark that the threshold k is existentially quantified and that f(x) ≥ k is imposed in the implication antecedent. It should also be noted that, if such a rational k exists, then each k′ ≥ k satisfies the condition of Definition 3.5. On the other hand, since, by hypothesis, f strictly increases at each iteration, there are two cases: either f is bounded from above by a constant, and thus the loop will terminate; or, after a finite number of iterations, f will cross the threshold k and ρ becomes a linear ranking function in the sense of Section 2 so that, again, the loop terminates.

Eventual linear ranking functions are a generalization of linear ranking functions.

Proposition 3.6. Let C be an SLC loop. If ρ is a linear ranking function for C, then there exists an increasing function f such that (C, f) has an eventual linear ranking function.

Proof. By hypothesis, there exists a linear ranking function ρ(x) for C. The linear function f(x) =^{def} −ρ(x) is nonpositive and strictly increasing for C. Considering k = 1 it can be seen that the function ρ′(x) =^{def} 0 is an eventual linear ranking function for (C, f).

The generalization is strict as the loop of Example 3.1 has no linear ranking function, but does have an eventual linear ranking function, as will be shown in the next section.

3.1 Detection given a Linear Increasing Func-

tion

As a first step towards full automation of the synthesis of eventual linear ranking functions, we assume that an SLC loop is given with a particular linear increasing function. Let us consider, e.g., the SLC loop of Example 3.1 and the increasing function of Example 3.3. Defining ρ(x, y) = ax + by, ρ is an eventual linear ranking function when

∃a, b, k . ∀x, y, x′, y′ : \{ \begin{matrix}x & ≥ 0, & x′ & ≤ x + y, \\ −y & ≥ k, & y′ & ≤ y − 1 \end{matrix}\}

⟹ \{ \begin{matrix}ax + by & ≥ 1 + ax′ + by′, \\ ax + by & ≥ 0. \end{matrix}

This definition of the problem, that we will denote for brevity with ∃a, b, k . ϕ(a, b, k), is also solvable via quantifier elimination, hence the problem is decidable. Considering a, b and k as parameters, we can apply Farkas’ Lemma as follows:

λ_{1} : 1x + 0y + 0x′ + 0y′ + 0 ≥ 0
λ_{2} : 1x + 1y − 1x′ + 0y′ + 0 ≥ 0
λ_{3} : 0x + 1y + 0x′ − 1y′ − 1 ≥ 0
λ_{4} : 0x − 1y + 0x′ + 0y′ − k ≥ 0

⟹

ax + by − ax′ − by′ − 1 ≥ 0
ax + by  ≥ 0.

Hence, formula ϕ(a, b, k) is equivalent to the conjunction of formulas DEC(a, b, k), i.e.,

∃λ_{1} ≥ 0, …, λ_{4} ≥ 0 .
\{ \begin{matrix}a & = λ_{1} + λ_{2}, & −a & = −λ_{2}, \\ b & = λ_{2} + λ_{3} − λ_{4}, & −b & = −λ_{3}, & −1 & ≥ −λ_{3} − kλ_{4}, \end{matrix}

ensuring the decreasing of the ranking function, and the formula POS(a, b, k), that is,

∃λ′_{1} ≥ 0, …, λ′_{4} ≥ 0 .
\{ \begin{matrix}a & = λ′_{1} + λ′_{2}, & 0 & = −λ′_{2} \\ b & = λ′_{2} + λ′_{3} − λ′_{4}, & 0 & = −λ′_{3} & 0 & ≥ −λ′_{3} − kλ′_{4}, \end{matrix}

ensuring the positivity of the ranking function.

Let us focus on DEC(a, b, k). We observe that the product kλ_{4} leads to a non-linearity that we can circumvent by noting that, as λ_{4} ≥ 0, either λ_{4} = 0 (hence kλ_{4} = 0) or λ_{4} > 0. In the latter case, we introduce a new variable P = kλ_{4}. We have the property:

Lemma 3.7. Formula ∃k . DEC(a, b, k) is equivalent to the disjunction DEC_{1}(a, b) ∨ DEC_{2}(a, b).

In our case, DEC_{1}(a, b) is equivalent to

∃λ_{1}, λ_{2}, λ_{3} ≥ 0 .
\{ \begin{matrix}a & = λ_{1} + λ_{2}, & −a & = −λ_{2}, \\ b & = λ_{2} + λ_{3}, & −b & = −λ_{3}, & −1 & ≥ −λ_{3}, \end{matrix}

and DEC_{2}(a, b) is equivalent to

∃λ_{1} ≥ 0, λ_{2} ≥ 0, λ_{3} ≥ 0, λ_{4} > 0, P .
\{ \begin{matrix}a & = λ_{1} + λ_{2}, & −a & = −λ_{2}, \\ b & = λ_{2} + λ_{3} − λ_{4}, & −b & = −λ_{3}, & −1 & ≥ −λ_{3} − P. \end{matrix}

Proof. (⟹) Let k be a rational number and λ_{i}’s for 1 ≤ i ≤ 4 four non-negative rational numbers such that DEC(a, b, k) holds. If λ_{4} = 0 then DEC(a, b, k) simplifies to DEC_{1}(a, b) which is true. If λ_{4} > 0, we take P = kλ_{4} and we can see that DEC_{2}(a, b) is true. (⟸) Assume first that DEC_{1}(a, b) is true. Then, taking λ_{4} = 0 and k = 0 (any rational number would be fine for k), we see that ∃k . DEC(a, b, k) is true. Assume then that DEC_{2}(a, b) is true. Taking k = P/λ_{4} (this is always possible as λ_{4} > 0), we observe that there exists k such that DEC(a, b, k) is true.

For the positivity condition, we can prove in a similar way

Lemma 3.8. Formula ∃k . POS(a, b, k) is equivalent to the disjunction POS_{1}(a, b) ∨ POS_{2}(a, b).

In our case, POS_{1}(a, b) is equivalent to

∃λ′_{1}, λ′_{2}, λ′_{3} ≥ 0 .
\{ \begin{matrix}a & = λ′_{1} + λ′_{2}, & 0 & = −λ′_{2}, \\ b & = λ′_{2} + λ′_{3}, & 0 & = −λ′_{3}, & 0 & ≥ −λ′_{3}, \end{matrix}

and POS_{2}(a, b) to

∃λ′_{1}, λ′_{2}, λ′_{3} ≥ 0, λ′_{4} > 0, P′ .
\{ \begin{matrix}a & = λ′_{1} + λ′_{2}, & 0 & = −λ′_{2}, \\ b & = λ′_{2} + λ′_{3} − λ′_{4}, & 0 & = −λ′_{3}, & 0 & ≥ −λ′_{3} − P′. \end{matrix}

Combining the previous results gives

Proposition 3.9. Formula ∃k.ϕ(a, b, k) is equivalent to [DEC_{1}(a, b) ∨ DEC_{2}(a, b)] ∧ [POS_{1}(a, b) ∨ POS_{2}(a, b)].

Proof. Thanks to the previous lemmata, it only remains to justify the equivalence between the formulas ∃k . ϕ(a, b, k) and ∃k . DEC(a, b, k) ∧ ∃k . POS(a, b, k).

(⟹) Let k_{0} be a rational such that ϕ(a, b, k_{0}). We have DEC(a, b, k_{0}) and POS(a, b, k_{0}) because

ϕ(a, b, k) ⟺ DEC(a, b, k) ∧ POS(a, b, k).

(⟸) Assume the existence of k_{d} such that DEC(a, b, k_{d}) and the existence of k_{p} such that POS(a, b, k_{p}). Then the rational k_{0} = max(k_{d}, k_{p}) verifies DEC(a, b, k_{0})∧POS(a, b, k_{0}) and shows that ∃k . ϕ(a, b, k).

Back to our initial problem, the existence of an eventual linear ranking function is equivalent to the satisfiability of at least one of the following four linear systems:

DEC_{1}(a, b) ∧ POS_{1}(a, b),
DEC_{1}(a, b) ∧ POS_{2}(a, b),
DEC_{2}(a, b) ∧ POS_{1}(a, b),
DEC_{2}(a, b) ∧ POS_{2}(a, b),

which we can decide in polynomial time. For our running example, DEC_{2}(a, b) ∧ POS_{1}(a, b) is satisfiable as proved by the following SICStus Prolog query:

                                                        ?- dec2pos1.
                                                        true.
                                                        ?-

after compilation of the program:

                                                        dec2pos1 :-
                                                           {L1 >= 0, L2 >= 0, L3 >= 0, L4 > 0,
                                                            A = L1 + L2, B = L2 + L3 - L4,
                                                            A = L2, B = L3, 1 =< L3 + P,
                                                            LP1 >= 0, LP2 >= 0, LP3 >= 0,
                                                            A = LP1 + LP2, B = LP2 + LP3,
                                                            0 = LP2, 0 = LP3, 0 =< LP3}.

The procedure we have informally outlined by means of examples is actually completely general. It is embodied in Algorithm 1, which is a (correct and complete) decision procedure for the existence of an eventual linear ranking function given a linear increasing function.

Algorithm 1 Existence of an eventual linear ranking function, given a linear increasing function Require: C, an SLC loop p(x) ← c(x, x′), p(x′), and f, a

linear increasing function for C Ensure: Returns true if and only if, for some vector a, ρ(x) = ⟨a, x⟩ is an eventual linear ranking function for (C, f).

1: DEC(a, k) := Farkas for the decreasing of ρ 2: DEC_{1}(a), DEC_{2}(a) := linearization of DEC(a, k) 3: POS(a, k) := Farkas for the positivity of ρ 4: POS_{1}(a), POS_{2}(a) := linearization of POS(a, k) 5: if ⋁_{1≤i,j≤2} DEC_{i}(a) ∧ POS_{j}(a) is satisfiable then 6: return true 7: else 8: return false 9: end if

Theorem 3.10. Let C be an SLC loop and f an increasing function for C. Algorithm 1 decides in polynomial time the existence of an eventual linear ranking function for (C, f).

Computing an eventual linear ranking function ρ and its associated threshold k can be done as follows:

• if DEC_{1}(a) ∧ POS_{1}(a) is satisfiable, we compute a solution a, ρ(x) = ⟨a, x⟩ is a standard linear ranking function and Proposition 3.6 applies;

• if DEC_{1}(a) ∧ POS_{2}(a) is satisfiable, we compute a solution a, λ′, P′ and we take k = P′/λ′_{n};

• if DEC_{2}(a) ∧ POS_{1}(a) is satisfiable, we compute a solution a, λ, P and we take k = P/λ_{n}; • if DEC_{2}(a)∧POS_{2}(a) is satisfiable, we compute a solu-

tion a, λ, P, λ′, P′ and we take k = max(P/λ_{n}, P′/λ′_{n}).

Example 3.11. Continuing with Example 3.1, here is the most general solution of DEC_{2}(a, b) ∧ POS_{1}(a, b):

?-  {L1 >= 0, L2>= 0, L3 >= 0, L4 > 0,
     A = L1 + L2, B = L2 + L3 - L4,
     A = L2, B = L3, 1 =< L3 + P,
     LP1 >= 0, LP2 >= 0, LP3 >= 0,
     A = LP1 + LP2, B = LP2 + LP3,
     0 = LP2, 0 = LP3, 0 =< LP3}.
B = 0, L1 = 0, L3 = 0, LP2 = 0, LP3 = 0,
{LP1 = L4, L2 = L4, A = L4, L4 > 0, P >= 1}.
?-

One particular solution is b = 0 = λ_{1} = λ_{3} = λ′_{2} = λ′_{3}, a = 1 = λ′_{1} = λ_{2} = λ_{4}, P = 1. Hence ρ(x, y) = x is an eventual linear ranking function from the threshold k = P/λ_{4} = 1.

We also provide a decision procedure for the existence of an eventual affine ranking function.

Corollary 3.12. The existence of an eventual affine ranking function for an SLC loop and associated increasing function, (C, f), can be decided in polynomial time.

Proof. From C, p(x) ← c(x, x′), p(x′), we construct C_{a}, p(x, y) ← c(x, x′), y = 1, y′ = 1, p(x′, y′), where y does not occur in x. Note that C_{a} is an SLC loop and that f_{a}(x, y) = f(x) is an increasing function for C_{a}. Algorithm 1 applied to (C_{a}, f_{a}) gives an answer in polynomial time.

If Algorithm 1 returns true then, by correctness, there exists a threshold k and an eventual linear function ρ_{a}(x, y) = ⟨a, x⟩+by for (C_{a}, f_{a}). We readily check that ρ(x) = ⟨a, x⟩+ b is an eventual affine ranking function for (C, f) from k.

If Algorithm 1 returns false then, by completeness, there is no eventual linear ranking function for (C_{a}, f_{a}). Assuming there exists an eventual affine ranking function ρ(x) = ⟨a, x⟩+b from k for (C, f), then ρ_{a}(x, y) = ⟨a, x⟩+by should be an eventual linear ranking function from k for (C_{a}, f_{a}), which is a contradiction. Hence there is no eventual affine ranking function for (C, f).

Example 3.13. The SLC loop

p(x, y) ← x ≥ −1, y′ ≤ y − 1, x′ ≤ x + y, p(x′, y′)

associated to the linear increasing function f(x, y) = −y does not admit an eventual linear ranking function, but does admit ρ(x, y) = x + 1 as an eventual affine ranking function from k = 1.

3.2 Fully Automated Detection

We now consider the problem in its full generality: given an SLC loop C, does there exist an increasing function for C such that C admits an eventual linear ranking function?

Note that the space of increasing functions can be obtained as a convex set over their coefficients via the Farkas’ Lemma and existentially quantified variables elimination.^{3}

Definition 3.14. Let C = (p(x) ← c(x, x′), p(x′)) be an SLC loop. We denote by INC the set of vectors b such that f(x) = ⟨b, x⟩ is increasing for C.

3See also [6, Section 4.4].

Example 3.15. A linear ranking function does not exist for the SLC loop C

p(x, y) ← x ≥ 0, x′ ≤ x + y, y′ ≤ −y − 1, p(x′, y′).

INC = { (b_{1}, b_{2}) ∈ ℚ × ℚ | b_{1} ≤ −2, b_{1} − 2b_{2} = 0 } induces the space of functions of the form f(x, y) = b_{1}x + b_{2}y, which are increasing for C.

Let us consider the SLC loop of Example 3.15 associated to an increasing function f(x, y) = b_{1}x + b_{2}y induced by INC. Defining ρ(x, y) = a_{1}x + a_{2}y and considering b_{1} and b_{2} as parameters, ρ is an eventual linear ranking function when

∃a_{1}, a_{2}, k . ∀x, y, x′, y′ : \{ \begin{matrix}x & ≥ 0, & x′ ≤ x + y, \\ b_{1}x + b_{2}y & ≥ k, & y′ ≤ −y − 1 \end{matrix}\}

⟹ \{ \begin{matrix}a_{1}x + a_{2}y & ≥ 1 + a_{1}x′ + a_{2}y′, \\ a_{1}x + a_{2}y & ≥ 0. \end{matrix}

This definition of the problem is denoted ∃a, k . ϕ(a, k). We can apply Farkas’ Lemma as follows:

λ_{1} : 1x + 0y + 0x′ + 0y′ + 0 ≥ 0
λ_{2} : 1x + 1y − 1x′ + 0y′ + 0 ≥ 0
λ_{3} : 0x − 1y + 0x′ − 1y′ − 1 ≥ 0
λ : b_{1}x + b_{2}y + 0x′ + 0y′ − k ≥ 0

⟹

a_{1}x + a_{2}y − a_{1}x′ − a_{2}y′ − 1 ≥ 0
a_{1}x + a_{2}y  ≥ 0.

Formula ϕ(a, k) is equivalent to the conjunction of formulas DEC(a, k), i.e.,

∃λ_{1} ≥ 0, λ_{2} ≥ 0, λ_{3} ≥ 0, λ ≥ 0 .
\{ \begin{matrix}a_{1} & = λ_{1} + λ_{2} + b_{1}λ & −a_{1} & = −λ_{2}, \\ a_{2} & = λ_{2} − λ_{3} + b_{2}λ, & −a_{2} & = −λ_{3}, & −1 & ≥ −λ_{3} − kλ, \end{matrix}

ensuring the decreasing of the ranking function and POS(a, k), that is,

∃λ′_{1} ≥ 0, λ′_{2} ≥ 0, λ′_{3} ≥ 0, λ′ ≥ 0 .
\{ \begin{matrix}a_{1} & = λ′_{1} + λ′_{2} + b_{1}λ′ & 0 & = −λ′_{2} \\ a_{2} & = λ′_{2} − λ′_{3} + b_{2}λ′, & 0 & = −λ′_{3} & 0 & ≥ −λ′_{3} − kλ′, \end{matrix}

ensuring the positivity of the ranking function.

Let us focus on DEC(a, k). We observe that the products with λ lead to a non-linearity that we can circumvent by noting that, as λ ≥ 0, either λ = 0 or λ > 0. In the latter case, we introduce a vector p = (p_{1}, p_{2}) of two new variables where p_{1} = b_{1}λ and p_{2} = b_{2}λ together with, as previously, the new variable P = kλ. Formula ∃k . DEC(a, k) is equivalent to the disjunction DEC_{1}(a)∨∃λ, p.DEC_{2}(a, λ, p) where in our case, DEC_{1}(a) is equivalent to

∃λ_{1} ≥ 0, λ_{2} ≥ 0, λ_{3} ≥ 0 .
\{ \begin{matrix}a_{1} & = λ_{1} + λ_{2}, & −a_{1} & = −λ_{2}, \\ a_{2} & = λ_{2} − λ_{3}, & −a_{2} & = −λ_{3}, & −1 & ≥ −λ_{3}, \end{matrix}

and DEC_{2}(a, λ, p) is equivalent to

∃λ_{1} ≥ 0, λ_{2} ≥ 0, λ_{3} ≥ 0, P .
\{ \begin{matrix}a_{1} & = λ_{1} + λ_{2} + p_{1}, & −a_{1} & = −λ_{2}, & λ & > 0, \\ a_{2} & = λ_{2} − λ_{3} + p_{2}, & −a_{2} & = −λ_{3}, & −1 & ≥ −λ_{3} − P. \end{matrix}

For the positivity condition, formula ∃k . POS(a, k) is equivalent to the disjunction POS_{1}(a) ∨ ∃λ′, p′.POS_{2}(a, p′) where we introduce a vector p′ = (p′_{1}, p′_{2}) of two new variables where p′_{1} = b_{1}λ′, p′_{2} = b_{2}λ′ together with, as previously, the new variable P′ = kλ′. In our case, POS_{1}(a) is equivalent to

∃λ′_{1} ≥ 0, λ′_{2} ≥ 0, λ′_{3} ≥ 0 .
\{ \begin{matrix}a_{1} & = λ′_{1} + λ′_{2}, & 0 & = −λ′_{2}, \\ a_{2} & = λ′_{2} − λ′_{3}, & 0 & = −λ′_{3}, & 0 & ≥ −λ′_{3}, \end{matrix}

and POS_{2}(a, λ′, p′) to

∃λ′_{1} ≥ 0, λ′_{2} ≥ 0, λ′_{3} ≥ 0, P′ .
\{ \begin{matrix}a_{1} & = λ′_{1} + λ′_{2} + p′_{1}, & 0 & = −λ′_{2}, & λ′ & > 0, \\ a_{2} & = λ′_{2} − λ′_{3} + p′_{2}, & 0 & = −λ′_{3}, & 0 & ≥ −λ′_{3} − P′. \end{matrix}

Back to our initial problem, the existence of an eventual linear ranking function is equivalent to the satisfiability of at least one of the following four systems:

1. DEC_{1}(a) ∧ POS_{1}(a): this case means that the increasing function and k are irrelevant. In other words, for each solution a, ρ(x) = ⟨a, x⟩ is a standard linear ranking function and Proposition 3.6 applies.

2. DEC_{1}(a) ∧ POS_{2}(a, λ′, p′) ∧ p′/λ′ ∈ INC: note that satisfiability of DEC_{1}(a) ∧ POS_{2}(a, λ′, p′) is not sufficient, as its solution might lead to the coefficients b_{1} = p′_{1}/λ′ and b_{2} = p′_{2}/λ′ (λ′ is strictly positive by definition), which could correspond to a non-increasing linear function. The third conjunct, p′/λ′ ∈ INC, ensures that we stay within the space of increasing functions.

3. DEC_{2}(a, λ, p) ∧ p/λ ∈ INC ∧ POS_{1}(a): this case is symmetric to previous one.

4. DEC_{2}(a, λ, p) ∧ p/λ ∈ INC ∧ POS_{2}(a, λ′, p′) ∧ p/λ = p′/λ′: this case combines the two previous ones. Note that the condition ensures that we consider the same linear ranking function and the same increasing function both in DEC_{2} and in POS_{2}.

For our running example, the following SICStus Prolog query proves that DEC_{2}(a, λ, p) ∧ p/λ ∈ INC ∧ POS_{1}(a) is satisfiable

?- dec2incpos1.
true.
?-

after compilation of the program

dec2incpos1 :-
{% DEC2:
L1 >= 0, L2 >= 0, L3 >= 0,
A1 = L1 + L2 + P1, A1 = L2, L > 0,
A2 = L2 - L3 + P2, A2 = L3, -1 >= -L3 - P,

    % INC: B1 =< -2, B1 - 2*B2 = 0
    P1 =< -2*L, P1 - 2*P2 = 0,
    % POS1:
    LP1 >= 0, LP2 >= 0, LP3 >= 0,
    A1 = LP1 + LP2, 0 = LP2,
    A2 = LP2 - LP3, 0 = LP3, 0 >= -LP3}.

The procedure we have informally outlined by means of examples is actually completely general and is embodied in Algorithm 2.

Algorithm 2 Existence of an eventual linear ranking function Require: C, an SLC loop p(x) ← c(x, x′), p(x′) Ensure: Returns true if and only if there exists an increas-

ing function f for C and ρ(x) = ⟨a, x⟩ such that ρ is an eventual linear ranking function for (C, f).

1: INC := the space of increasing functions for C

2: DEC(a, k) := Farkas for the decreasing of ρ 3: DEC_{1}(a), DEC_{2}(a, λ, p) := linearization of DEC(a, k) 4: POS(a, k) := Farkas for the positivity of ρ 5: POS_{1}(a), POS_{2}(a, λ′, p′) := linearization of POS(a, k) 6: ϕ_{1,1} := DEC_{1}(a) ∧ POS_{1}(a) 7: ϕ_{1,2} := DEC_{1}(a) ∧ POS_{2}(a, λ′, p′) ∧ p′/λ′ ∈ INC 8: ϕ_{2,1} := DEC_{2}(a, λ, p) ∧ p/λ ∈ INC ∧ POS_{1}(a) 9: ϕ_{2,2} := DEC_{2}(a, λ, p) ∧ p/λ ∈ INC ∧ POS_{2}(a, λ′, p′) ∧

p/λ = p′/λ′ 10: if ⋁_{1≤i,j≤2} ϕ_{i,j} is satisfiable then 11: return true 12: else 13: return false 14: end if

Theorem 3.16. Let C be an SLC loop. Algorithm 2 decides the existence of an increasing function f and a linear function ρ such that ρ is an eventual linear ranking function for (C, f).

Exactly as in the previous section, if Algorithm 2 returns true then we can extract an increasing function f, a threshold k, and a linear function ρ. We can also generalize the approach to the fully automated detection of eventual affine ranking functions.

With respect to complexity, Algorithm 2 is not polynomial for two reasons. In step 1, computing the set INC of linear increasing functions for C requires elimination of existentially quantified variables. In step 2, formula ϕ_{2,2} leads to a non-linear system and we may have to check its satisfiability in step 10. Although decidable, we are not aware of the existence of polynomial algorithms for these problems.

3.3 Verification

Given C an SLC loop, an associated increasing function f, and a linear function ρ, we want to know whether ρ is a ranking function. We can run Algorithm 1, with the coefficients a fully instantiated. If needed, we can compute the threshold k as explained in Section 3.1. It follows that the verification problem is polynomial.

3.4 Implementation

We have implemented both algorithms in SICStus Prolog. However, as ϕ_{2,2} of Algorithm 2 leads to a non-linear system, we relaxed this formula to

DEC_{2}(a, λ, p) ∧ p/λ ∈ INC ∧ POS_{2}(a, λ′, p′) ∧ p′/λ′ ∈ INC,

which is now linear. As shown in the following proposition, the existence of an eventual linear ranking function (hence termination) is preserved, but the associated increasing function is not linear.

Proposition 3.17. Let C be an SLC loop and assume the truth of

DEC_{2}(a, λ, p) ∧ p/λ ∈ INC ∧ POS_{2}(a, λ′, p′) ∧ p′/λ′ ∈ INC.

Then there exists a non-linear increasing function f such that ρ(x) = ⟨a, x⟩ is an eventual linear ranking function for (C,f).

Proof. As DEC_{2}(a, λ, p) ∧ p/λ ∈ INC is true, there exists an increasing function f_{d} and a rational k_{d} such that when the value of f_{d} is beyond k_{d}, ρ decreases. Similarly, as POS_{2}(a, λ′, p′)∧p′/λ′ ∈ INC is true, there exists an increasing function f_{p} and a rational k_{p} such that when the value of f_{p} is beyond k_{p}, ρ is non-negative. Let k = max(k_{p}, k_{d}) and f(x) = min(f_{p}(x), f_{d}(x)). One readily checks that f is a non-linear increasing function for C and ρ is an eventual linear ranking function for (C, f).

4. RELATED WORK AND EXPERIMENTS

As eventual linear ranking functions generalize linear ranking functions, we focus on related work that goes beyond linear ranking functions for SLC loops. In order to appreciate the relative power of the different methods, we report on the results obtained with our algorithms on the loops discussed in the papers where the other approaches were introduced.

The method proposed in [27] repeatedly divides the state space to find a linear ranking function on each subspace, and then checks that the transitive closure of the transition relation is included in the union of the ranking relations. As the process may not terminate, one needs to bound the search.

[27] also proposes a test suite, upon which we tested our approach. Our implementation analyzes the complete test suite in less than 2 seconds on a standard desktop computer. As expected, every loop [27, Table 1] which terminates with a linear ranking also has an eventual linear ranking. Moreover, loops 6, 12, 13, 18, 21, 23, 24, 26, 27, 28, 31, 32, 35, and 36 admit an eventual linear ranking function (which is discovered without using neither ϕ_{2,2} nor its relaxation). These are all shown terminating with the tool of [27]. On the other hand, loops 14, 34, and 38 do have a disjunctive ranking function (following the terminology of [27]), but do not admit an eventual linear ranking function.

[17] shows how to partition the loop relation into behaviors that terminate and behaviors to be analyzed in a subsequent termination proof after refinement. This work addresses both termination and conditional termination problems in the same framework. Concerning the benchmarks proposed in [17, Table 1], loops 6–41 all have an eventually linear ranking function except for loops 11, 14, 30, 34, and 38.

A method based on abstract interpretation for synthesizing ranking functions is described in [26]. Although the work contains no completeness result, the approach is able to discover piecewise-defined ranking functions.

Finally, let us point out that the concept of eventual termination appeared first in [13, 14]. The class loops studied in these works is wider but, as the technique of [14] relies on finite differences, this approach is incomplete. On the other hand, while [13] is also based on Farkas’ Lemma, it seems [A. R. Bradley, Personal communication, May 2013] that the polyranking approach cannot prove, e.g., termination of the SLC loop p(x, y) ← x ≥ 1, x′ = y, y′ = y − 1, p(x′, y′), which admits an eventual linear ranking function.

5. CONCLUSION AND FUTURE WORK

We have proposed a definition of eventual linear ranking function for SLC loops that strictly generalizes the concept of linear ranking function. We also defined two correct and complete algorithms for detecting such ranking functions under different hypotheses. The first algorithm shows that the mere knowledge of the right increasing function allows checking the existence or even synthesizing an eventual linear ranking function in polynomial time. The second algorithm decides the existence of an eventual linear ranking function in its full generality but is not polynomial. We have also explained how to extend the algorithms for deciding eventual affine ranking functions. The algorithms admit a simple formulation as a constraint logic program and have been fully implemented in SICStus Prolog inside the Bin-Term termination prover [24].

We plan to incorporate the algorithms in the Parma Polyhedra Library [4] and then in the ECLAIR static analyzer for C, C^{++} and Java programs.^{4} This will enable us to conduct an extensive experimental evaluation on real programs. Moreover, as ECLAIR already includes linearization of floating-point constraints [8] as well as other sophisticated reasoning techniques over floating-point numbers (such as, e.g., [3]), the way is paved to explore a very interesting direction for future work: synthesis of eventual linear ranking functions for loops controlled by floating-point quantities. It has to be noted that a nice property of the notion of eventual (not necessarily linear) ranking function is its simplicity. This is important when functions that witness termination have to be provided (and/or understood) by humans. This is the case when annotating a C/ACSL program with loop variants [7]: for the cases when a ranking function to be specified in a loop variant clause is not obvious, one could extend ACSL with a loop prevariant clause that allows the annotator to indicate a candidate increasing function. In the linear case, our first algorithm can efficiently decide whether the two clauses constitute a termination witness. On the other hand, there obviously are, as indicated in Section 4, more complex classes of ranking functions and algorithms that allow to establish the termination of SLC loops that do not admit an eventual linear ranking functions. A proper assessment of the relative merits of these approaches, all extremely recent, requires an extensive experimental evaluation that, as mentioned already, is one of the main objectives for future work.

The verification of linear ranking functions for integer SLC loops, that is to say, checking the satisfiability of

c(x, x′) ∧ ρ(x) < 1 + ρ(x′)

and

c(x, x′) ∧ ρ(x) < 0,

                                                        4http://bugseng.com/products/eclair

is an NP-complete problem. Concerning the existence of linear ranking functions, as the Farkas’ Lemma is not true for the integers, the method presented in Section 2 is not valid. The problem, which has been solved very recently in [10], is coNP-complete, and the paper proposes an exponential-time algorithm. Extending the present approach to integer SLC loops is another interesting idea to consider for future work.

Acknowledgments.

We are grateful to Anthony Alezan, Aaron R. Bradley, Étienne Payet, and some anonymous referees for their helpful comments.

6. REFERENCES

[1] E. Albert, P. Arenas, S. Genaim, M. Gómez-Zamalloa, G. Puebla, D. V. Ramírez, G. Román, and D. Zanardini. Termination and cost analysis with COSTA and its user interfaces. Electronic Notes in Theoretical Computer Science, 258(1):109–121, 2009.

[2] A. Alezan, R. Bagnara, F. Mesnard, and E. Payet. Détection des fonctions de rang linéaires à terme. In Actes des NeuviÃĺmes JournÃľes Francophones de Programmation par Contraintes (JFPC 2013), pages 11–20, Aix-en-Provence, France, 2013. In French.

[3] R. Bagnara, M. Carlier, R. Gori, and A. Gotlieb. Symbolic path-oriented test data generation for floating-point programs. In Proceedings of the 6th IEEE International Conference on Software Testing, Verification and Validation, Luxembourg City, Luxembourg, 2013. IEEE Press.

[4] R. Bagnara, P. M. Hill, and E. Zaffanella. The Parma Polyhedra Library: Toward a complete set of numerical abstractions for the analysis and verification of hardware and software systems. Science of Computer Programming, 72(1–2):3–21, 2008.

[5] R. Bagnara, F. Mesnard, A. Pescetti, and E. Zaffanella. The automatic synthesis of linear ranking functions: The complete unabridged version.

Report arXiv:cs.PL/1004.0944v2, 2012. Available at
http://arxiv.org/ and
http://bugseng.com/products/ppl/.

[6] R. Bagnara, F. Mesnard, A. Pescetti, and E. Zaffanella. A new look at the automatic synthesis of linear ranking functions. Information and Computation, 215:47–67, 2012.

[7] P. Baudin, P. Cuoq, J.-C. Filliâtre, C. Marché, B. Monate, Y. Moy, and V. Prevosto. ACSL: ANSI/ISO C Specification Language. CEA LIST and INRIA, 1.7 edition, 2013.

[8] M. S. Belaid, C. Michel, and M. Rueher. Boosting local consistency algorithms over floating-point numbers. In M. Milano, editor, Proceedings of the 18th International Conference on Principles and Practice of Constraint Programming, volume 7514 of Lecture Notes in Computer Science, pages 127–140, Québec City, Canada, 2012. Springer-Verlag, Berlin.

[9] A. M. Ben-Amram and S. Genaim. On the linear ranking problem for integer linear-constraint loops. Technical Report arXiv:1208.4041v2 [cs.PL], 2013.

Available from http://arxiv.org/.

[10] A. M. Ben-Amram and S. Genaim. On the linear ranking problem for integer linear-constraint loops. In R. Giacobazzi and R. Cousot, editors, Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’13), pages 51–62, Rome, Italy, 2013. Association for Computing Machinery.

[11] A. M. Ben-Amram, S. Genaim, and A. N. Masud. On the termination of integer loops. ACM Transactions on Programming Languages and Systems, 34(4):16:1–16:24, 2012.

[12] M. Bozga, R. Iosif, and F. Konecný. Deciding conditional termination. In C. Flanagan and B. König, editors, Tools and Algorithms for the Construction and Analysis of Systems: Proceedings of the 18th International Conference (TACAS 2012), volume 7214 of Lecture Notes in Computer Science, pages 252–266, Tallinn, Estonia, 2012. Springer.

[13] A. R. Bradley, Z. Manna, and H. B. Sipma. The polyranking principle. In L. Caires, G. F. Italiano, L. Monteiro, C. Palamidessi, and M. Yung, editors, Automata, Languages and Programming: Proceedings of the 32nd International Colloquium (ICALP 2005), volume 3580 of Lecture Notes in Computer Science, pages 1349–1361, Lisbon, Portugal, 2005. Springer.

[14] A. R. Bradley, Z. Manna, and H. B. Sipma.

Termination of polynomial programs. In R. Cousot, editor, Verification, Model Checking and Abstract Interpretation: Proceedings of the 6th International Conference (VMCAI 2005), volume 3385 of Lecture Notes in Computer Science, pages 113–129, Paris, France, 2005. Springer-Verlag, Berlin.

[15] M. Braverman. Termination of integer linear programs. In T. Ball and R. B. Jones, editors, Computer Aided Verification: Proceedings of the 18th International Conference (CAV 2006), volume 4144 of Lecture Notes in Computer Science, pages 372–385, Seattle, WA, USA, 2006. Springer.

[16] B. Cook, A. Podelski, and A. Rybalchenko.

Termination proofs for systems code. In M. I. Schwartzbach and T. Ball, editors, Proceedings of the ACM SIGPLAN 2006 Conference on Programming Language Design and Implementation, pages 415–426, Ottawa, Ontario, Canada, 2006. Association for Computing Machinery.

[17] P. Ganty and S. Genaim. Proving termination starting from the end. Technical Report arXiv:abs/1302.4539, 2013. Preprint version [18].

[18] P. Ganty and S. Genaim. Proving termination starting from the end. In N. Sharygina and H. Veith, editors, Computer Aided Verification: Proceedings of the 25th International Conference (CAV 2013), volume 8044 of Lecture Notes in Computer Science, pages 397–412, Saint Petersburg, Russia, 2013. Springer.

[19] A. C. Hearn. REDUCE: the first forty years. In A. Dolzmann, A. Seidl, and T. Sturm, editors, Algorithmic Algebra and Logic: Proceedings of the A3L 2005 Conference in Honor of the 60th Birthday of Volker Weispfenning, pages 19–24, Passau, Germany, 2005.

[20] C. Holzbaur. OFAI clp(Q,R). Austrian Research Institute for Artificial Intelligence, Vienna, 1.3.3 edition, 1995. Published as TR-95-09.

[21] C. Otto, M. Brockschmidt, C. von Essen, and J. Giesl.

Automated termination analysis of Java bytecode by term rewriting. In C. Lynch, editor, Proceedings of the 21st International Conference on Rewriting Techniques and Applications (RTA 2010), volume 6 of Leibniz International Proceedings in Informatics (LIPIcs), pages 259–276, Edinburgh, Scotland, UK, 2010. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik.

[22] A. Podelski and A. Rybalchenko. A complete method for the synthesis of linear ranking functions. In B. Steffen and G. Levi, editors, Verification, Model Checking and Abstract Interpretation: Proceedings of the 5th International Conference (VMCAI 2004), volume 2937 of Lecture Notes in Computer Science, pages 239–251, Venice, Italy, 2004. Springer.

[23] K. Sohn and A. Van Gelder. Termination detection in logic programs using argument sizes (extended abstract). In D. J. Rosenkrantz, editor, Proceedings of the Tenth ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems, pages 216–226, Denver, CO, USA, 1991. Association for Computing Machinery.

[24] F. Spoto, F. Mesnard, and É. Payet. A termination analyzer for Java bytecode based on path-length. ACM Transactions on Programming Languages and Systems, 32(3), 2010.

[25] A. Tiwari. Termination of linear programs. In R. Alur and D. Peled, editors, Computer Aided Verification: Proceedings of the 16th International Conference (CAV 2004), volume 3114 of Lecture Notes in Computer Science, pages 70–82, Boston, MA, USA, 2004. Springer.

[26] C. Urban. The abstract domain of segmented ranking functions. In F. Logozzo and M. Fahndrich, editors, Proceedings of the 20th International Symposium on Static Analysis (SAS 2013), volume 7935 of Lecture Notes in Computer Science, pages 43–62, Seattle, WA, USA, 2013. Springer.

[27] H. Yi Chen, S. Flur, and S. Mukhopadhyay.

Termination proofs for linear simple loops. In A. Miné and D. Schmidt, editors, Proceedings of the 19th International Symposium on Static Analysis (SAS 2012), volume 7460 of Lecture Notes in Computer Science, pages 422–438, Deauville, France, 2012. Springer.