Termination Analysis Without the Tears

TL;DR

This paper introduces ComPACT, a practical termination analysis tool that is compositional and monotone, extending graph path-solving methods to analyze infinite paths and offering stronger behavioral guarantees than existing tools.

Contribution

It extends Tarjan's method for path problems to infinite paths and develops monotone conditional termination analyses, enabling more reliable termination analysis.

Findings

ComPACT is competitive with state-of-the-art tools.

Provides stronger behavioral guarantees.

Effective analysis of infinite paths.

Abstract

Determining whether a given program terminates is the quintessential undecidable problem. Algorithms for termination analysis are divided into two groups: (1) algorithms with strong behavioral guarantees that work in limited circumstances (e.g., complete synthesis of linear ranking functions for polyhedral loops [Podelski and Rybalchenko, 2004]), and (2) algorithms that are widely applicable, but have weak behavioral guarantees (e.g., Terminator [Cook et al., 2006]). This paper investigates the space in between: how can we design practical termination analyzers with useful behavioral guarantees? This paper presents a termination analysis that is both compositional (the result of analyzing a composite program is a function of the analysis results of its components) and monotone ("more information into the analysis yields more information out"). The paper has two key contributions. The first is an extension of Tarjan's method for solving path problems in graphs to solve infinite path problems. This provides a foundation upon which to build compositional termination analyses. The second is a collection of monotone conditional termination analyses based on this framework. We demonstrate that our tool ComPACT (Compositional and Predictable Analysis for Conditional Termination) is competitive with state-of-the-art termination tools while providing stronger behavioral guarantees.