基于动态分析的软件不变量综合技术
作者:
作者单位:

作者简介:

王博(1989-),男,河北邯郸人,博士生,CCF学生会员,主要研究领域为软件测试,缺陷自动修复;卢思睿(1998-),男,学士,CCF学生会员,主要研究领域为软件工程;姜佳君(1992-),男,博士生,CCF学生会员,主要研究领域为软件工程,缺陷修复,程序变换;熊英飞(1982-),男,博士,研究员,博士生导师,CCF专业会员,主要研究领域为软件工程,程序设计语言.

通讯作者:

熊英飞,E-mail:xiongyf@pku.edu.cn

中图分类号:

基金项目:

国家自然科学基金(61922003,61672045)


Survey of Dynamic Analysis Based Program Invariant Synthesis Techniques
Author:
Affiliation:

Fund Project:

National Natural Science Foundation of China (61922003, 61672045)

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

    软件不变量是软件的重要属性,在软件验证、软件调试和软件测试等领域有重要作用.自20世纪末以来,基于动态分析的不变量综合技术成为相关领域的一个研究热点,并且取得了一定的进展.收集了90篇相关论文对该领域进行系统总结.基于动态分析的不变量综合技术是该领域的核心问题,提出了“学习者-预言”框架统一描述相关方法,并且在此框架内根据学习者的归纳方法将综合技术大致分为4类,分别是基于模板穷举的方法、基于数值计算的方法、基于统计学习的方法以及基于符号执行的方法.其次,讨论了基于动态分析综合的不变量在软件验证和软件工程等领域的重要应用.随后,总结不变量生成技术中常用的实验对象程序和开源的不变量综合工具.最后,总结该领域并展望未来的研究方向.

    Abstract:

    Program invariants are important properties of software, which play important roles in many software research fields, such as verification, debugging, and testing. Since the end of 20th century, research on dynamic analysis based program invariant synthesis has become a hot topic in related research areas and made remarkable progress. This paper collects 90 related papers to survey researches within this topic. To dynamically synthesize invariants is the key problem of this field. An abstract framework, “learner-oracle”, is proposed to model and subsume synthesis approaches. In general, the synthesis approaches can be classified into four types, i.e. pattern enumeration based approaches, numerical calculation based approaches, statistical learning based approaches, and symbolic execution based approaches. Furthermore, important applications are discussed of dynamic invariants in software engineering and software verification. Then, important subject programs and synthesis tools are briefly summarized. Finally, the remaining opportunities are presented and a conclusion is reached.

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

王博,卢思睿,姜佳君,熊英飞.基于动态分析的软件不变量综合技术.软件学报,2020,31(6):1681-1702

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

京公网安备 11040202500063号