KMS Chongqing Institute of Green and Intelligent Technology, CAS
Detection of Ranking Functions of Polynomial Loop Programs | |
Li, Yi; Feng, Yong | |
2019 | |
摘要 | Synthesizing ranking functions of loop programs is the dominant method for checking their termination. In this study, the synthesis of ranking functions of a class of loop program is reduced to the detection of positive polynomial on the standard simplex. This then enables the computation of the desired ranking functions by linear programming tool. Different from the existing methods based on cylindrical algebraic decomposition, the proposed method in the study can get more expressive polynomial ranking functions within an acceptable time. © Copyright 2019, Institute of Software, the Chinese Academy of Sciences. All rights reserved. |
DOI | 10.13328/j.cnki.jos.005567 |
发表期刊 | Ruan Jian Xue Bao/Journal of Software |
ISSN | 10009825 |
卷号 | 30期号:11页码:3243-3258 |
收录类别 | EI |
语种 | 中文 |