C语言以其对底层机器操控的灵活性，在操作系统、嵌入式软件、底层驱动等要求高效的软件设计领域得到广泛应用。然而出于灵活性和效率的考虑，C语言赋予程序员对计算机完全掌控的能力同时，牺牲了一定的安全性:非法指针解引用、内存泄漏、缓冲区溢出等内存安全问题在C语言程序中尤其突出。　　提高软件的可靠性一直是软件开发过程中所追求的目标之一。程序动态测试、程序静态分析和程序验证是目前确保软件安全质量的主要方法。程序验证作为保证程序正确性的最严格的手段，通过形式化方法对程序的各种性质给出严格的数学证明，从而保证了程序的可靠性;然而程序验证目前还未实现自动化证明，需要大量的人工证明，因此未能在工业界得到广泛的应用。程序动态测试的测试结果依赖于给定的测试集，面对复杂的软件系统测试集很难做到代码的高覆盖率，而且动态测试的成本和风险较高。程序静态分析在程序运行之前对代码进行分析，可以较早并且低成本地发现代码中可能存在的缺陷。　　符号执行技术以其良好的精度控制和代码覆盖率，被广泛用于程序静态分析之中。对一个程序进行分析时，符号执行引擎以模拟真实的程序执行过程的方式，分析程序的数据流和控制流信息，并检查程序执行过程中可能出现的所有状态，得到程序的分析结果。高精度和高覆盖率要求对程序状态描述具体而完备，这会导致符号执行过程中常见的状态爆炸问题，使得符号执行技术的可伸缩性（Scalability）较差。笔者所在项目组基于符号执行技术实现了一个带形状分析功能的C程序分析工具，该工具同样存在路径爆炸、可伸缩性较差的问题，本文的主要工作是设计和实现状态合并功能及其优化，主要贡献有:　　针对带形状分析的符号执行引擎，设计并实现了状态合并的算法，这其中主要的难点在于如何确保状态合并的引入不会造成程序分析结果精度的下降，尤其是在引入形状分析之后，在特定的状态抽象规则之上，如何判定状态是否可以合并，以及合并规则对分析精度的保证。　　根据状态合并在符号执行引擎中的实际效果，考虑约束求解器的求解能力以及求解时间开销，引入了约束求解器求解代价驱动的优化，在LLVM中间代码上实现了精确的数据依赖分析，并根据求解代价的变化，驱动合并操作是否执行，以取得工具整体性能的最优。　　参与ShapeChecker程序分析工具原型系统的实现，该程序分析工具能够自动发现C程序中常见的安全相关的错误，并且支持对单链表、双链表和二叉树等递归定义数据结构的分析。