D 2021

Proving non-termination by program reversal

CHATTERJEE, Krishnendu, Ehsan Kafshdar GOHARSHADY, Petr NOVOTNÝ and Djordje ŽIKELIĆ

Basic information

Original name

Proving non-termination by program reversal

Authors

CHATTERJEE, Krishnendu (356 India), Ehsan Kafshdar GOHARSHADY (364 Islamic Republic of Iran), Petr NOVOTNÝ (203 Czech Republic, guarantor, belonging to the institution) and Djordje ŽIKELIĆ (688 Serbia)

Edition

New York, NY, USA, Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), p. 1033-1048, 16 pp. 2021

Publisher

ACM

Other information

Language

English

Type of outcome

Stať ve sborníku

Field of Study

10201 Computer sciences, information science, bioinformatics

Country of publisher

United States of America

Confidentiality degree

není předmětem státního či obchodního tajemství

Publication form

electronic version available online

RIV identification code

RIV/00216224:14330/21:00119267

Organization unit

Faculty of Informatics

ISBN

978-1-4503-8391-2

DOI

http://dx.doi.org/10.1145/3453483.3454093

UT WoS

000723661700067

Keywords in English

program analysis; nontermination proving

Tags

core_A, firank_1, formela-ver

Tags

International impact, Reviewed
Změněno: 29/4/2022 08:14, RNDr. Pavel Šmerk, Ph.D.

Abstract

V originále

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.

Links

GJ19-15134Y, research and development project
Name: Verifikace a analýza pravděpodobnostních programů
Displayed: 7/11/2024 16:23