当今计算机技术的发展日新月异,软件在我们的生活中扮演着水和电的重要角色。C语言作为一门广泛应用的语言,已有40多年的历史,它在系统软件如操作系统、编译器、数据库等领域中仍然具着强劲的优势,在保持底层运行效率的同时,它也给程序员带来一些负担,程序员需要关注内存泄露、空指针和悬空指针解引用、缓冲区溢出等问题。目前提高软件可靠性和安全性的方法主要有程序验证、动态测试和静态分析。程序验证目前还未实现完全的自动化证明,动态测试的精确性和覆盖率受到测试集的很大影响,且运行时的检查成本和风险相对较高,静态分析则是比较精确和经济的手段。在静态分析领域中,符号执行被广泛用于测试例的自动生成,它的主要思想是对代码中变量的取值进行符号化,模拟执行程序中所有可能的路径,因此随着程序中的控制结构变得越来越复杂,所需执行的状态数目将急剧增加,严重影响分析工具的伸缩性。针对状态爆炸问题,本文提出了两种在符号执行的不同阶段的优化方法来缓解。第一,使用针对缺陷的程序切片技术对被测程序的中间表示做预处理。首先根据用户关心的缺陷生成源程序的切片准则,然后分析源代码生成数据依赖图和控制依赖图,由两者共同构成程序依赖图,再根据切片准则做程序切片,将源程序规模缩小,最后将切片后的程序交给程序分析工具分析。第二,在符号执行引擎执行过程中对无副作用的控制结构做程序变换。在静态分析工具执行到某个函数时,先分析该函数的所有控制结构,如果某控制结构对程序的后续执行没有影响,则将该控制结构简化,为了不影响分析精度,将工具要检测的缺陷语句提出,这样减少了路径数目,提高了工具的分析性能。笔者所在的课题组目前已实现了一个基于符号执行的C程序静态分析工具,应用本文提出的优化方法,该静态分析工具的分析性能获得了较为明显的改善。