Computer Science

Computer Science ›› 2023, Vol. 50 ›› Issue (9): 108-116.doi: 10.11896/jsjkx.220700214

• Computer Software • Previous Articles     Next Articles

Termination Analysis of Single Path Loop Programs Based on Iterative Trajectory Division

WANG Yao1,2, LI Yi1   

  1. 1 Chongqing Key Laboratory of Automated Reasoning and Cognition,CIGIT,CAS,Chongqing 400714,China
    2 Chongqing School,University of Chinese Academy of Sciences,Chongqing 400714,China
  • Received:2022-07-24 Revised:2022-11-30 Online:2023-09-15 Published:2023-09-01
  • About author:WANG Yao,born in 1997,postgra-duate.Her main research interest is program verification.
    LI Yi,born in 1980,Ph.D,associate professor.His main research interests include program verification and symbolic computation.
  • Supported by:
    National Natural Science Foundation of China(61572024,11771421,61103110),National Science Foundation of Chongqing,China(cstc2019jcyj-msxmX0638),Chongqing Science and Technology Innovation Guidance Special Project(cstc2018jcyj-yszxX0002,cstc2019yszx-jcyjX0003),National Key Research and Development Program of China(2020YFA07123000) and Chinese Academy of Sciences “Light of West China” program.

PDF (PC)

3774

Abstract: The ranking function has been extensively studied as an important method of program termination analysis.In this paper,we focus on the termination of single-path loops.Firstly,the concept of two-way iterative loops is proposed,and the single-path loops are divided into bidirectional iterative loops and non-bidirectional iterative loops.Secondly,for the bidirectional iterative loop program,a division method and concept of trivial ranking function are proposed,and it is proved that if a bidirectional iterative loop exists a trivial rank function,it is terminated.As for the non-bidirectional iterative loop,we use incremental function as the division method,i.e.,the original program space is divided into smaller spaces by using incremental function,and the termination of the original program is proved by computing the ranking function on the smaller space.Finally,the problem of computing the trivial ranking function comes down to the SVM classification problem,and we verifies candidate ran-king functions using the tools Z3 or bottema.

Key words: Program verification, Ranking functions, Machine learning, Program termination

CLC Number: 

  • TP311
[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.
[1] HUANG Shuxin, ZHANG Quanxin, WANG Yajie, ZHANG Yaoyuan, LI Yuanzhang. Research Progress of Backdoor Attacks in Deep Neural Networks [J]. Computer Science, 2023, 50(9): 52-61.
[2] LI Ke, YANG Ling, ZHAO Yanbo, CHEN Yonglong, LUO Shouxi. EGCN-CeDML:A Distributed Machine Learning Framework for Vehicle Driving Behavior Prediction [J]. Computer Science, 2023, 50(9): 318-330.
[3] LIU Xiang, ZHU Jing, ZHONG Guoqiang, GU Yongjian, CUI Liyuan. Quantum Prototype Clustering [J]. Computer Science, 2023, 50(8): 27-36.
[4] WANG Yu, WANG Zuchao, PAN Rui. Survey of DGA Domain Name Detection Based on Character Feature [J]. Computer Science, 2023, 50(8): 251-259.
[5] LI Yang, LI Zhenhua, XIN Xianlong. Attack Economics Based Fraud Detection for MVNO [J]. Computer Science, 2023, 50(8): 260-270.
[6] ZHU Boyu, CHEN Xiao, SHA Letian, XIAO Fu. Two-layer IoT Device Classification Recognition Model Based on Traffic and Text Fingerprints [J]. Computer Science, 2023, 50(8): 304-313.
[7] LU Xingyuan, CHEN Jingwei, FENG Yong, WU Wenyuan. Privacy-preserving Data Classification Protocol Based on Homomorphic Encryption [J]. Computer Science, 2023, 50(8): 321-332.
[8] WANG Dongli, YANG Shan, OUYANG Wanli, LI Baopu, ZHOU Yan. Explainability of Artificial Intelligence:Development and Application [J]. Computer Science, 2023, 50(6A): 220600212-7.
[9] WANG Xiya, ZHANG Ning, CHENG Xin. Review on Methods and Applications of Text Fine-grained Emotion Recognition [J]. Computer Science, 2023, 50(6A): 220900137-7.
[10] WANG Jinjin, CHENG Yinhui, NIE Xin, LIU Zheng. Fast Calculation Method of High-altitude Electromagnetic Pulse Environment Based on Machine Learning [J]. Computer Science, 2023, 50(6A): 220500046-5.
[11] YIN Xingzi, PENG Ningning, ZHAN Xueyan. Filtered Feature Selection Algorithm Based on Persistent Homology [J]. Computer Science, 2023, 50(6): 159-166.
[12] CHEN Jinjie, HE Chao, XIAO Xiao, LEI Yinjie. Optical Performance Monitoring Method Based on Fine-grained Constellation Diagram Recognition [J]. Computer Science, 2023, 50(4): 220-225.
[13] PENG Yuefeng, ZHAO Bo, LIU Hui, AN Yang. Survey on Membership Inference Attacks Against Machine Learning [J]. Computer Science, 2023, 50(3): 351-359.
[14] XU Xia, ZHANG Hui, YANG Chunming, LI Bo, ZHAO Xujian. Fair Method for Spectral Clustering to Improve Intra-cluster Fairness [J]. Computer Science, 2023, 50(2): 158-165.
[15] WANG Yitan, WANG Yishu, YUAN Ye. Survey of Learned Index [J]. Computer Science, 2023, 50(1): 1-8.
Viewed
Full text


Abstract

Cited
  Shared   
  Discussed   
No Suggested Reading articles found!
渝ICP备16013121号-4
Add:18# Honghu West Rd., Yubei ,Chongqing,China    Post Code: 401121
Tel: 023-63500828/023-67039612/023-67039623
E-mail: jsjkx12@163.com
Powered by Beijing Magtech Co., Ltd.