DocumentCode :
2618725
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
fYear :
2011
fDate :
27-29 June 2011
Firstpage :
3124
Lastpage :
3127
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;
fLanguage :
English
Publisher :
ieee
Conference_Titel :
Computer Science and Service System (CSSS), 2011 International Conference on
Conference_Location :
Nanjing
Print_ISBN :
978-1-4244-9762-1
Type :
conf
DOI :
10.1109/CSSS.2011.5974588
Filename :
5974588
Link To Document :
بازگشت