Symbolic termination analysis of solvable loops

ISCAS OpenIR

	Symbolic termination analysis of solvable loops
	Xu, Ming; Li, Zhi-Bin
	2013
发表期刊	JOURNAL OF SYMBOLIC COMPUTATION
ISSN	0747-7171
卷号	50 页码:28-49
摘要	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
关键词	Program Verification Termination Analysis Polynomial Loops Symbolic Computation Quantifier Elimination Real Root Bounds
部门归属	[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.
语种	英语
WOS记录号	WOS:000312574000002
引用统计	被引频次：8[WOS] [WOS记录] [WOS相关记录]
内容类型	期刊论文
URI标识	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.