Computer Science ›› 2018, Vol. 45 ›› Issue (6): 151-155.doi: 10.11896/j.issn.1002-137X.2018.06.026

• Software & Database Technology • Previous Articles     Next Articles

Termination Analysis of Linear Assignment Loop Program Based on k-ranking Functions

LI Yi1,2, CAI Tian-xun1,2, WU Wen-yuan2   

  1. College of Computer Science and Technology,Chongqing University of Posts and Telecommunications,Chongqing 400065,China1;
    Chongqing Key Laboratory of Automated Reasoning and Cognition,Chongqing Institute of Green and Intelligent Technology, Chinese Academy of Sciences,Chongqing 400714,China2
  • Received:2017-04-26 Online:2018-06-15 Published:2018-07-24

Abstract: The termination of loop programs plays an important role in program analysis.This paper focused on the termination of linear assignment loop programs which have no traditional linear ranking functions.Based on the precise computation of Anx,this paper expanded the concept of traditionally defined raking functions,gave a definition of k-ranking functions and proved the existence of k-ranking functions.All the computations on the synthesis of k-ranking functions were done by Regularchains,a symbolic computation tool in Maple.Experimental results show that somelinearloop programs which have no traditional linear ranking functions indeed can be proven to be terminating by the proposed method.

Key words: k-ranking functions, Linear loop programs, RegularChains, Termination analysis

CLC Number: 

  • TP311.5
[1]COLN M,SIPMA H.Synthesis of Linear Ranking Functions[C]//International Conf+Y63erence on Tools and Algorithms for the Construction and Analysis of Systems.Springer Berlin Heidelberg,2001:67-81.
[2]COLÓN M,SIPMA H.Practical Methods for Proving Program Termination[C]//International Conference on Computer Aided Verification.Springer Berlin Heidelberg,2002:442-454.
[3]PODELSKI A,RYBALCHENKO A.A Complete Method for the Synthesis of Linear Ranking Functions[C]//International Workshop on Verification,Model Checking,and Abstract Interpretation.Springer Berlin Heidelberg,2004:239-251.
[4]CHEN Y H,XIA B C,YANG L,et al.Discovering Non-linear Ranking Functions by Solving Semialgebraic Systems[C]//International Colloquium on Theoretical Aspects of Computing,Springer Berlin Heidelberg,2007:34-49.
[5]HEIZMANN M,HOENICKE J,LEIKE J.Linear Ranking for Linear Lasso Programs[C]//International Symposium on Automated Technology for Verification and Analysis.Springer,Cham,2013:365-380.
[6]BAGNARA R,MESNARD F.Eventual Linear Ranking Functions[C]//Proceedings of the 15th Symposium on Principles and Practice of Declarative Programming.Madrid,Spain,ACM,2013:229-238.
[7]LI Y,ZHU G,FENG Y.The L-Depth Eventual Linear Ranking Functions for Single-Path Linear Constraint Loops[C]//2016 10th International Symposium on Theoretical Aspects of Software Engineering.Shanghai,2016 :30-37.
[8]LEIKE J,HEIZMANN M.Ranking Templates for Linear Loops[C]//Tools and Algorithms for the Construction and Analysis of Systems,Springer Berlin Heidelberg,2014:172-186.
[9]BEN-AMRAM A M,GENAIM S.On the Linear Ranking Problem for Integer Linear-constraint Loops[C]//Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages(POPL’13).Rome,Italy,ACM,2013:51-62.
[10]TIWARI A.Termination of Linear Programs[C]//16th International Conference on Computer Aided Verification.Springer Berlin Heideiberg,2004:70-82.
[11]BRAVERMAN M.Termination of integer linear programs[C]//Proceedings of the 18th International conference on Computer Aided Verification.Springer-Verlag,2006:372-385.
[12]XIA B C,ZHANG Z H.Termination of linear programs with nonlinear constraints[J].Journal of Symbolic Computation,2010,45(11):1234-1249.
[13]LI Y.Termination of Single-Path Polynomial Loop Programs[C]//International Colloquium on Theoretical Aspects of Computing.2016:33-50.
[14]CHEN C B,MAZA M M.Quantifier Elimination by Cylindrical Algebraic Decomposition Based on Regular Chains[C]//Proceedings of the 39th International Symposium on Symbolic and Algebraic Computation.ACM,2014:91-98.
[1] ZHU Guang, LI Yi and WU Wen-yuan. New Method for Computing Eventual Linear Ranking Functions [J]. Computer Science, 2017, 44(1): 194-198.
Viewed
Full text


Abstract

Cited

  Shared   
  Discussed   
No Suggested Reading articles found!