---
_id: '9644'
abstract:
- lang: eng
  text: '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.'
acknowledgement: We thank the anonymous reviewers for their helpful comments. This
  research was partially supported by the ERCCoG 863818 (ForM-SMArt) and the Czech
  Science Foundation grant No. GJ19-15134Y.
article_processing_charge: No
arxiv: 1
author:
- first_name: Krishnendu
  full_name: Chatterjee, Krishnendu
  id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
  last_name: Chatterjee
  orcid: 0000-0002-4561-241X
- first_name: Ehsan Kafshdar
  full_name: Goharshady, Ehsan Kafshdar
  last_name: Goharshady
- first_name: Petr
  full_name: Novotný, Petr
  id: 3CC3B868-F248-11E8-B48F-1D18A9856A87
  last_name: Novotný
- first_name: Dorde
  full_name: Zikelic, Dorde
  id: 294AA7A6-F248-11E8-B48F-1D18A9856A87
  last_name: Zikelic
  orcid: 0000-0002-4681-1699
citation:
  ama: '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>'
  apa: '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>'
  chicago: 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>.
  ieee: 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.
  ista: '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.'
  mla: 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>.
  short: 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.
conference:
  end_date: 2021-06-26
  location: Online
  name: 'PLDI: Programming Language Design and Implementation'
  start_date: 2021-06-20
date_created: 2021-07-11T22:01:17Z
date_published: 2021-06-01T00:00:00Z
date_updated: 2026-04-07T13:27:55Z
day: '01'
department:
- _id: KrCh
doi: 10.1145/3453483.3454093
ec_funded: 1
external_id:
  arxiv:
  - '2104.01189'
  isi:
  - '000723661700067'
fulldoi: https://doi.org/10.1145/3453483.3454093
isi: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: https://arxiv.org/abs/2104.01189
month: '06'
oa: 1
oa_version: Preprint
page: 1033-1048
project:
- _id: 0599E47C-7A3F-11EA-A408-12923DDC885E
  call_identifier: H2020
  grant_number: '863818'
  name: 'Formal Methods for Stochastic Models: Algorithms and Applications'
publication: Proceedings of the 42nd ACM SIGPLAN International Conference on Programming
  Language Design and Implementation
publication_identifier:
  isbn:
  - '9781450383912'
publication_status: published
publisher: Association for Computing Machinery
quality_controlled: '1'
related_material:
  record:
  - id: '15284'
    relation: research_data
    status: public
  - id: '14539'
    relation: dissertation_contains
    status: public
scopus_import: '1'
status: public
title: Proving non-termination by program reversal
type: conference
user_id: 4359f0d1-fa6c-11eb-b949-802e58b17ae8
year: '2021'
...