# Proving Non-termination by Program Reversal

arXiv: https://arxiv.org/abs/2104.01189 · HTML: https://mlsanity.com/paper/2104.01189/

## Key facts

- Cited by 9 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 2 Apr 2021.

## Built on by (most cited first, 9 of 9)

- [Non-Termination Proving: 100 Million LoC and Beyond](https://mlsanity.com/paper/2509.05293/) (2025)
- [SINGA-Easy: An Easy-to-Use Framework for MultiModal Analysis](https://mlsanity.com/paper/2108.02572/) (2021)
- [VisualTextRank: Unsupervised Graph-based Content Extraction for Automating Ad Text to Image Search](https://mlsanity.com/paper/2108.02725/) (2021)
- [Text is NOT Enough: Integrating Visual Impressions into Open-domain Dialogue Generation](https://mlsanity.com/paper/2109.05778/) (2021)
- [Discovering Personalized Semantics for Soft Attributes in Recommender Systems using Concept Activation Vectors](https://mlsanity.com/paper/2202.02830/) (2022)
- [Reinforced MOOCs Concept Recommendation in Heterogeneous Information Networks](https://mlsanity.com/paper/2203.11011/) (2022)
- [Explanation-Guided Fairness Testing through Genetic Algorithm](https://mlsanity.com/paper/2205.08335/) (2022)
- [Using Graph Neural Networks for Program Termination](https://mlsanity.com/paper/2207.14648/) (2022)
- [Tribe or Not? Critical Inspection of Group Differences Using TribalGram](https://mlsanity.com/paper/2303.09664/) (2023)

## Abstract (arXiv)

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.