Proving non-termination by program reversal

Kód výsledku v 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>

Výsledek na webu

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

Jazyk výsledku

angličtina

Název v původním jazyce

Proving non-termination by program reversal

Popis výsledku v původním jazyce

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.

Název v anglickém jazyce

Proving non-termination by program reversal

Popis výsledku anglicky

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.

Druh

D - Stať ve sborníku

CEP obor

—

OECD FORD obor

10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Projekt

<a href="/cs/project/GJ19-15134Y" target="_blank" >GJ19-15134Y: Verifikace a analýza pravděpodobnostních programů</a><br>

Návaznosti

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)

Rok uplatnění

2021

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název statě ve sborníku

Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)

ISBN

9781450383912

ISSN

—

e-ISSN

—

Počet stran výsledku

16

Strana od-do

1033-1048

Název nakladatele

ACM

Místo vydání

New York, NY, USA

Místo konání akce

online

Datum konání akce

1. 1. 2021

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

000723661700067