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