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
LI Yi1,2, CAI Tian-xun1,2, WU Wen-yuan2
CLC Number:
[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. |
|