DocumentCode
2098547
Title
Termination of Nested Loop
Author
Wu, Bin ; Bi, Zhongqin
Author_Institution
Shanghai Key Lab. of Trustworthy Comput., East China Normal Univ., Shanghai, China
Volume
2
fYear
2008
fDate
20-22 Dec. 2008
Firstpage
536
Lastpage
539
Abstract
The verification of termination is a difficult problem. While most of the recent work on automated termination proofs focuses on the construction of linear ranking functions for unnested loops, we present an algorithm based on region graphs to prove termination of nested loops. The method can prove the termination of terminating nested loops that may not have linear ranking function. For the programs we have considered, this approach converges faster and sufficiently.
Keywords
data flow graphs; program control structures; program verification; linear ranking functions; nested loop; program loops; termination verification; Arithmetic; Bismuth; Computational modeling; Computer science; Flow graphs; Laboratories; Safety; nested loop; program verification; ranking function; termination;
fLanguage
English
Publisher
ieee
Conference_Titel
Computer Science and Computational Technology, 2008. ISCSCT '08. International Symposium on
Conference_Location
Shanghai
Print_ISBN
978-1-4244-3746-7
Type
conf
DOI
10.1109/ISCSCT.2008.58
Filename
4731682
Link To Document