基于动态分析的软件不变量综合技术

来源：软件学报杂志2020年第6期北京时间：

作者：王博，卢思睿，姜佳君，熊英飞

单位：王博，北京大学 信息科学技术学院 计算机科学技术系 软件研究所, 北京 100871;高可信软件技术教育部重点实验室(北京大学), 北京 10087111,卢思睿，北京大学 信息科学技术学院 计算机科学技术系 软件研究所, 北京 100871;高可信软件技术教育部重点实验室(北京大学), 北京 10087102,姜佳君，北京大学 信息科学技术学院 计算机科学技术系 软件研究所, 北京 100871;高可信软件技术教育部重点实验室(北京大学), 北京 10087103,熊英飞，北京大学 信息科学技术学院 计算机科学技术系 软件研究所, 北京 100871;高可信软件技术教育部重点实验室(北京大学), 北京 10087104

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

关键词：不变量|动态分析|软件规约|软件验证|软件测试

基金资助：国家自然科学基金（61922003，61672045）