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 :
بازگشت