基于深度学习和反例制导的循环程序秩函数生成
作者:
作者单位:

作者简介:

通讯作者:

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

中图分类号:

基金项目:

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


Ranking Function Synthesis for Loop Programs via Counterexample Guided Deep Learning
Author:
Affiliation:

Fund Project:

  • 摘要
  • |
  • 图/表
  • |
  • 访问统计
  • |
  • 参考文献
  • |
  • 相似文献
  • |
  • 引证文献
  • |
  • 资源附件
  • |
  • 文章评论
    摘要:

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

    Abstract:

    In this paper, we propose a novel approach for synthesizing ranking functions that are expressed as feed-forward neural networks. The approach employs a counterexample-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. We implement the tool SyntheRF, then evaluate its scalability and effectiveness over a set of benchmark examples.

    参考文献
    相似文献
    引证文献
引用本文

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

复制
分享
文章指标
  • 点击次数:
  • 下载次数:
  • HTML阅读次数:
  • 引用次数:
历史
  • 收稿日期:2021-09-05
  • 最后修改日期:2021-10-14
  • 录用日期:
  • 在线发布日期: 2022-01-28
  • 出版日期:
您是第位访问者
版权所有:中国科学院软件研究所 京ICP备05046678号-3
地址:北京市海淀区中关村南四街4号,邮政编码:100190
电话:010-62562563 传真:010-62562533 Email:jos@iscas.ac.cn
技术支持:北京勤云科技发展有限公司

京公网安备 11040202500063号