CSpace
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.
DOI10.13328/j.cnki.jos.005567
发表期刊Ruan Jian Xue Bao/Journal of Software
ISSN10009825
卷号30期号:11页码:3243-3258
收录类别EI
语种中文