considering any possible unrolling of the loop. After some state has been recorded, from this point out the termination argument is checked using the recorded state and the current state. In this case the assertion can fail, meaning that the termination argument is not valid.

If we were to attempt to check this
condition in a naïve way (for example,
by simply executing the program) we
would never find a proof for all but the
most trivial of cases. Thus, assertion
checkers must be cleverly designed to
find proofs about all possible execu-
tions without actually executing all of
the paths. A plethora of recently devel-
oped techniques now make this pos-
sible. Many recent assertion checkers
are designed to produce a path to a bug
in the case that the assertion statement
cannot be proved. For example, a path
leading to the assertion failure is 1 →
2 → 3 → 4 → 5 → 7 → 8 → 9 → 10 →
11→ 12 → 16 → 17 → 4 → 5 → 6. This
path can be broken into parts, each
representing different phases of the ex-
ecution: the prefix-path 1 → 2 → 3 →
4 is the path from the program initial
state to the recorded state in the failing
pair of states. The second part of the
path 4 → 5 → . . . 5 → 6 represents how
we reached the current state from the
recorded one. That is: this is the unroll-
ing found that demonstrates that the
assertion statement can fail. What we
know is that the termination argument
does not currently cover the case where
this path is repeated forever.

x goes down by at least 1 and is larger than 0

or

y goes down by at least 1 and is larger than 0.

figure 7. Program prepared for abstract interpretation.

This assertion cannot fail. The fact that it cannot fail can be proved by a number of assertion verification tools.

 

1

2

3

4

5

6

7

8

9

10

11

12

13

14

15

16

17

18

copied := 0;
x := input();
y := input();
while x > 0 and y > 0 do
if copied = 1 then
skip;
elsif input() = 1 then
copied := 1;
oldx := x;
oldy := y;
fi
if input() = 1 then
x := x – 1;
y := y + 1;
else
y := y – 1;
fi
done

figure 8. example C loop over a linked-list data-structure with fields next and data.

c = head;
while (c != NULL) {
}
c = c–>next;

figure 9. example program illustrating nontermination.

1

2

3

4

x := 10;
while x > 9 do
x := x – 232;
done
example program demonstrating nontermination when variables range over fixed-width numbers. The
program terminates if x ranges over arbitrary size integers, but repeatedly visits the state where x =
10 in the case that x ranges over 32-bit unsigned numbers.

finding termination arguments

We have examined how we can check a termination argument’s validity via a translation to a program with an assertion statement. We now discuss known methods for finding monolithic termination arguments.

Rank function synthesis. In some cases simple ranking functions can be automatically found. We call a ranking function simple if it can be defined by a linear arithmetic expression (for example, −3x = −2y + 100). The most popular approach for finding this class of ranking function uses a result from Farkas16 together with tools for solving linear constraint systems. (See Colón and Sipma11 or Polel-ski and Rybalchecko30 for examples of tools using Farkas’ lemma.) Many other approaches for finding ranking functions for different classes of programs have been proposed (see refs1, 6− 8, 19, 37). Tools for the synthesis of ranking functions are sometimes applied directly to programs, but more frequently they are used (on small and simplified program fragments) internally within termination proving tools for suggesting the single ranking functions that appear in a disjunctive termination argument.

Termination analysis. Numerous approaches have been developed for finding disjunctive termination arguments in which—in effect—the validity condition for disjunctive termination arguments is almost guaranteed to hold by construction. In some cases—for example, Berdine et al. 3—to prove termination we need only check