Proving Non-termination by Program Reversal

TL;DR

This paper introduces a simple yet efficient method for proving non-termination of non-deterministic integer programs by reversing the program's transition system and using SMT-solvers for invariant synthesis, handling complex features like non-determinism and polynomial arithmetic.

Contribution

It presents a novel approach combining program reversal and SMT-based invariant synthesis, offering stronger guarantees and handling more complex programs than previous methods.

Findings

The approach is at least as effective as state-of-the-art tools.

It can handle non-determinism and polynomial arithmetic.

Experimental results show non-trivial improvements.

Abstract

We present a new approach to proving non-termination of non-deterministic integer programs. Our technique is rather simple but efficient. It relies on a purely syntactic reversal of the program's transition system followed by a constraint-based invariant synthesis with constraints coming from both the original and the reversed transition system. The latter task is performed by a simple call to an off-the-shelf SMT-solver, which allows us to leverage the latest advances in SMT-solving. Moreover, our method offers a combination of features not present (as a whole) in previous approaches: it handles programs with non-determinism, provides relative completeness guarantees and supports programs with polynomial arithmetic. The experiments performed with our prototype tool RevTerm show that our approach, despite its simplicity and stronger theoretical guarantees, is at least on par with the state-of-the-art tools, often achieving a non-trivial improvement under a proper configuration of its parameters.