that actually terminate. Termination provers are also typically unable to find or check non-linear termination arguments (x2, for example) when they are required. Some preliminary efforts in this direction have been made, 1, 6 but these techniques are weak. To improve the current power of termination provers, further developments in non-linear reasoning are required.

Concurrency. Concurrency adds an extra layer of difficulty when attempting to prove program termination. The problem here is that we must consider all possible interactions between concurrently executing threads. This is especially true for modern fine-grained concurrent algorithms, in which threads interact in subtle ways through dynamically allocated data structures. Rather than attempting to explicitly consider all possible interleavings of the threads (which does not scale to large programs) the usual method for proving concurrent programs correct is based on rely-guarantee or assume-guarantee style of reasoning, which considers every thread in isolation under assumptions on its environment and thus avoids reasoning about thread interactions directly. Much of the power of a rely-guarantee proof system (such as Jones22 and Misra and Chandy28) comes from the cyclic proof rules, where we can assume a property of the second thread while proving property of the first thread, and then assume the recently proved property of the first thread when proving the assumed property of the second thread. This strategy can be extended to liveness properties using induction over time, for example, Gotsman et al. 20 and McMillan. 27

As an example, consider the two code fragments in Figure 10. Imagine that we are executing these two fragments concurrently. To prove the termination of the left thread we must prove that it does not get stuck waiting for the call to lock. To prove this we can assume the other thread will always eventually release the lock—but to prove this of the code on the right we must assume the analogous property of the thread on the left, and so on. In this case we can certainly just consider all possible interleavings of the threads, thus turning the concurrent program into a sequential model

With fresh
advances in
methods for
proving the
termination
of sequential
programs that
operate over
mathematical
numbers, we are
now in the position
to begin proving
termination of
more complex
programs.

representing its executions, but this approach does not scale well to larger programs. The challenge is to develop automatic methods of finding non-cir-cular rely-guarantee termination arguments. Recent steps20 have developed heuristics that work for non-blocking algorithms, but more general techniques are still required.

Advanced programming features. The industrial adoption of high-level programming features such as virtual functions, inheritance, higher-order functions, or closures make the task of proving industrial programs more of a challenge. With few exceptions (such as Giesl et al. 18), this area has not been well studied.

Untyped or dynamically typed programs also contribute difficulty when proving termination, as current approaches are based on statically discovering data-structure invariants and finding arithmetic measures in order to prove termination. Data in untyped programs is often encoded in strings, using pattern matching to marshal data in and out of strings. Termination proving tools for JavaScript would be especially welcome, given the havoc that nonterminating JavaScript causes daily for Web browsers.

Finding preconditions that guarantee termination. In the case that a program does not guarantee termination from all initial configurations, we may want to automatically discover the conditions under which the program does guarantee termination. That is, when calling some function provided by a library: what are the conditions under which the code is guaranteed to return with a result? The challenge in this area is to find the right precondition: the empty precondition is correct but useless, whereas the weakest precondition for even very simple programs can often be expressed only in complex domains not supported by today’s tools. Furthermore, they should be computed quickly (the weakest precondition expressible in the target logic may be too expensive to compute). Recent work has shown some preliminary progress in this direction. 13, 33

Liveness. We have alluded to the connection between liveness properties and the program termination problem. Formally, liveness properties expressed in temporal logics can