微信服务号

微信订阅号

2025年4月1日 22:12 星期二
首页 > 过刊浏览>2022年第33卷第8期 >2918-2929. DOI:10.13328/j.cnki.jos.006605
PDF HTML阅读 XML下载 导出引用 引用提醒
基于深度学习和反例制导的循环程序秩函数生成
作者:
作者简介:

林开鹏(1997－),男,硕士生,CCF学生会员,主要研究领域为形式化方法;
林望(1982－),男,博士,副教授,CCF专业会员,主要研究领域为形式化方法,软件分析与验证;
梅国泉(2001－),男,主要研究领域为形式化方法;
丁佐华(1964－),男,博士,教授,博士生导师,CCF高级会员,主要研究领域为智能系统软件建模,分析与测试.

通讯作者:

林望,E-mail:linwang@zstu.edu.cn

中图分类号:

TP311

基金项目:

浙江省自然科学基金(LY20F020020);上海工业控制系统安全创新功能型平台开放课题;上海工业控制安全创新科技有限公司资助课题


Ranking Function Synthesis for Loop Programs via Counterexample Guided Deep Learning
Author:
  • 摘要
    • | |
  • 访问统计
    • |
  • 参考文献 [27]
    • |
  • 相似文献 [20]
    • | | |
  • 文章评论
    摘要:

    程序终止性判定是程序分析与验证领域中的一个研究热点.针对非线性循环程序,提出了一种基于反例制导的神经网络型秩函数的构造方法.该方法采用学习组件和验证组件交互的迭代框架,其中,学习组件利用程序轨迹作为训练集合构造一个候选秩函数;验证组件运用可满足性模理论(satisfiability modulo theories,SMT)确保候选秩函数的有效性;而由SMT返回的反例则进一步用于扩展学习组件中的训练集合,以对候选秩函数进行精化.实验结果表明,所提出的方法比已有的机器学习方法在秩函数的构造效率和构造能力上具有优势.

    Abstract:

    This study proposes a novel approach for synthesizing ranking functions that are expressed as feed-forward neural networks. The approach employs a counter example-guided synthesis procedure, where a learner and a verifier interact to synthesize ranking function. The learner trains a candidate ranking function that satisfies the ranking function conditions over a set of sampled data, and the verifier either ensures the validity of the candidate ranking function or yields counterexamples, which are passed back to further guide the learner. The procedure leverages efficient supervised learning algorithm, while guaranteeing formal soundness via SMT solver. The tool SyntheRF is implemented, then, its scalability and effectiveness are evaluated over a set of benchmark examples.

    参考文献
    [1] Cousot P, Cousot R.An abstract interpretation framework for termination.ACM SIGPLAN Notices, 2012, 47(1):245-258.
    [2] Lee CS, Jones ND, Ben-Amram AM.The size-change principle for program termination.In:Proc.of the 28th ACM SIGPLANSIGACT Symp.on Principles of Programming Languages.2001.81-92.
    [3] Urban C.The abstract domain of segmented ranking functions.In:Proc.of the Int'l Static Analysis Symp.Berlin, Heidelberg:Springer, 2013.43-62.
    [4] Braverman M.Termination of integer linear programs.In:Proc.of the Int'l Conf.on Computer Aided Verification.Berlin, Heidelberg:Springer, 2006.372-385.
    [5] Tiwari A.Termination of linear programs.In:Proc.of the Int'l Conf.on Computer Aided Verification.Berlin, Heidelberg:Springer, 2004.70-82.
    [6] Numbers ONC.With an application to the entschenidugsproblem.1937.
    [7] Colón MA, Sipma HB.Practical methods for proving program termination.In:Proc.of the Int'l Conf.on Computer Aided Verification.Berlin, Heidelberg:Springer, 2002.442-454.
    [8] Podelski A, Rybalchenko A.A complete method for the synthesis of linear ranking functions.In:Proc.of the Int'l Workshop on Verification, Model Checking, and Abstract Interpretation.Berlin, Heidelberg:Springer, 2004.239-251.
    [9] Ben-Amram AM, Genaim S.On multiphase-linear ranking functions.In:Proc.of the Int'l Conf.on Computer Aided Verification.Cham:Springer, 2017:601-620.
    [10] Bradley AR, Manna Z, Sipma HB.The polyranking principle.In:Proc.of the Int'l Colloquium on Automata, Languages, and Programming.Berlin, Heidelberg:Springer, 2005.1349-1361.
    [11] Cook B, See A, Zuleger F.Ramsey vs.lexicographic termination proving.In:Proc.of the Int'l Conf.on Tools and Algorithms for the Construction and Analysis of Systems.Berlin, Heidelberg:Springer, 2013.47-61.
    [12] Urban C.The abstract domain of segmented ranking functions.In:Proc.of the Int'l Static Analysis Symp.Berlin, Heidelberg:Springer, 2013.43-62.
    [13] Chen Y, Xia B, Yang L, et al.Discovering non-linear ranking functions by solving semi-algebraic systems.In:Proc.of the Int'l Colloquium on Theoretical Aspects of Computing.Berlin, Heidelberg:Springer, 2007.34-49.
    [14] Shen L, Wu M, Yang Z, et al.Generating exact nonlinear ranking functions by symbolic-numeric hybrid method.Journal of Systems Science and Complexity, 2013, 26(2):291-301.
    [15] Yuan Y, Li Y.Ranking function detection via SVM:A more general method.Proc.of the IEEE Access, 2019, 7:9971-9979.
    [16] Fan RE, Chang KW, Hsieh CJ, et al.LIBLINEAR:A library for large linear classification.Proc.of the Journal of Machine Learning Research, 2008, 9:1871-1874.
    [17] Li Y, Sun X, Li Y, et al.Synthesizing nested ranking functions for loop programs via SVM.In:Proc.of the Int'l Conf.on Formal Engineering Methods.Cham:Springer, 2019.438-454.https://doi.org/10.1007/978-3-030-32409-4_27
    [18] De Moura L, Bjørner N.Z3:An efficient SMT solver.In:Proc.of the Int'l Conf.on Tools and Algorithms for the Construction and Analysis of Systems.Berlin, Heidelberg:Springer, 2008.337-340.
    [19] Brown CW, Davenport JH.The complexity of quantifier elimination and cylindrical algebraic decomposition.In:Proc.of the 2007 Int'l Symp.on Symbolic and Algebraic Computation (ISSAC 2007).New York:Association for Computing Machinery, 2007.54-60.
    [20] Si X, Dai H, Raghothaman M, et al.Learning loop invariants for program verification.In:Proc.of the of Neural Information Processing Systems.2018.7762-7773.
    [21] Chang YC, Roohi N, Gao S.Neural Lyapunov control.In:Proc.of the 33rd Int'l Conf.on Neural Information Processing Systems.2019.3245-3254.
    [22] Abate A, Ahmed D, Giacobbe M, et al.Formal synthesis of Lyapunov neural networks.Proc.of the IEEE Control Systems Letters, 2020, 5(3):773-778.
    [23] Giacobbe M, Kroening D, Parsert J.Neural termination analysis.arXiv preprint arXiv:2102.03824, 2021.
    [24] Tan W, Li Y.Synthesis of ranking functions via DNN.Proc.of the Neural Computing and Applications, 2021:1-21.https://doi.org/10.1007/s00521-021-05763-8
    [25] Floyd RW.Assigning meanings to programs.In:Proc.of the Symp.in Applied llathematics.1967.
    [26] Cybenko G.Approximations by superpositions of a sigmoidal function.Proc.of the Mathematics of Control, Signals and Systems, 1989, 2:183-192.
    [27] Le TC, Antonopoulos T, Fathololumi P, et al.DynamiTe:Dynamic termination and non-termination proofs.Proc.of the ACM on Programming Languages, 2020, 4(OOPSLA):1-30.
    引证文献
    网友评论
    网友评论
    分享到微博
    发 布
引用本文

林开鹏,梅国泉,林望,丁佐华.基于深度学习和反例制导的循环程序秩函数生成.软件学报,2022,33(8):2918-2929

复制
分享
文章指标
  • 点击次数:1010
  • 下载次数: 3609
  • HTML阅读次数: 2685
  • 引用次数: 0
历史
  • 收稿日期:2021-09-05
  • 最后修改日期:2021-10-14
  • 在线发布日期: 2022-01-28
  • 出版日期: 2022-08-06
文章二维码
友情链接:中国科学院软件研究所中国计算机学会中国科学院国家自然科学基金委员会CCF数字图书馆Int'l J of Softw Info计算机系统应用
您是第19766051位访问者
版权所有：中国科学院软件研究所 京ICP备05046678号-3
地址：北京市海淀区中关村南四街4号,邮政编码：100190
电话：010-62562563 传真：010-62562533 Email：jos@iscas.ac.cn
技术支持：北京勤云科技发展有限公司

京公网安备 11040202500063号