Proving Non-termination Using Max-SMT?

Abstract. We show how Max-SMT-based invariant generation can be exploited for proving non-termination of programs. The construction of the proof of non-termination is guided by the generation of quasi-invariants – properties such that if they hold at a location during execution once, then they will continue to hold at that location from then onwards. The check that quasi-invariants can indeed be reached is then performed separately. Our technique considers strongly con-nected subgraphs of a program’s control flow graph for analysis and thus pro-duces more generic witnesses of non-termination than existing methods. More-over, it can handle programs with unbounded non-determinism and is more likely to converge than previous approaches.