Title :
Termination of Two Variable Homogeneous Linear Loops
Author :
Yi Li ; Chuancan Li ; Wenyuan Wu ; Yong Feng
Author_Institution :
Chongqing Key Lab. of Automated Reasoning & Cognition, CIGIT, Chongqing, China
Abstract :
Tiwari gave the quantified formulas to check whether the two variable homogeneous linear loop terminates in 2004. But we find that a certain quantified formula is neglected in Tiwari´s result, which corresponds to a possible case of the set NT of nonterminating points. In this paper, through analysing all possible cases of NT, we reconstruct a group of complete quantified formulas to determine if the two variable homogeneous linear loop terminates.
Keywords :
program verification; software reliability; NT; complete quantified formulas; nonterminating points; program verification; quantified formulas; reliable software systems; two variable homogeneous linear loops; Algorithm design and analysis; Cognition; Computers; Security; Software systems; Standards; Vectors; Loop Termination; Program Verification; QEP-CAD; Quantifier Elimination;
Conference_Titel :
Business Intelligence and Financial Engineering (BIFE), 2013 Sixth International Conference on
Conference_Location :
Hangzhou
Print_ISBN :
978-1-4799-4778-2
DOI :
10.1109/BIFE.2013.3
