随着软件技术的普及发展,软件系统被应用到我们生活的各个方面,在带来极大便利的同时我们也承受着由软件漏洞所带来的巨大风险。如何有效的保证软件质量是一个极为迫切的需求。在保证软件质量的方法中有两大类,前期可以通过静态分析源代码尽早发现潜在漏洞;后期可以动态运行二进制代码分析实际运行结果。程序的漏洞越早发现其修改成本越小,所以程序静态分析是一种重要的软件质量保证方法。在众多的静态分析方法中,符号执行以其高度的精确性获得了极大关注。符号执行是一种路径敏感上下文相关的分析方法,在计算资源足够充分的情况下它可以对程序进行非常精确地分析,从而发现一些细微的漏洞。然而符号执行理论本身也面临着几大难题,其中包括路径爆炸、约束求解和内存模型。论文首先对近三十年来符号执行技术的发展进行了概述,讨论了符号执行的基本原理和近年提出的一些改进方法。这些改进包括:在测试数据生成方面提出了动态符号执行,它是一种结合具体值和符号值的方法;在路径爆炸抑制方面提出一些启发式搜索策略;在约束求解方面主要提出了无关约束消除和增量式求解。本文紧接着分析讨论了一种非常强大的中间语言LLVM IR,对其语法构成、数据类型及指令集做了分析,并对其数据类型和指令集进行了形式化描述。本文随后对符号执行中内存模型展开了讨论,对比了当下符号执行理论中各种主流内存模型(名字值模型、数组模型和基于区域的三元组模型)的优缺点,并提出一种树状结构的内存模型TMM(Tree-memory model)。这种内存模型的核心思想是以树状结构来表示那些嵌套数据。该内存模型能够有效的解决内存模型理论中类型转换、指针与别名和大小不确定数据等难题。本文最后以LLVM IR指令集的一个核心子集和TMM内存模型为基础并集成SMT求解器Z3,实现了一个简单的符号执行引擎SSE(Simple symbolic execution engine),并通过实验验证了SSE和TMM的有效性和先进性。