计算机科学 ›› 2017, Vol. 44 ›› Issue (1): 194-198.doi: 10.11896/j.issn.1002-137X.2017.01.037
朱广,李轶,吴文渊
ZHU Guang, LI Yi and WU Wen-yuan
摘要： 程序的终止性分析作为程序验证中重要的一环,在软件正确性验证中极为重要。对于一个线性循环程序,若该程序没有传统定义的线性秩函数,则基于传统定义的秩函数终止性分析方法失效。2013年,Bagnara提出了最终线性秩函数(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] COLN 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! |
|
||
首页