Termination Analysis without the Tears


Determining whether a given program terminates is the quintessential undecidable problem. Algorithms for termination analysis may be classified into two groups:(1) algorithms with strong behavioral guarantees that work in limited circumstances (eg, complete synthesis of linear ranking functions for polyhedral loops), and (2) algorithms that are widely applicable, but have weak behavioral guarantees (eg, Terminator). This paper investigates the space in between: how can we design practical termination analyzers with useful behavioral guarantees?

In Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation