Journal of Computer Applications ›› 2022, Vol. 42 ›› Issue (2): 565-573.DOI: 10.11772/j.issn.1001-9081.2021020221
• Computer software technology • Previous Articles Next Articles
Received:
2021-02-05
Revised:
2021-04-12
Accepted:
2021-04-13
Online:
2022-02-11
Published:
2022-02-10
Contact:
Yi LI
About author:
TAN Wang, born in 1995, M. S. candidate. His research interests include, termination verification for loop programs, machine learning.Supported by:
通讯作者:
李轶
作者简介:
谭旺(1995—),男,重庆人,硕士研究生,主要研究方向:循环程序终止性验证、机器学习;基金资助:
CLC Number:
Wang TAN, Yi LI. Synthesis of loop bound functions for loop programs[J]. Journal of Computer Applications, 2022, 42(2): 565-573.
谭旺, 李轶. 循环程序的界函数合成[J]. 《计算机应用》唯一官方网站, 2022, 42(2): 565-573.
Add to citation manager EndNote|Ris|BibTeX
URL: https://www.joca.cn/EN/10.11772/j.issn.1001-9081.2021020221
编号 | 界函数模板 | 负类点 | 模板系数 |
---|---|---|---|
1 | (0,0,1) | (2,2,2) | |
2 | (10,1) | (10,0) | |
3 | (-1,-1,1) | (1,1,1) | |
4 | (0,0,1) | (3.34,3.32,1) | |
5 | (-1,0.5,1) | (2,2,1) | |
6 | (0,0,1) | (3,5,4) | |
7 | (-1,-1,1) | (2,2,4) | |
8 | (-1,-1,1) | (3,3,9) | |
9 | (-1,-1,1) | (3,2,16) | |
10 | (0,0,1) | (6,6,25) |
Tab. 2 Experimental parameters and template coefficients
编号 | 界函数模板 | 负类点 | 模板系数 |
---|---|---|---|
1 | (0,0,1) | (2,2,2) | |
2 | (10,1) | (10,0) | |
3 | (-1,-1,1) | (1,1,1) | |
4 | (0,0,1) | (3.34,3.32,1) | |
5 | (-1,0.5,1) | (2,2,1) | |
6 | (0,0,1) | (3,5,4) | |
7 | (-1,-1,1) | (2,2,4) | |
8 | (-1,-1,1) | (3,3,9) | |
9 | (-1,-1,1) | (3,2,16) | |
10 | (0,0,1) | (6,6,25) |
编号 | 基于QE 秩函数合成 | 基于SVM 秩函数合成 | 多阶段线性秩函数合成 | 本文方法 |
---|---|---|---|---|
1 | 成功 | 成功 | 失败 | 成功 |
2 | 成功 | 成功 | 成功 | 成功 |
3 | 失败 | 成功 | 失败 | 成功 |
4 | 失败 | 成功 | 失败 | 成功 |
5 | 失败 | 成功 | 失败 | 成功 |
6 | 失败 | 成功 | 失败 | 成功 |
7 | 失败 | 失败 | 成功 | 成功 |
8 | 失败 | 失败 | 成功 | 成功 |
9 | 失败 | 失败 | 成功 | 成功 |
10 | 失败 | 失败 | 失败 | 成功 |
Tab. 3 Feasibility comparison of different methods
编号 | 基于QE 秩函数合成 | 基于SVM 秩函数合成 | 多阶段线性秩函数合成 | 本文方法 |
---|---|---|---|---|
1 | 成功 | 成功 | 失败 | 成功 |
2 | 成功 | 成功 | 成功 | 成功 |
3 | 失败 | 成功 | 失败 | 成功 |
4 | 失败 | 成功 | 失败 | 成功 |
5 | 失败 | 成功 | 失败 | 成功 |
6 | 失败 | 成功 | 失败 | 成功 |
7 | 失败 | 失败 | 成功 | 成功 |
8 | 失败 | 失败 | 成功 | 成功 |
9 | 失败 | 失败 | 成功 | 成功 |
10 | 失败 | 失败 | 失败 | 成功 |
编号 | 基于QE 秩函数合成 | 基于SVM 秩函数合成 | 多阶段线性 秩函数合成 | 本文方法 |
---|---|---|---|---|
1 | 线性 | 线性 | 无法合成 | 线性 |
2 | 线性 | 线性 | 线性 | 线性 |
3 | 无法合成 | 线性 | 无法合成 | 线性 |
4 | 无法合成 | 线性 | 无法合成 | 线性 |
5 | 无法合成 | 非线性 | 无法合成 | 线性 |
6 | 无法合成 | 非线性 | 无法合成 | 线性 |
7 | 无法合成 | 无法合成 | 多阶段线性 | 线性 |
8 | 无法合成 | 无法合成 | 多阶段线性 | 线性 |
9 | 无法合成 | 无法合成 | 多阶段线性 | 线性 |
10 | 无法合成 | 无法合成 | 无法合成 | 非线性 |
Tab. 4 Comparison of experimental results in functional forms
编号 | 基于QE 秩函数合成 | 基于SVM 秩函数合成 | 多阶段线性 秩函数合成 | 本文方法 |
---|---|---|---|---|
1 | 线性 | 线性 | 无法合成 | 线性 |
2 | 线性 | 线性 | 线性 | 线性 |
3 | 无法合成 | 线性 | 无法合成 | 线性 |
4 | 无法合成 | 线性 | 无法合成 | 线性 |
5 | 无法合成 | 非线性 | 无法合成 | 线性 |
6 | 无法合成 | 非线性 | 无法合成 | 线性 |
7 | 无法合成 | 无法合成 | 多阶段线性 | 线性 |
8 | 无法合成 | 无法合成 | 多阶段线性 | 线性 |
9 | 无法合成 | 无法合成 | 多阶段线性 | 线性 |
10 | 无法合成 | 无法合成 | 无法合成 | 非线性 |
1 | COUSOT P, COUSOT R. An abstract interpretation framework for termination [C]// Proceedings of the 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. New York: ACM, 2012: 245-258. 10.1145/2103656.2103687 |
2 | LEE S C, JONES N D, BEN-AMRAM A M. The size-change principle for program termination [C]// Proceedings of the 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. New York: ACM, 2001: 81-92. 10.1145/360204.360210 |
3 | LEIKE J, HEIZMANN M. Geometric nontermination arguments [C]// Proceedings of the 2018 International Conference on Tools and Algorithms for the Construction and Analysis of Systems, LNCS10806. Cham: Springer, 2018: 266-283. |
4 | BRAVERMAN M. Termination of integer linear programs [C]// Proceedings of the 2006 International Conference on Computer Aided Verification, LNCS4144. Berlin: Springer, 2006: 372-385. |
5 | TIWARI A. Termination of linear programs [C]// Proceedings of the 2004 International Conference on Computer Aided Verification, LNCS3114. Berlin: Springer, 2004: 70-82. |
6 | TURING A M. On computable numbers, with an application to the Entscheidungsproblem[J]. Proceedings of the London Mathematical Society, 1937, s2-41(1): 230-265. 10.1112/plms/s2-42.1.230 |
7 | CHEN Y F, HEIZMANN M, LENGÁL O, et al. Advanced automata-based algorithms for program termination checking [C]// Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation. New York: ACM, 2018: 135-150. 10.1145/3192366.3192405 |
8 | FEDYUKOVICH G, ZHANG Y L, GUPTA A. Syntax-guided termination analysis [C]// Proceedings of the 2018 International Conference on Computer Aided Verification, LNCS10981. Cham: Springer, 2018: 124-143. |
9 | LI Y. Witness to non-termination of linear programs[J]. Theoretical Computer Science, 2017, 681: 75-100. 10.1016/j.tcs.2017.03.036 |
10 | BAGNARA R, MESNARD F. Eventual linear ranking functions [C]// Proceedings of the 15th International Symposium on Principles and Practice of Declarative Programming. New York: ACM, 2013: 229-238. 10.1145/2505879.2505884 |
11 | BEN-AMRAM A M, GENAIM S. Ranking functions for linear-constraint loops[J]. Journal of the ACM, 2014, 61(4): No.26. 10.1145/2629488 |
12 | BEN-AMRAM A M, GENAIM S. On multiphase-linear ranking functions [C]// Proceedings of the 2017 International Conference on Computer Aided Verification, LNCS10427. Cham: Springer, 2017: 601-620. |
13 | LEIKE J, HEIZMANN M. Ranking templates for linear loops [C]// Proceedings of the 2014 International Conference on Tools and Algorithms for the Construction and Analysis of Systems, LNCS8413. Berlin: Springer, 2014: 172-186. 10.2168/lmcs-11(1:16)2015 |
14 | LI Y, ZHU G, FENG Y. The l-depth eventual linear ranking functions for single-path linear constraint loops [C]// Proceedings of the 10th International Symposium on Theoretical Aspects of Software Engineering. Piscataway: IEEE, 2016: 30-37. 10.1109/tase.2016.8 |
15 | CHEN Y H, XIA B C, YANG L, et al. Discovering non-linear ranking functions by solving semi-algebraic systems [C]// Proceedings of the 2007 International Colloquium on Theoretical Aspects of Computing, LNCS4711. Berlin: Springer, 2007: 34-49. |
16 | SHEN L Y, WU M, YANG Z F, et al. Generating exact nonlinear ranking functions by symbolic-numeric hybrid method[J]. Journal of Systems Science and Complexity, 2013, 26(2): 291-301. 10.1007/s11424-013-1004-1 |
17 | YUAN Y, LI Y. Ranking function detection via SVM: a more general method[J]. IEEE Access, 2019, 7: 9971-9979. 10.1109/access.2018.2890692 |
18 | KOVÁCS L. Automated invariant generation by algebraic techniques for imperative program verification in Theorema[D]. Linz: Johannes Kepler University Linz, 2007: 43-75. |
19 | GULWANI S, JAIN S, KOSKINEN E. Control-flow refinement and progress invariants for bound analysis [C]// Proceedings of the 30th ACM SIGPLAN Conference on Programming Languages Design and Implementation. New York: ACM, 2009: 375-385. 10.1145/1542476.1542518 |
20 | GULWANI S, MEHRA K K, CHILIMBI T. SPEED: precise and efficient static estimation of program computational complexity [C]// Proceedings of the 36th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. New York: ACM, 2009: 127-139. 10.1145/1594834.1480898 |
21 | NORI A V, SHARMA R. Termination proofs from tests [C]// Proceedings of the 9th Joint Meeting on Foundations of Software Engineering. New York: ACM, 2013: 246-256. 10.1145/2491411.2491413 |
22 | 邢建英.程序验证关键技术研究[D].长沙:国防科学技术大学, 2011: 63-75. |
XING J Y. Study on program verification[D]. Changsha: National University of Defense Technology, 2011: 63-75. | |
23 | BERDINE J, CHAWDHARY A, COOK B, et al. Variance analyses from invariance analyses [C]// Proceedings of the 34th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. New York: ACM, 2007: 211-224. 10.1145/1190216.1190249 |
24 | CHAWDHARY A, COOK B, GULWANI S, et al. Ranking abstractions [C]// Proceedings of the 2008 International Conference on European Symposium on Programming. Cham: Springer, 2008: 148-162. 10.1007/978-3-540-78739-6_13 |
25 | TSITOVICH A, SHARYGINA N, WINTERSTEIGER C M, et al. Loop summarization and termination analysis [C]// Proceedings of the 2011 International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Cham: Springer, 2011: 81-95. 10.1007/978-3-642-19835-9_9 |
26 | KROENING D, SHARYGINA N, TSITOVICH A, et al. Termination analysis with compositional transition invariants [C]// Proceedings of the 2010 International Conference on Computer Aided Verification, LNCS6174. Berlin: Springer, 2010: 89-103. |
27 | PODELSKI A, RYBALCHENKO A. Transition invariants [C]// Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science. Piscataway: IEEE, 2004: 32-41. 10.1109/lics.2004.1319598 |
28 | PEDREGOSA F, VAROQUAUX G, GRAMFORT A, et al. Scikit-learn: machine learning in Python[J]. Journal of Machine Learning Research, 2011, 12: 2825-2830. 10.3389/fninf.2014.00014 |
29 | GULWANI S. SPEED: symbolic complexity bound analysis [C]// Proceedings of the 2009 International Conference on Computer Aided Verification, LNCS5643. Berlin: Springer, 2009: 51-62. |
30 | VAPNIK V N, CHERVONENKIS A Y. A note on one class of perceptrons[J]. Automation and Remote Control, 1964, 25(1): 103-109. |
31 | VAPNIK V N. Statistical learning theory[J]. Encyclopedia of the Sciences of Learning, 1998, 41(4): 3185-3185. |
32 | 周志华.机器学习[M].北京:清华大学出版社, 2016: 121-124. 10.21436/inbom.12382432 |
ZHOU Z H. Machine Learning[M]. Beijing: Tsinghua University Press, 2016: 121-124. 10.21436/inbom.12382432 |
[1] | Min SUN, Qian CHENG, Xining DING. CBAM-CGRU-SVM based malware detection method for Android [J]. Journal of Computer Applications, 2024, 44(5): 1539-1545. |
[2] | Enbao QIAO, Xiangyang GAO, Jun CHENG. Self-recovery adaptive Monte Carlo localization algorithm based on support vector machine [J]. Journal of Computer Applications, 2024, 44(10): 3246-3251. |
[3] | Xueyu HUANG, Huaiyu HE, Huimin LIN, Jinshui CHEN. Classification and recognition method of copper alloy metallograph based on feature aggregation [J]. Journal of Computer Applications, 2023, 43(8): 2593-2601. |
[4] | Lei YANG, Hongdong ZHAO, Kuaikuai YU. End-to-end speech emotion recognition based on multi-head attention [J]. Journal of Computer Applications, 2022, 42(6): 1869-1875. |
[5] | Zhen QU, Kunting LI, Zhixi FENG. Remote sensing image scene classification based on effective channel attention [J]. Journal of Computer Applications, 2022, 42(5): 1431-1439. |
[6] | Guifang QIAO, Shouming HOU, Yanyan LIU. Facial expression recognition algorithm based on combination of improved convolutional neural network and support vector machine [J]. Journal of Computer Applications, 2022, 42(4): 1253-1259. |
[7] | Qian GE, Guangbin ZHANG, Xiaofeng ZHANG. Automatic feature selection algorithm based on interaction of ReliefF with maximum information coefficient and SVM [J]. Journal of Computer Applications, 2022, 42(10): 3046-3053. |
[8] | Hongfei JIA, Xi LIU, Yu WANG, Hongbing XIAO, Suxia XING. Application of 3DPCANet in image classification of functional magnetic resonance imaging for Alzheimer’s disease [J]. Journal of Computer Applications, 2022, 42(1): 310-315. |
[9] | JIA Heming, JIANG Zichao, LI Yao, SUN Kangjian. Simultaneous feature selection optimization based on improved spotted hyena optimizer algorithm [J]. Journal of Computer Applications, 2021, 41(5): 1290-1298. |
[10] | YUAN Qianqian, DENG Hongmin, WANG Xiaohang. Citrus disease and insect pest area segmentation based on superpixel fast fuzzy C-means clustering and support vector machine [J]. Journal of Computer Applications, 2021, 41(2): 563-570. |
[11] | Hongliang CAO, Ying ZHANG, Bin WU, Fanyu LI, Xubo NA. Prediction method of liver transplantation complications based on transfer component analysis and support vector machine [J]. Journal of Computer Applications, 2021, 41(12): 3608-3613. |
[12] | Kai LI, Jie LI. Structure-fuzzy multi-class support vector machine algorithm based on pinball loss [J]. Journal of Computer Applications, 2021, 41(11): 3104-3112. |
[13] | TONG Lin, GUAN Zheng. Fuzzy granulation prediction of traffic flow based on improved whale optimization support vector machine [J]. Journal of Computer Applications, 2021, 41(10): 2919-2927. |
[14] | ZHANG Jianming, SHI Yuanhao, XU Zhengyi, WEI Jianming. Adaptive UWB/PDR fusion positioning algorithm based on error prediction [J]. Journal of Computer Applications, 2020, 40(6): 1755-1762. |
[15] | WANG Yang, ZHAO Hongdong. Human activity recognition based on improved particle swarm optimization-support vector machine and context-awareness [J]. Journal of Computer Applications, 2020, 40(3): 665-671. |
Viewed | ||||||
Full text |
|
|||||
Abstract |
|
|||||