We found a match
Your institution may have rights to this item. Sign in to continue.
- Title
On ranking functions for single-path linear-constraint loops.
- Authors
Li, Yi; Wu, Wenyuan; Feng, Yong
- Abstract
Program termination is a fundamental research topic in program analysis. In this paper, we present a new complete polynomial-time method for the existence problem of linear ranking functions for single-path loops described by a conjunction of linear constraints, when variables range over the reals (or rationals). Unlike existing methods, our method does not depend on Farkas' Lemma and provides us with counterexamples to existence of linear ranking functions, when no linear ranking function exists. In addition, we extend our results established over the rationals to the setting of the integers. This deduces an alternative approach to deciding whether or not a given SLC loop has a linear ranking function over the integers. Finally, we prove that the termination of bounded single-path linear-constraint loops is decidable over the reals (or rationals).
- Subjects
INTEGERS; SOFTWARE reliability
- Publication
International Journal on Software Tools for Technology Transfer, 2020, Vol 22, Issue 6, p655
- ISSN
1433-2779
- Publication type
Article
- DOI
10.1007/s10009-019-00549-9