Proving Termination Starting from the End

TL;DR

This paper introduces a new modular technique for proving program termination by partitioning program behaviors based on current partial proofs, enhancing incremental reasoning and extending to conditional termination.

Contribution

It presents a novel approach that uses partial proofs to partition transition relations, enabling more effective incremental termination proofs and applicability to conditional termination.

Findings

Prototype implementation improves termination proof success rates.

Method effectively handles conditional termination scenarios.

Advances state-of-the-art in termination analysis.

Abstract

We present a novel technique for proving program termination which introduces a new dimension of modularity. Existing techniques use the program to incrementally construct a termination proof. While the proof keeps changing, the program remains the same. Our technique goes a step further. We show how to use the current partial proof to partition the transition relation into those behaviors known to be terminating from the current proof, and those whose status (terminating or not) is not known yet. This partition enables a new and unexplored dimension of incremental reasoning on the program side. In addition, we show that our approach naturally applies to conditional termination which searches for a precondition ensuring termination. We further report on a prototype implementation that advances the state-of-the-art on the grounds of termination and conditional termination.