Proving non-termination using max-SMT
Document typeConference report
Rights accessOpen Access
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 connected subgraphs of a program's control flow graph for analysis and thus produces more generic witnesses of non-termination than existing methods. Moreover, it can handle programs with unbounded non-determinism and is more likely to converge than previous approaches.
CitationLarraz, D. [et al.]. Proving non-termination using max-SMT. A: International Conference on Computer Aided Verification. "Computer Aided Verification : 26th International Conference CAV 2014 : held as part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18-22, 2014 : Proceedings". Vienna: Springer, 2014, p. 779-796.