微信服务号

微信订阅号

2025-4-6- 6
Home > Archive>Volume 30, Issue 11, 2019 >3243-3258. DOI:10.13328/j.cnki.jos.005567
PDF HTML XML Export Cite reminder
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
    • | |
  • Metrics
    • |
  • Reference [28]
    • |
  • Related [20]
    • | | |
  • 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
    [1] Cook B, Podelski A, Rybalchenko A. Proving program termination. Communications of the ACM, 2011,54(5):88-98.
    [2] Chen YH, Xia BC, Yang L, Zhou CC. Discovering non-linear ranking functions by solving semi-algebraic systems. In:Proc. of the 4th Int'l Colloquium on Theoretical Aspects of Computing. Berlin, Heidelberg:Springer-Verlag, 2007.34-49.
    [3] Colón M, Sipma HB. Practical methods for proving program termination. In:Proc. of the Computer Aided Verification. Berlin, Heidelberg:Springer-Verlag, 2002.227-240.
    [4] Podelski A, Rybalchenko A. A complete method for the synthesis of linear ranking functions. In:Proc. of the 5th Int'l Conf. on Verification, Model Checking, and Abstract Interpretation. Berlin, Heidelberg:Springer-Verlag, 2004.239-251.
    [5] Bradley A, Manna Z, Sipma H. The polyranking principle. In:Caires L, Italiano G, Monteiro L, Palamidessi C, Yung M, eds. Proc. of the Automata, Languages and Programming. Berlin, Heidelberg:Springer-Verlag, 2005.1349-1361.
    [6] Bradley A, Manna Z, Sipma H. Linear ranking with reachability. In:Proc. of the Int'l Conf. on Computer Aided Verification. Berlin, Heidelberg:Springer-Verlag, 2005.491-504.
    [7] Bagnara R, Mesnard F, Pescetti A, Zaffanella E. A new look at the automatic synthesis of linear ranking functions. Information and Computation, 2012,215:47-67.
    [8] Ben-Amram AM, Genaim S. On the linear ranking problem for integer linear-constraint loops. In:Proc. of the 40th Annual ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages. New York:ACM Press, 2013.51-62.
    [9] Cousot P. Proving program invariance and termination by parametric abstraction, langrangian relaxation and semidefinite programming. In:Proc. of the 6th Int'l Conf. on Verification, Model Checking, and Abstract Interpretation. Berlin, Heidelberg:Springer-Verlag, 2005.1-24.
    [10] Yang L, Zhou CC, Zhan NJ, Xia BC. Recent advances in program verification through computer algebra. Frontiers of Computer Science in China, 2010, 4(1):1-16.
    [11] Chen HY, Cook B, Fuhs C, Nimkar K, et al. Proving nontermination via safety. In:Proc. of the 20th Int'l Conf. on Tools and Algorithms for the Construction and Analysis of Systems. Berlin, Heidelberg:Springer-Verlag, 2014.156-171.
    [12] Gupta A, Henzinger T, Majumdar R, et al. Proving non-termination. In:Proc. of the 35th Annual ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages. New York:ACM Press, 2008.147-158.
    [13] Tiwari A. Termination of linear programs. In:Proc. of the 16th Int'l Conf. on Computer Aided Verification. Berlin, Heidelberg:Springer-Verlag, 2004.70-82.
    [14] Braverman M. Termination of integer linear programs. In:Proc. of the 18th Int'l Conf. on Computer Aided Verification. Berlin, Heidelberg:Springer-Verlag, 2006.372-385.
    [15] Xia BC, Yang L, Zhan NJ, Zhang ZH. Symbolic decision procedure for termination of linear programs. Formal Aspects of Computing, 2009,23(2):171-190.
    [16] Bradley A, Manna Z, Sipma H. Termination of polynomial programs. In:Proc. of the 6th Int'l Conf. on Verification, Model Checking, and Abstract Interpretation. Berlin, Heidelberg:Springer-Verlag, 2005.113-129.
    [17] Xia BC, zhang ZH. Termination of linear programs with nonlinear constraints. Journal of Symbolic Computation, 2010,45(11):1234-1249.
    [18] Babic D, Cook B, Hu AJ, et al. Proving termination of nonlinear command sequences. Formal Aspects of Computing, 2013,25(3):389-403.
    [19] Liu J, Xu M, Zhan NJ, Zhao HJ. Discovering non-terminating inputs for multi-path polynomial programs. Journal of Systems Science and Complexity, 2014,27(4):1284-1304.
    [20] Colón M, Sipma HB. Synthesis of linear ranking functions. In:Proc. of the 7th Int'l Conf. on Tools and Algorithms for the Construction and Analysis of Systems. Berlin, Heidelberg:Springer-Verlag, 2001.67-81.
    [21] Powers V, Reznick B. A new bound for Polya's theorem with applications to polynomials positive on polyhedra. Journal of Pure and Applied Algebra, 2001,164(1-2):221-229.
    [22] Collins GE. Quantifier elimination for real closed fields by cylindrical algebraic decomposition. In:Proc. of the Automata Theory and Formal Languages. Berlin, Heidelberg:Springer-Verlag, 1975.134-165.
    [23] Yang L, Xia BC. Mechanical Inequality Proving and Automated Discovering. Beijing:Science Press, 2008(in Chinese).
    [24] Löfberg J. YALMIP:A MATLAB toolbox for rapid prototyping of optimization problems. Automatic Control Laboratory, Eidgenössische Technische Hochschule Zürich, 2004. http://control.ee.ethz.ch/joloef/yalmip.msql
    [25] Hou XR, Shao JW. Bounds on the number of steps of WDS required for checking the positivity of integral forms. Applied Mathematics and Computation, 2011,217(2):9978-9984.
    [26] Pugh W. The omega test:A fast and practical integer programming algorithm for dependence analysis. In:Martin JL, ed. Proc. of the Supercomputing. ACM Press, 1991.4-13.
    附中文参考文献:
    [23] 杨路,夏壁灿.不等式机器证明与自动发现.北京:科学出版社,2008.
    Cited by
    Comments
    Comments
    分享到微博
    Submit
Get Citation

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

Copy
Share
Article Metrics
  • Abstract:2655
  • PDF: 4033
  • HTML: 2334
  • Cited by: 0
History
  • Received:September 01,2017
  • Revised:November 09,2017
  • Online: May 02,2018
Links:Institute of Software, CASChina Computer FederationCASNSFC
You are the first2033299Visitors
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