Proving non-termination by program reversal

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:
Static Analysis
Program Termination
Backward Analysis
Invariant Generation
Completeness Guarantees
Programming Languages and Compilers
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

Internet

https://ink.library.smu.edu.sg/sis_research/9072
https://ink.library.smu.edu.sg/context/sis_research/article/10075/viewcontent/3453483.3454093.pdf

Similar Items