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.
All rights reserved. This work is protected by the corresponding intellectual and industrial property rights. Without prejudice to any existing legal exemptions, reproduction, distribution, public communication or transformation of this work are prohibited without permission of the copyright holder. If you wish to make any use of the work not provided for in the law, please contact: email@example.com