For decades, the best approach to attacking the decision problem (proving whether a given program will terminate in a finite amount of time) has been to use monolithic ranking functions. These are usually a combination of a conditional coupled with arithmetic functions in the natural numbers domain. Even for simple programs, however, this approach can be difficult. According to Cook et al., several alternatives exist.

We can add modularity by using disjunctive arguments, which we can further improve by using assertion statements during compile time. We can do so even if complete assertion checking during compile time is itself an undecidable problem, but falls within an easier class of difficulty than termination.

Implementation of disjunctive termination arguments can be through refinement, where it is started with a ranking function, which, if unsuccessful, we may further refine with another ranking function that has a broader (or more complex) domain, and so on. Another way is through variance analysis, meaning that we use a finite amount of ranking functions, and then use a synthesis tool to check that each ranking function is well founded. This last approach always terminates (as opposed to the refinement method), but may return “don’t know” in cases where the refinement-based method succeeds.

Cook et al. also mention future directions, such as dynamically allocated heaps and nonlinear systems (akin somehow to multi-threading systems), and liveness as opposed to static systems, to prevent crash dumps.

I strongly recommend this paper to researchers in artificial intelligence and operating systems developers; however, it is clearly written so any computer specialist or advanced undergraduate could read it.