Proving Non-termination by Program Reversal

Krishnendu Chatterjee, Ehsan Kafshdar Goharshady, Petr Novotný +1

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