支持形状分析的符号执行引擎的设计与实现

作     者：梁家彪 李兆鹏 朱玲 沈咸飞 LIANG Jia-biao;LI Zhao-peng;ZHU Ling;SHEN Xian-fei

作者机构：中国科学技术大学计算机科学与技术学院合肥230026 中国科学技术大学先进技术研究院中国科大-国创高可信软件工程中心合肥230027 

基　　金：国家自然科学基金面上项目(61170018)资助 

出 版 物：《计算机科学》 (Computer Science)

年 卷 期：2016年第43卷第3期

页      码：193-198页

摘      要：目前提高软件可靠性的方法有3种:动态测试、静态分析和程序验证。动态测试的结果依赖于测试集的设计,误报率低,漏报率高,分析结果不稳定。程序验证可以对程序的各种性质进行完备的验证。但目前程序验证通常都需要手动证明,分析成本最高。而程序静态分析可以更早、更全面、较高效和低成本地检测到程序中的缺陷。其中符号执行技术是一种比较有应用前景的静态分析技术,可以很好地控制精确度。针对符号执行可伸缩性差和容易产生路径爆炸的问题,在符号执行过程中利用形状分析技术实现自动推导循环不变式和构建函数行为规范,实现了一个较为实用的C程序分析工具。

主 题 词：符号执行 静态分析 循环不变式 递归函数 

学科分类：08[工学] 0835[0835] 081202[081202] 0812[工学-测绘类] 

D　O　I：10.11896/j.issn.1002-137X.2016.3.036

馆 藏 号：203397825...