Detection of Ranking Functions of Polynomial Loop Programs
Author:
Affiliation:

Clc Number:

TP301

Fund Project:

National Natural Science Foundation of China (61572024, 61103110, 11671377); Natural Science Foundation of Chongqing (cstc2019jcyj-msxmX0638)

  • Article
  • |
  • Figures
  • |
  • Metrics
  • |
  • Reference
  • |
  • Related
  • |
  • Cited by
  • |
  • Materials
  • |
  • Comments
    Abstract:

    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.

    Reference
    Related
    Cited by
Get Citation

李轶,冯勇.多项式循环程序的秩函数探测.软件学报,2019,30(11):3243-3258

Copy
Share
Article Metrics
  • Abstract:
  • PDF:
  • HTML:
  • Cited by:
History
  • Received:September 01,2017
  • Revised:November 09,2017
  • Adopted:
  • Online: May 02,2018
  • Published:
You are the firstVisitors
Copyright: Institute of Software, Chinese Academy of Sciences Beijing ICP No. 05046678-4
Address:4# South Fourth Street, Zhong Guan Cun, Beijing 100190,Postal Code:100190
Phone:010-62562563 Fax:010-62562533 Email:jos@iscas.ac.cn
Technical Support:Beijing Qinyun Technology Development Co., Ltd.

Beijing Public Network Security No. 11040202500063