Termination analysis of linear loops

Verification of program termination is an important problem in program correctness analysis. Automatically proving termination or finding nonterminating inputs as counter-examples for many programs will be a big breakthrough in theoretical computer science. A remarkable result, provided by Tiwari(2004), showed that the termination of linear loops is decidable and an eventually nonterminating input can be found for the given nonterminating loop. But some essential lemmas were missing in that proof and his algorithm could not generate a nonterminating input, which might be more widely utilized in software testing. In this paper, we discuss these details carefully and present an algorithm for producing a nonterminating input automatically. We reduce the problem of finding a nonterminating input to that of computing real root bound of a multi-exponential polynomial. This algorithm has been implemented in a Maple package based on symbolic computation. Thereby a stronger and complete decidable result in termination problem is established.