Regular PapersNo Access

TERMINATION ANALYSIS OF LINEAR LOOPS

Shanghai Key Laboratory of Trustworthy Computing, Department of Computer Science, East China Normal University, Shanghai 200062, China

Search for more papers by this author

LIANGYU CHEN

Shanghai Key Laboratory of Trustworthy Computing, East China Normal University, Shanghai 200062, China

Search for more papers by this author

ZHENBING ZENG

Shanghai Key Laboratory of Trustworthy Computing, East China Normal University, Shanghai 200062, China

Search for more papers by this author

, and

ZHI-BIN LI

Shanghai Key Laboratory of Trustworthy Computing, Department of Computer Science, East China Normal University, Shanghai 200062, China

Search for more papers by this author

https://doi.org/10.1142/S0129054110007696Cited by:3 (Source: Crossref)

Abstract

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.

Keywords:

AMSC: 68N30, 68Q60, 68W30

References

M. Achatz, S. McCallum and V. Weispfenning, Deciding polynomial-exponential problems, ISSAC (ACM Press, New York, 2008) pp. 215–222. Google Scholar
A. R. Bradley, Z. Manna and H. B. Sipma, Linear ranking with reachability, CAV, LNCS 3576, eds. K. Etessami and S. K. Rajamani (Springer, New York, 2005) pp. 491–504. Google Scholar
A. R. Bradley, Z. Manna and H. B. Sipma, The polyranking principle, ICALP, LNCS 3580, eds. L. Caireset al. (Springer, New York, 2005) pp. 1349–1361. Google Scholar
M. Braverman, Termination of integer linear programs, CAV, LNCS 4144, eds. T. Ball and R. B. Jones (Springer, New York, 2006) pp. 372–385. Google Scholar
P. Cousot, Proving program invariance and termination by parametric abstraction, Lagrangian relaxation and semidefinite programming, VMCAI, LNCS 3385, ed. R. Cousot (Springer, New York, 2005) pp. 1–24. Google Scholar
P. Cousot and R. Cousot, Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints, POPL (ACM Press, New York, 1977) pp. 238–252. Google Scholar
M. D. Davis and E. J. Weyuker , Computability, Complexity, and Languages: Fundamentals of Theoretical Computer Science ( Academic Press , New York , 1983 ) . Google Scholar
G. H. Hardy and E. M. Wright, An Introduction to the Theory of Numbers, 5th edn. (Oxford University Press, London, 1979). Google Scholar
C. A. R. Hoare, Communications of the ACM 12(10), 576 (1969), DOI: 10.1145/363235.363259. Crossref, Web of Science, Google Scholar
K. Hoffman and R. Kunze , Linear Algebra , 2nd edn. ( Prentice Hall , New Jersey , 1971 ) . Google Scholar
R. A. Horn and C. R. Johnson , Matrix Analysis ( Cambridge University Press , Cambridge , 1985 ) . Crossref, Google Scholar
V. I. Istratescu , Fixed Point Theory: An Introduction ( Springer , New York , 2001 ) . Google Scholar
N. Jacobson , Basic Algebra I ( W. H. Freeman and Company , San Francisco , 1974 ) . Google Scholar
D. Kapur, Journal of Systems Science and Complexity 19(3), 307 (2006), DOI: 10.1007/s11424-006-0307-x. Crossref, Web of Science, Google Scholar
S. Leue and W. Wei, A region graph based approach to termination proofs, TACAS, LNCS 3920, eds. H. Hermanns and J. Palsberg (Springer, New York, 2006) pp. 318–333. Google Scholar
A. Podelski and A. Rybalchenko, Transition invariants, LICS (IEEE Computer Society, 2004) pp. 32–41. Google Scholar
A. Podelski and A. Rybalchenko, ACM Transactions on Programming Languages and Systems 29(3), 132 (2007), DOI: 10.1145/1232420.1232422. Google Scholar
A. Tiwari, Termination of linear programs, CAV, LNCS 3114, eds. R. Alur and D. A. Peled (Springer, New York, 2004) pp. 70–82. Google Scholar
L. Yanget al., Program verification by using DISCOVERER, VSTTE, LNCS 4171, eds. B. Meyer and J. Woodcock (Springer, New York, 2005) pp. 528–538. Google Scholar