---
res:
  bibo_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.@eng'
  bibo_authorlist:
  - foaf_Person:
      foaf_givenName: Krishnendu
      foaf_name: Chatterjee, Krishnendu
      foaf_surname: Chatterjee
      foaf_workInfoHomepage: http://www.librecat.org/personId=2E5DCA20-F248-11E8-B48F-1D18A9856A87
    orcid: 0000-0002-4561-241X
  - foaf_Person:
      foaf_givenName: Ehsan Kafshdar
      foaf_name: Goharshady, Ehsan Kafshdar
      foaf_surname: Goharshady
  - foaf_Person:
      foaf_givenName: Petr
      foaf_name: Novotný, Petr
      foaf_surname: Novotný
      foaf_workInfoHomepage: http://www.librecat.org/personId=3CC3B868-F248-11E8-B48F-1D18A9856A87
  - foaf_Person:
      foaf_givenName: Dorde
      foaf_name: Zikelic, Dorde
      foaf_surname: Zikelic
      foaf_workInfoHomepage: http://www.librecat.org/personId=294AA7A6-F248-11E8-B48F-1D18A9856A87
    orcid: 0000-0002-4681-1699
  bibo_doi: 10.1145/3453483.3454093
  dct_date: 2021^xs_gYear
  dct_identifier:
  - UT:000723661700067
  dct_isPartOf:
  - http://id.crossref.org/issn/9781450383912
  dct_language: eng
  dct_publisher: Association for Computing Machinery@
  dct_title: Proving non-termination by program reversal@
...