TERMINATOR swMATH ID: 6692 Software Authors: Xu, Ming; Li, Zhi-Bin Description: Symbolic termination analysis of solvable loops. Termination is an essential part of program correctness. For a class of regular programs, both automatically proving termination and constructing witnesses of nontermination are significant in theoretical computer science. Many traditional theorem-proving methods for analyzing termination are based on Presburger arithmetic or linear programming, so they are valid only for restricted linear problems. On the contrary, some newly-emerged algebraic methods are suitable for polynomial problems, and are promising in deciding termination of polynomial programs. In this paper, we investigate a large class of imperative programs, called solvable loops, whose guards are general polynomials and assignments are special polynomial mappings. We then propose some sufficient criteria for proving termination and nontermination of such loops in parallel. These criteria can further be translated to the quantifier elimination problem over the reals, and hence are computable. Finally, feasible sample points in the process for inferring nontermination are eventually nonterminating inputs, which can be used to generate witnesses of nontermination. Our decision procedure uses symbolic computation and is mechanically implementable in spite of considerably high complexity. Thereby a series of strong and exact results are established in analyzing termination of loops. Homepage: http://dl.acm.org/citation.cfm?id=2400793 Keywords: program verification; termination analysis; polynomial loops; symbolic computation; quantifier elimination; real root bounds Related Software: REACH; DISCOVERER Cited in: 3 Publications Standard Articles 1 Publication describing the Software, including 1 Publication in zbMATH Year Symbolic termination analysis of solvable loops. Zbl 1253.68224Xu, Ming; Li, Zhi-Bin 2013 all top 5 Cited by 7 Authors 3 Xu, Ming 2 Li, Zhibin 1 Huang, Chengchao 1 Liu, Jiang 1 Zeng, Zhenbing 1 Zhan, Naijun 1 Zhao, Hengjun Cited in 3 Serials 1 Theoretical Computer Science 1 Journal of Symbolic Computation 1 Journal of Systems Science and Complexity Cited in 4 Fields 2 Computer science (68-XX) 1 Mathematical logic and foundations (03-XX) 1 Group theory and generalizations (20-XX) 1 Dynamical systems and ergodic theory (37-XX) Citations by Year