that the argument indeed represents a set of measures. In other cases, such as Lee et al. 24 or Manolios and Vroon, 26 the tool makes a one-time guess as to the termination argument and then checks it using techniques drawn from abstract interpretation.

Consider the modified program in Figure 7. The termination strategy described in Berdine et al. 3 and Podelski and Rybalchenko32 essentially builds a program like this and then applies a custom program analysis to find the following candidate termination argument:

 

(copied ≠ 1) or (oldx ≥ x + 1, oldx > 0, oldy > 0, x ≥ 0, y > 0) or (oldx ≥ x, oldy ≥ y + 1, oldx > 0, oldy > 0, x > 0, y ≥ 0)

 

for the program at line 4—meaning we could pass this complex expression to the assertion at line 4 in Figure 7 and know that the assertion cannot fail. We know this statement is true of any unrolling of the loop in the original Figure 1. What remains is to prove that each piece of the candidate argument represents a measure that decreases— here we can use rank function synthesis tools to prove that oldx > x + 1 and oldx > 0 . . . represents the measure based on x. If each piece between the ors in fact represents a measure (with the exception of copied ≠ 1 which comes from the encoding) then we have proved termination.

One difficulty with this style of termination proving is that, in the case that the program doesn’t terminate, the tools can only report “unknown,” as the techniques used inside the abstract interpretation tools have lost so much detail that it is impossible to find a non-terminating execution from the failed proof and then prove it non-terminating. The advantage when compared to other known techniques is it is much faster.

Finding arguments by refinement. Another method for discovering a termination argument is to follow the approach of Cook et al. 14 or Chawdhary et al. 9 and search for counterexamples to (possibly invalid) termination arguments and then refine them based on new ranking functions found via the counterexamples.

In recent years,
powerful new
termination tools
have emerged that
return “unknown”
infrequently enough
that they are useful
in practice.

Recall Figure 5, which encoded the invalid termination argument for the program in Figure 1, and the path leading to the failure of the assertion: is 1 → 2 → 3 → 4 → 5 → 7 → 8 → 9 → 10 → 11 → 12 → 16 → 17 → 4 → 5 → 6. Recall this path represents two phases of the program’s execution: the path to the loop, and some unrolling of the loop such that the termination condition doesn’t hold. In this case the path 4 → 5 → . . . 6 represents how we reached the second failing state from the first. This is a counterexample to the validity of the termination argument, meaning that the current termination argument does not take this path and others like it into account.

If the path can be repeated forever during the program’s execution then we have found a real counterexample. Known approaches (for example, Gupta et al. 21) can be used to try and prove this path can be repeated forever. In this case, however, we know that the path cannot be repeated forever, as y is decremented on each iteration through the path and also constrained via a conditional statement to be positive. Thus this path is a spurious counterexample to termination and can be ruled out via a refinement to the termination argument. Again, using rank function synthesis tools we can automatically find a ranking function that demonstrates the spuriousness of this path. In this case a rank function synthesis tool will find y, meaning that the reason this path cannot be repeated forever is that “y always goes down by at least one and is larger than 0.” We can then refine the current termination argument used in Figure 5:

 

x goes down by at least 1 and is larger than 0
with the larger termination argument:
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

 

We can then check the validity of this termination argument using a tool such as IMPACT on the program in Figure 6. IMPACT can prove this assertion never fails, thus proving the termination of the program in Figure 1.

further Directions

With fresh advances in methods for proving the termination of sequen-