Termination Analysis

Termination analysis answers the question of whether a program terminates, or whether there are any possible infinite loops in the program. This is the most famous undecidable problem, so the analysis cannot always be successful: in some cases, the analysis will mark a terminating program as possibly nonterminating.

The aim is to have an analysis that is as precise as possible, so that any infinite loops reported by the analysis point to real bugs in the program.

Size-Change Termination

Size-change termination is a simple framework for termination proofs, which is nonetheless very effective on natural programs. The SCT criterion handles copied or permuted arguments, mutual recursion and generalises lexicographic orders for termination.

An SCT-based termination analysis proceeds by generating size-change graphs along each function call, to record the effect of the call on values. There is then an algorithm for checking whether some flow of control in the program could be nonterminating. Despite its high complexity (PSPACE-complete), this performs well in practice.

Higher-Order Programs

My work on termination is concerned with analysing higher-order programs. The challenge is that the SCT method requires the construction of a call graph for the program. This is straightforward in the first-order case, but constructing a precise call graph for a higher-order program is much more complex. Simple strategies are ineffective: many programs are found to be nonterminating because of the imprecision of the call graph.

I have evaluated three call graph construction strategies: a context-insensitive call graph (0CFA), a variation on Shivers' k-CFA to record environment structures (k-bounded CFA) and a novel analysis based on the representation of environments as tree automata. I have shown precise relationships between classes of programs found as terminating by each of these analyses.

A question of great interest is the relationship between termination analysis and other means of guaranteeing termination, in particular simple types. It turns out that for the SCT analysis (with any of these call graphs), there are simply-typed lambda expressions which are not found to be terminating; of course there are many programs that are not simply-typed that are found to terminate. The precise relationship between typing disciplines and static analysis for termination is very much an open question.

References

• Damien Sereni, Termination Analysis and Call Graph Construction for Higher-Order Functional Programs (ICFP 2007)
• Damien Sereni and Neil D. Jones, Termination Analysis of Higher-Order Functional Programs (APLAS 2005)
• My thesis