Other formats:
BibTeX
LaTeX
RIS
@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Ý and 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, p.~1033-1048. ISBN~978-1-4503-8391-2. Available from: https://dx.doi.org/10.1145/3453483.3454093.
|