Institutional Repository
| Symbolic termination analysis of solvable loops | |
| Xu, Ming; Li, Zhi-Bin | |
| 2013 | |
| Source | JOURNAL OF SYMBOLIC COMPUTATION
 |
| ISSN | 0747-7171 |
| Volume | 50Pages:28-49 |
| English Abstract | 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. (C) 2012 Elsevier B.V. All rights reserved.; 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. (C) 2012 Elsevier B.V. All rights reserved. |
| Indexed Type | SCI |
| Keyword | Program Verification Termination Analysis Polynomial Loops Symbolic Computation Quantifier Elimination Real Root Bounds |
| Department | [Xu, Ming; Li, Zhi-Bin] E China Normal Univ, Dept Comp Sci & Technol, Shanghai 200241, Peoples R China. [Xu, Ming] Chinese Acad Sci, Inst Software, State Key Lab Comp Sci, Beijing 100190, Peoples R China. |
| Language | 英语 |
| WOS ID | WOS:000312574000002 |
| Citation statistics | |
| Content Type | 期刊论文 |
| URI | http://ir.iscas.ac.cn/handle/311060/16945 |
| Collection | 中国科学院软件研究所 |
| Recommended Citation GB/T 7714 | Xu, Ming,Li, Zhi-Bin. Symbolic termination analysis of solvable loops[J]. JOURNAL OF SYMBOLIC COMPUTATION,2013,50:28-49. |
| APA | Xu, Ming,&Li, Zhi-Bin.(2013).Symbolic termination analysis of solvable loops.JOURNAL OF SYMBOLIC COMPUTATION,50,28-49. |
| MLA | Xu, Ming,et al."Symbolic termination analysis of solvable loops".JOURNAL OF SYMBOLIC COMPUTATION 50(2013):28-49. |
| Files in This Item: | There are no files associated with this item. | |||||
Items in the repository are protected by copyright, with all rights reserved, unless otherwise indicated.
Edit Comment