conference paper published yes Krishnendu Chatterjee author 2E5DCA20-F248-11E8-B48F-1D18A9856A870000-0002-4561-241X Ehsan Kafshdar Goharshady author Petr Novotný author 3CC3B868-F248-11E8-B48F-1D18A9856A87 Dorde Zikelic author 294AA7A6-F248-11E8-B48F-1D18A9856A870000-0002-4681-1699 KrCh department PLDI: Programming Language Design and Implementation Formal Methods for Stochastic Models: Algorithms and Applications project 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. Association for Computing Machinery2021Online eng 9781450383912 2104.01189 00072366170006710.1145/3453483.3454093 1033-1048 https://research-explorer.ista.ac.at/record/15284 https://research-explorer.ista.ac.at/record/14539 Chatterjee, Krishnendu, Ehsan Kafshdar Goharshady, Petr Novotný, and Dorde Zikelic. “Proving Non-Termination by Program Reversal.” In <i>Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation</i>, 1033–48. Association for Computing Machinery, 2021. <a href="https://doi.org/10.1145/3453483.3454093">https://doi.org/10.1145/3453483.3454093</a>. Chatterjee K, Goharshady EK, Novotný P, Zikelic D. 2021. Proving non-termination by program reversal. Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation. PLDI: Programming Language Design and Implementation, 1033–1048. Chatterjee, K., Goharshady, E. K., Novotný, P., &#38; Zikelic, D. (2021). Proving non-termination by program reversal. In <i>Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation</i> (pp. 1033–1048). Online: Association for Computing Machinery. <a href="https://doi.org/10.1145/3453483.3454093">https://doi.org/10.1145/3453483.3454093</a> K. Chatterjee, E.K. Goharshady, P. Novotný, D. Zikelic, in:, Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, Association for Computing Machinery, 2021, pp. 1033–1048. Chatterjee, Krishnendu, et al. “Proving Non-Termination by Program Reversal.” <i>Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation</i>, Association for Computing Machinery, 2021, pp. 1033–48, doi:<a href="https://doi.org/10.1145/3453483.3454093">10.1145/3453483.3454093</a>. Chatterjee K, Goharshady EK, Novotný P, Zikelic D. Proving non-termination by program reversal. In: <i>Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation</i>. Association for Computing Machinery; 2021:1033-1048. doi:<a href="https://doi.org/10.1145/3453483.3454093">10.1145/3453483.3454093</a> K. Chatterjee, E. K. Goharshady, P. Novotný, and D. Zikelic, “Proving non-termination by program reversal,” in <i>Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation</i>, Online, 2021, pp. 1033–1048. 96442021-07-11T22:01:17Z2026-04-07T13:27:55Z