Proving non-termination by program reversal
The result's identifiers
Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F21%3A00119267" target="_blank" >RIV/00216224:14330/21:00119267 - isvavai.cz</a>
Result on the web
<a href="http://dx.doi.org/10.1145/3453483.3454093" target="_blank" >http://dx.doi.org/10.1145/3453483.3454093</a>
DOI - Digital Object Identifier
<a href="http://dx.doi.org/10.1145/3453483.3454093" target="_blank" >10.1145/3453483.3454093</a>
Alternative languages
Result language
angličtina
Original language name
Proving non-termination by program reversal
Original language 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.
Czech name
—
Czech description
—
Classification
Type
D - Article in proceedings
CEP classification
—
OECD FORD branch
10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)
Result continuities
Project
<a href="/en/project/GJ19-15134Y" target="_blank" >GJ19-15134Y: Verification and Analysis of Probabilistic Programs</a><br>
Continuities
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)
Others
Publication year
2021
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Data specific for result type
Article name in the collection
Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)
ISBN
9781450383912
ISSN
—
e-ISSN
—
Number of pages
16
Pages from-to
1033-1048
Publisher name
ACM
Place of publication
New York, NY, USA
Event location
online
Event date
Jan 1, 2021
Type of event by nationality
WRD - Celosvětová akce
UT code for WoS article
000723661700067