Proving non-termination by program reversal

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 b...

Full description

Saved in:
Bibliographic Details
Main Authors: CHATTERJEE, Krishnendu, GOHARSHADY, Ehsan Kafshdar, NOVOTNÝ, Petr, ZIKELIC, Dorde
Format: text
Language:English
Published: Institutional Knowledge at Singapore Management University 2021
Subjects:
Online Access:https://ink.library.smu.edu.sg/sis_research/9072
https://ink.library.smu.edu.sg/context/sis_research/article/10075/viewcontent/3453483.3454093.pdf
Tags: Add Tag
No Tags, Be the first to tag this record!
Institution: Singapore Management University
Language: English
id sg-smu-ink.sis_research-10075
record_format dspace
spelling sg-smu-ink.sis_research-100752024-08-01T15:23:36Z Proving non-termination by program reversal CHATTERJEE, Krishnendu GOHARSHADY, Ehsan Kafshdar NOVOTNÝ, Petr ZIKELIC, Dorde 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. 2021-06-01T07:00:00Z text application/pdf https://ink.library.smu.edu.sg/sis_research/9072 info:doi/10.1145/3453483.3454093 https://ink.library.smu.edu.sg/context/sis_research/article/10075/viewcontent/3453483.3454093.pdf http://creativecommons.org/licenses/by-nc-nd/4.0/ Research Collection School Of Computing and Information Systems eng Institutional Knowledge at Singapore Management University Static Analysis Program Termination Backward Analysis Invariant Generation Completeness Guarantees Programming Languages and Compilers
institution Singapore Management University
building SMU Libraries
continent Asia
country Singapore
Singapore
content_provider SMU Libraries
collection InK@SMU
language English
topic Static Analysis
Program Termination
Backward Analysis
Invariant Generation
Completeness Guarantees
Programming Languages and Compilers
spellingShingle Static Analysis
Program Termination
Backward Analysis
Invariant Generation
Completeness Guarantees
Programming Languages and Compilers
CHATTERJEE, Krishnendu
GOHARSHADY, Ehsan Kafshdar
NOVOTNÝ, Petr
ZIKELIC, Dorde
Proving non-termination by program reversal
description 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.
format text
author CHATTERJEE, Krishnendu
GOHARSHADY, Ehsan Kafshdar
NOVOTNÝ, Petr
ZIKELIC, Dorde
author_facet CHATTERJEE, Krishnendu
GOHARSHADY, Ehsan Kafshdar
NOVOTNÝ, Petr
ZIKELIC, Dorde
author_sort CHATTERJEE, Krishnendu
title Proving non-termination by program reversal
title_short Proving non-termination by program reversal
title_full Proving non-termination by program reversal
title_fullStr Proving non-termination by program reversal
title_full_unstemmed Proving non-termination by program reversal
title_sort proving non-termination by program reversal
publisher Institutional Knowledge at Singapore Management University
publishDate 2021
url https://ink.library.smu.edu.sg/sis_research/9072
https://ink.library.smu.edu.sg/context/sis_research/article/10075/viewcontent/3453483.3454093.pdf
_version_ 1814047723862622208