Proving non-termination by program reversal

D 2021

Proving non-termination by program reversal

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

Základní údaje

Originální název

Proving non-termination by program reversal

Autoři

CHATTERJEE, Krishnendu (356 Indie), Ehsan Kafshdar GOHARSHADY (364 Írán), Petr NOVOTNÝ (203 Česká republika, garant, domácí) a Djordje ŽIKELIĆ (688 Srbsko)

Vydání

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

Nakladatel

ACM

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Spojené státy

Utajení

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

Forma vydání

elektronická verze "online"

Kód RIV

RIV/00216224:14330/21:00119267

Organizační jednotka

Fakulta informatiky

ISBN

978-1-4503-8391-2

DOI

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

UT WoS

000723661700067

Klíčová slova anglicky

program analysis; nontermination proving

Štítky

core_A, firank_1, formela-ver

Příznaky

Mezinárodní význam, Recenzováno

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

Anotace

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.

Návaznosti

GJ19-15134Y, projekt VaV

Název: Verifikace a analýza pravděpodobnostních programů

Citovat

CHATTERJEE, Krishnendu, Ehsan Kafshdar GOHARSHADY, Petr NOVOTNÝ a Djordje ŽIKELIĆ. Proving non-termination by program reversal. Online. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI). New York, NY, USA: ACM, 2021, s. 1033-1048. ISBN 978-1-4503-8391-2. Dostupné z: https://dx.doi.org/10.1145/3453483.3454093.

@inproceedings{1797364,
   author = {Chatterjee, Krishnendu and Goharshady, Ehsan Kafshdar and Novotný, Petr and Žikelić, Djordje},
   address = {New York, NY, USA},
   booktitle = {Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)},
   doi = {http://dx.doi.org/10.1145/3453483.3454093},
   keywords = {program analysis; nontermination proving},
   howpublished = {elektronická verze "online"},
   language = {eng},
   location = {New York, NY, USA},
   isbn = {978-1-4503-8391-2},
   pages = {1033-1048},
   publisher = {ACM},
   title = {Proving non-termination by program reversal},
   year = {2021}
}

TY  - JOUR
ID  - 1797364
AU  - Chatterjee, Krishnendu - Goharshady, Ehsan Kafshdar - Novotný, Petr - Žikelić, Djordje
PY  - 2021
TI  - Proving non-termination by program reversal
PB  - ACM
CY  - New York, NY, USA
SN  - 9781450383912
KW  - program analysis
KW  - nontermination proving
N2  - 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.
ER  -

CHATTERJEE, Krishnendu, Ehsan Kafshdar GOHARSHADY, Petr NOVOTNÝ a Djordje ŽIKELI$\backslash$'C. Proving non-termination by program reversal. Online. In \textit{Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)}. New York, NY, USA: ACM, 2021, s.~1033-1048. ISBN~978-1-4503-8391-2. Dostupné z: https://dx.doi.org/10.1145/3453483.3454093.

Podrobný výpis o publikaci