DocumentCode
2215827
Title
Termination of programs over the union of intervals
Author
Mu, Lin ; Li, Yi ; Jin, Taige ; Luo, Jiawei
Author_Institution
Lab. for Automated Reasoning & Programming, CAS, Chengdu, China
Volume
1
fYear
2010
fDate
20-22 Aug. 2010
Abstract
For a generic loop: while (constraints) {updates} it is well known that the termination problem is undecidable in general, even for a simple class of polynomial programs. If the constraints or the updating function in the above loop is not linear, the loop is called nonlinear. In this paper, we investigate how to solve the termination of the above loop by deciding whether a fixed point exists, when the constraints are the union of intervals and the updating functions are polynomials. Furthermore, when all fixed points are on the boundaries of the union of intervals, we also establish a corresponding necessary and sufficient condition of nontermination.
Keywords
constraint handling; nonlinear programming; polynomials; program control structures; program verification; generic loop; nonlinear loop; polynomial program; program termination; union of intervals; updating function; Orbits; Fixed point; Nonlinear Program; Program Verification; Termination Analysis;
fLanguage
English
Publisher
ieee
Conference_Titel
Advanced Computer Theory and Engineering (ICACTE), 2010 3rd International Conference on
Conference_Location
Chengdu
ISSN
2154-7491
Print_ISBN
978-1-4244-6539-2
Type
conf
DOI
10.1109/ICACTE.2010.5579031
Filename
5579031
Link To Document