Title :
Termination of Nested Loop
Author :
Wu, Bin ; Bi, Zhongqin
Author_Institution :
Shanghai Key Lab. of Trustworthy Comput., East China Normal Univ., Shanghai, China
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;
Conference_Titel :
Computer Science and Computational Technology, 2008. ISCSCT '08. International Symposium on
Conference_Location :
Shanghai
Print_ISBN :
978-1-4244-3746-7
DOI :
10.1109/ISCSCT.2008.58
