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

摘要：

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

关键词：符号执行、静态分析、循环不变式、递归函数

所属期刊栏目：43

分类号：TP311(计算技术、计算机技术)

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

在线出版日期：2016-04-14（万方平台首次上网日期，不代表论文的发表时间）

页数：共6页

页码：193-198