Symbolic termination analysis of solvable loops
文献类型：期刊论文
| 作者 | Xu, Ming ; Li, Zhi-Bin |
| 刊名 | JOURNAL OF SYMBOLIC COMPUTATION
 |
| 出版日期 | 2013 |
| 卷号 | 50页码:28-49 |
| ISSN号 | 0747-7171 |
| 关键词 | Program verification Termination analysis Polynomial loops Symbolic computation Quantifier elimination Real root bounds |
| 中文摘要 | 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. |
| 收录类别 | SCI |
| 语种 | 英语 |
| WOS记录号 | WOS:000312574000002 |
| 公开日期 | 2014-12-16 |
| 源URL | [http://ir.iscas.ac.cn/handle/311060/16945]  |
| 专题 | 软件研究所_软件所图书馆_期刊论文 |
| 推荐引用方式 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. |
入库方式： OAI收割
来源：软件研究所
浏览0
下载0
收藏0
其他版本
除非特别说明，本系统中所有内容都受版权保护，并保留所有权利。