KMS Chongqing Institute of Green and Intelligent Technology, CAS
| On ranking functions for single-path linear-constraint loops | |
Li, Yi  ; Wu, Wenyuan; Feng, Yong
| |
| 2019-11-13 | |
| 摘要 | 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). |
| 关键词 | Software reliability Program termination Linear ranking functions Farkas' lemma |
| DOI | 10.1007/s10009-019-00549-9 |
| 发表期刊 | INTERNATIONAL JOURNAL ON SOFTWARE TOOLS FOR TECHNOLOGY TRANSFER
 |
| ISSN | 1433-2779 |
| 页码 | 12 |
| 通讯作者 | Li, Yi(zm_liyi@163.com) |
| 收录类别 | SCI |
| WOS记录号 | WOS:000496208800001 |
| 语种 | 英语 |
