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.68224
Xu, Ming; Li, Zhi-Bin

Citations by Year