Computer Science ›› 2017, Vol. 44 ›› Issue (1): 194-198.doi: 10.11896/j.issn.1002-137X.2017.01.037

Previous Articles     Next Articles

New Method for Computing Eventual Linear Ranking Functions

ZHU Guang, LI Yi and WU Wen-yuan   

  • Online:2018-11-13 Published:2018-11-13

Abstract: Termination of linear loop programs has received extensive attention in these years.In this paper,we focused on the termination of linear constraint loops which has no traditional linear ranking functions.A method of detecting eventual linear ranking functions by Bagnara were introduced for termination analysis first.Such an eventual linear ranking function implies the loop terminates.We presented a new method for computing eventual linear ranking functions.Semi-algebraic systems,equivalent to linear increasing functions and eventual linear ranking functions,were established.Several methods for synthesizing eventual linear ranking functions were compared.And experimental results show that the semi-algebraic system for synthesis of eventual linear ranking functions established by our method is simpler.

Key words: Linear loop programs,Termination analysis,Eventual linear ranking functions,Mathematica

[1] 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 .
[2] BAGNARA R,MESNARD F,PESCETTI A, et al.A new look at the automatic synthesis of linear ranking functions[J].Information and Computation,2012,215(3):47-67.
[3] BEN-AMRAM A M,GENAIM S,MASUD A.On the Termination of Integer Loops[M].Verification,Model Checking,and Abstract Interpretation.V.Kuncak and A.Rybalchenko,SpringerBerlin Heidelberg,2012,7148:72-87.
[4] 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.
[5] BEN-AMRAM A M,GENAIM S.Ranking Functions for Linear-Constraint Loops[J].Journal of the ACM,2014,61(4):1-55.
[6] BRADLEY A,MANNA Z,SIPMA H.Linear Ranking with Rea-chability.Computer Aided Verification[M].Etessami K,Rajamani S.Springer Berlin Heidelberg,2005,3576:491-504.
[7] BRADLEY A,MANNA Z,SIPMA H.The Polyranking Principle.Automata,Languages and Programming[M].Caires L,Ita-liano G,Monteiro L,et al.eds.,Springer Berlin Heidelberg,2005,3580:1349-1361.
[9] CHEN H Y,FLUR S,MUKHOPADHYAY S.TerminationProofs for Linear Simple Loops[M]∥Static Analysis.A.Miné and D.Schmidt,Springer Berlin Heidelberg,2012,0:422-438.
[10] CHEN Y H,XIA B C,YANG L,et al.Discovering Non-linear Ranking Functions by Solving Semi-algebraic Systems[M]∥Theoretical Aspects of Computing(ICTAC 2007).Springer Berlin Heidelberg,2007:34-49.
[11] CHEN Y H,XIA B X,YANG L,et al.Generating Polynomial Invariants with DISCOVERER and QEPCAD[M].Formal Methods and Hybrid Real-Time Systems.CliffB Jones,Zhiming Liu and Jim Woodcock,Springer Berlin Heidelberg,2007,4700:67-82.
[12] COLN M,SIPMA H.Synthesis of Linear Ranking Functions.Tools and Algorithms for the Construction and Analysis of Systems[M].T.Margaria and W.Yi,Springer Berlin Heidelberg,2001,2031:67-81.
[13] COOK B,GULWANI S,LEV-AMI T,et al.Proving Conditional Termination.Computer Aided Verification[M].A.Gupta and S.Malik,Springer Berlin Heidelberg,2008,5123:328-340.
[14] GANTY P,GENAIM S.Proving Termination Starting from the End.Computer Aided Verification[M].Sharygina N,Veith H.Springer Berlin Heidelberg,2013,8044:397-412.
[15] HEIZMANN M,HOENICKE J,LEIKE J,et al.Linear Ranking for Linear Lasso Programs[M].Automated Technology for Verification and Analysis.Van Hung D,Ogawa M.Springer International Publishing,2013,8172:365-380.
[16] PODELSKI A,RYBALCHENKO A.A Complete Method forthe Synthesis of Linear Ranking Functions[M].Verification,Model Checking,and Abstract Interpretation.Steffen B,Levi G.Springer Berlin Heidelberg,2004,2937:239-251.
[17] TIWARI A.Termination of Linear Programs.Computer Aided Verification[M].R.Alur and D.Peled,Springer Berlin Heidelberg,2004,3114:70-82.
[18] LI K,SHAN Z G,WANG J,et al.Overview on Major Research Plan of Trustworthy Software[J].Bulletin of National Natural Science Foundation of China,2008,2(3):145-151.(in Chinese) 李克,单志广,王戟,等.可信软件基础研究重大研究计划综述[J].中国科学基金,2008,22(3):145-151.
[19] YANG L,ZHANG J Z,HOU X R.Nonlinear Systems of Algebraic Equations and Automated Theorem Proving[M].Beijing:Shanghai Scientific and Technological Education Publishing House,1996.(in Chinese) 杨路,张景中,侯晓荣.非线性代数方程组与定理机器证明[M].北京:上海科技教育出版社,1996.
[20] YANG L,XIA B C.Inequality Machine Proving and Automated Discovery[M].Beijing:Science Press,2008.(in Chinese) 杨路,夏壁灿.不等式机器证明与自动发现[M].北京:科学出版社,2008.

No related articles found!
Viewed
Full text


Abstract

Cited

  Shared   
  Discussed   
No Suggested Reading articles found!