Proving Non-termination Using Max-SMT

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