Title :
Decidability analysis on termination set of loop programs
Author :
Zhao, Shizhong ; Chen, Donghuo
Author_Institution :
Shanghai Key Lab. of Trustworthy Comput., East China Normal Univ., Shanghai, China
Abstract :
For half a century, computer programs have been widely applied in all areas of industry and daily life. Given any program, whether it can terminate has direct impact on software safety. Many researchers have been working on the termination of programs. One definition of termination is as follows: a program is terminating if it terminates for any initial values; while it is non-terminating if at least one initial value makes it not terminates. Obviously, this definition does not consider program termination\´s dependency on initial values, and actually presents two extreme situations of the complicated programs in reality. Different from these two situations, this paper discusses what kinds of initial values can guarantee a program to terminate and what kinds of initial values cannot. For some linear loop assignment programs, whose terminations are decidable, the paper proposes a method using "limit" and "backward iteration" to derive the initial value set that make programs terminate.
Keywords :
decidability; program control structures; program verification; backward iteration; computer program; decidability analysis; limit iteration; linear loop assignment program; loop programs; program termination; program verification; software safety; termination set; Bismuth; Colon; Conferences; Logic programming; Polynomials; program verification; termination; termination set;
Conference_Titel :
Computer Science and Service System (CSSS), 2011 International Conference on
Conference_Location :
Nanjing
Print_ISBN :
978-1-4244-9762-1
DOI :
10.1109/CSSS.2011.5974588