Proving non-termination by program reversal

• المؤلفون الرئيسيون: CHATTERJEE, Krishnendu, GOHARSHADY, Ehsan Kafshdar, NOVOTNÝ, Petr, ZIKELIC, Dorde
• التنسيق: text
• اللغة: English
• منشور في: Institutional Knowledge at Singapore Management University 2021
• الموضوعات: Static Analysis; Program Termination; Backward Analysis; Invariant Generation; Completeness Guarantees; Programming Languages and Compilers
• الوصول للمادة أونلاين: https://ink.library.smu.edu.sg/sis_research/9072; https://ink.library.smu.edu.sg/context/sis_research/article/10075/viewcontent/3453483.3454093.pdf
• المؤسسة: Singapore Management University

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