随着信息技术产业日益蓬勃发展，软件作为信息技术产业的核心与灵魂，已经广泛渗透到社会的各行各业。与此同时，随着软件需求的不断增加，软件系统的规模和复杂性不断提高，软件质量越发难以保证。特别是越来越多应用在航天、国防以及汽车等安全攸关领域的浮点数程序，软件中存在的缺陷可能会造成重大的损失和灾难性的事故。　　符号执行作为一种静态分析技术，它能自动化地根据程序的内部结构来对程序进行快速有效的分析，在现实中分析那些具有高可靠性要求的程序非常实用。然而，尽管符号执行技术日渐成熟，基于符号执行的浮点数程序分析还较少有人研究和探索。本文主要研究的是基于符号执行的浮点数程序静态分析和缺陷检测。根据浮点数程序中的缺陷种类不同，本文的研究工作包括两方面的内容，分别是浮点数程序中一般性缺陷的检测和浮点数程序中特有缺陷的检测。　　首先，在浮点数程序中一般性缺陷的检测方面，我们研究了面向缺陷检测的符号执行引擎的浮点数语义扩充。一般性缺陷指的是程序中的通用缺陷，如值未定义使用，也存在于非浮点数程序中。针对现有的符号执行引擎大多不支持浮点数语义分析的现状，我们探索了如何有效扩充通用符号执行引擎以支持浮点数语义的分析，从而提高检测浮点数程序中一般性缺陷的效率和效益。为达到分析效益和分析代价的平衡，我们为浮点数库函数构造了一个轻量级的抽象模型。此外，为了加快分析，我们为约束求解引入了后验证求解策略。　　其次，在浮点数程序中特有缺陷检测方面，我们主要探索基于符号执行的浮点数异常的检测。浮点数异常作为浮点数程序中最常见的特有缺陷之一，它的特殊性给基于符号执行的静态分析带来了极大的挑战。我们经过观察发现在真实程序中浮点数异常不常出现，变量的值往往会被加以限制来避免浮点数异常的发生。因此，我们可以利用变量的值区间信息来加速异常的检测。基于区间约束传播技术，我们研究了结合符号执行和值区间分析的浮点数异常检测的方法。在符号执行过程中，我们同时分析和维护变量的值区间信息，该信息用于浮点数异常的快速检测。此外，值区间信息还能用于浮点数库函数的建模，有助于消减误报。据我们所知，我们的工作是第一个结合符号执行和值区间分析的浮点数异常检测方法。随后，结合浮点数表示的特性以及浮点数各类异常的特性，我们还探索和初步实现了增强符号执行检测浮点数异常的三值区间分析方法。该方法为每个变量维护三个子区间，在真实程序分析中，既能缓解区间爆炸问题，又能够较好地应用于浮点数异常的检测。