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
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;
Conference_Titel :
Advanced Computer Theory and Engineering (ICACTE), 2010 3rd International Conference on
Conference_Location :
Chengdu
Print_ISBN :
978-1-4244-6539-2
DOI :
10.1109/ICACTE.2010.5579031