Termination Analysis of Single-path Linear Constraint Loops

被引：0
|
作者：
Li Y. [1 ]
Tang T. [1 ,2 ]
机构：
[1] Automated Reasoning and Cognition Center, Chongqing Institute of Green and Intelligent Technology, Chinese Academy of Sciences, Chongqing
[2] University of Chinese Academy of Sciences, Beijing
来源：
Ruan Jian Xue Bao/Journal of Software | 2024年 / 35卷 / 03期
关键词：
increasing function; linear ranking function; loop program; multiphase ranking function; termination;
D O I：
10.13328/j.cnki.jos.006817
中图分类号：
学科分类号：
摘要：
The ranking function method is the main method for the termination analysis of loops, and it indicates that loop programs can be terminated. In view of single-path linear constraint loop programs, this study presents a method to analyze the termination of the loops. Based on the calculation of the normal space of the increasing function, this method considers the calculation of the ranking function in the original program space as that in the subspace. Experimental results show that the method can effectively verify the termination of most loop programs in the existing literature. © 2024 Chinese Academy of Sciences. All rights reserved.
引用
收藏
页码：1307 / 1320
页数：13
相关论文
共 30 条
  • [1] Turing AM., On computable numbers, with an application to the Entscheidungsproblem, Proc. of the London Mathematical Society, s2-42, 1, pp. 230-265, (1937)
  • [2] Turing AM., On computable numbers, with an application to the Entscheidungsproblem—A correction, Proc. of the London Mathematical Society, s2-43, 1, pp. 544-546, (1938)
  • [3] Tiwari A., Termination of linear programs, Proc. of the 16th Int’l Conf. on Computer Aided Verification, pp. 70-82, (2004)
  • [4] Li Y., Witness to non-termination of linear programs, Theoretical Computer Science, 681, pp. 75-100, (2017)
  • [5] Xia BC, Zhang ZH., Termination of linear programs with nonlinear constraints, Journal of Symbolic Computation, 45, 11, pp. 1234-1249, (2010)
  • [6] Liu J, Xu M, Zhan NJ, Zhao HJ., Discovering non-terminating inputs for multi-path polynomial programs, Journal of Systems Science and Complexity, 27, 6, pp. 1286-1304, (2014)
  • [7] Chen YF, Heizmann M, Lengal O, Li Y, Tsai MH, Turrini A, Zhang LJ., Advanced automata-based algorithms for program termination checking, ACM SIGPLAN Notices, 53, 4, pp. 135-150, (2018)
  • [8] He F, Han JT., Termination analysis for evolving programs: An incremental approach by reusing certified modules, Proc. of the ACM on Programming Languages, 4, (2020)
  • [9] Chatterjee K, Fu HF, Goharshady AK., Termination analysis of probabilistic programs through positivstellensatz’s, Proc. of the 28th Int’l Conf. on Computer Aided Verification, pp. 3-22, (2016)
  • [10] Xue B, Zhan NJ, Li YJ, Wang QY., Robust non-termination analysis of numerical software, Proc. of the 4th Int’l Symp. on Dependable Software Engineering. Theories, Tools, and Applications, pp. 69-88, (2018)
123