计算机科学 ›› 2023, Vol. 50 ›› Issue (9): 108-116.doi: 10.11896/jsjkx.220700214
王垚1,2, 李轶1
WANG Yao1,2, LI Yi1
摘要： 秩函数作为循环程序终止性分析的重要方法已得到广泛研究。文中着重研究了单分支循环的终止性。首先提出了双向迭代循环概念,将单分支循环分为双向迭代循环和非双向迭代循环。其次,针对双向迭代循环程序,建立了一种划分思路,提出了三段式秩函数的概念,并证明了若该双向迭代循环存在三段式秩函数,则其是终止的。而对非双向迭代循环,引用增函数的划分思路,即利用增函数将原程序空间划分为更小的空间,并通过计算更小空间上的秩函数来证明原程序的终止性。最后,将三段式秩函数的计算问题归结为SVM分类问题,并利用工具Z3或bottema对由SVM所得的候选秩函数进行验证。
中图分类号:
| [1]COL'ON M A,SIPMA H B.Synthesis of Linear Ranking Functions[C]//International Conference on Tools and Algorithms for the Construction and Analysis of Systems.Berlin:Springer,2001:67-81. [2]COL'ON M A,SIPMA H B.Practical Methods for Proving Program Termination[C]//International Conference on Computer Aided Verification.Berlin:Springer,2002:442-454. [3]PODELSKI A,RYBALCHENKO A.A Complete Method forthe Synthesis of Linear Ranking Functions[C]//International Workshop on Verification,Model Checking,and Abstract Interpretation.Berlin:Springer,2004:239-251. [4]BRADLEY A R,MANNA Z,SIPMA H B.The PolyrankingPrinciple[C]//International Colloquium on Automata,Languages,and Programming.Berlin:Springer,2005:1349-1361. [5]BRADLEY A R,MANNA Z,SIPMA H B.Linear Ranking with Reachability[C]//Computer Aided Verification,17th International Conference,CAV 2005.Edinburgh,Scotland:DBLP,2005:491-504. [6]BEN-AMRAM A M,GENAIM S.Ranking Functions forLinear-Constraint Loops[J].Journal of the ACM,2012,61(4):1-55. [7]BAGNARA R,ESNARD F,PESCETTI A,et al.A new look at the automatic synthesis of linear ranking functions[J].Information and Computation,2012,215:47-67. [8]BEN-AMRAM A M,GENAIM S,MASUD A N.On the Termination of Integer Loops[J].ACM Transactions on Programming Languages & Systems,2012,34(4):1-24. [9]BAGNARA R,MESNARD F.Eventual Linear Ranking Func-tions [C]//Proceedings of the 15th Symposium on Principles and Practice of Declarative Programming.Madrid,Spain:ACM,2013:229-238. [10]BEN-AMRAM A M,GENAIM S.On the Linear Ranking Pro-blem for Integer Linear-ConstraintLoops[J].ACM Sigplan Notices,2013,48(1):51-62. [11]LEIKE J,HEIZMANN M,HOENICKE J,et al.Linear Ranking for Linear Lasso Programs.[C]//Automated Technology for Verification and Analysis.Cham:Springer,2013:365-380. [12]LEIKE J,HEIZMANN M.Ranking Templates for Linear Loops[J].Logical Methods in Computer Science,2015,11(1):1-27. [13]BEN-AMRAM A M,GENAIM S.On Multiphase-Linear Ran-king Functions[C]//International Conference on Computer Aided Verification.Cham:Springer,2017:601-620. [14]BEN-AMRAM A M,DOMÉNECH J J,GENAIM S.Multi-phase-Linear Ranking Functions and their Relation to Recurrent Sets[C]//International Static Analysis Symposium.Cham:Springer,2018:459-480. [15]COUSOT P.Proving Program Invariance and Termination byParametric Abstraction,Lagrangian Relaxation and Semidefinite Programming[C]//Verification,Model Checking,& Abstract Interpretation.Berlin:Springer,2005:1-24. [16]CHEN Y,XIA B,LU Y,et al.Discovering Non-linear Ranking Functions by Solving Semi-algebraic Systems[C]//Theoretical Aspects of Computing－ICTAC 2007.2007:34-49. [17]SHEN L,WU M,YANG Z,et al.Generating exact nonlinearranking functions by symbolic-numeric hybrid method[J].Journal of Systems Science and Complexity,2013,26(2):291-301. [18]LI Y,ZHU G,FENG Y.The L-Depth Eventual Linear Ranking Functions for Single-Path Linear Constraint Loops[C]//The 10th International Symposium on Theoretical Aspects of Software Engineering.IEEE,2016:30-37. [19]YUAN Y,LI Y.Ranking function detection via SVM:A more general method[J].IEEE Access,2019(7):9971-9979. [20]LI Y,SUN X C,LI Y,et al.Synthesizing Nested Ranking Functions for Loop Programs via SVM[C]//International Confe-rence on Formal Engineering Methods.Cham:Springer,2019:438-454. [21]SUN X C.Proving the Termination of Loop Programs based on SVM [D].Beijing:Institute of Software,Chinese Academy of Sciences,2020. [22]GENAIM S.LoopKiller:website for termination analysis[EB/OL].http://loopkiller.com/irankfinder. |
|
||
首页