可信软件的相关研究是软件工程领域的一个焦点,如何在软件的开发过程或测试阶段中尽早的发现并消除掉软件缺陷,是构建可信软件的重要途径。软件代码中的缺陷是导致软件故障及漏洞的主要原因,其中静态分析技术是检测代码级缺陷的一种有效方法,但静态分析的结果不可能既是可靠的又是完备的,导致静态缺陷检测出现漏报或误报。对某些高可信软件,需要达到缺陷的零漏报,因此对缺陷进行充分检测的研究非常具有实用价值。空指针引用是一种具有代表性的代码级缺陷,也一直是缺陷检测领域的研究热点之一。虽然目前对空指针引用缺陷检测已有许多相关研究,但对空指针引用进行充分测试依然是难以达到的一个目标。因此,本文对可靠的数据流分析、空指针引用缺陷充分检测中的一系列关键技术问题进行了深入研究,主要工作包括如下内容：(1)可寻址表达式的充分识别。本文将C程序中的可寻址表达式作为静态分析的基本对象,并介绍了基于抽象语法树识别可寻址表达式的方法。首先,归纳总结出了C程序中内存对象与可寻址表达式的语法规则,以及可寻址表达式与抽象语法树上节点的映射关系；其次,介绍了可寻址表达式的命名规则、类型推导及作用域推导规则；最后,介绍了基于抽象语法树充分识别可寻址表达式的方法。(2)应用基于区域的符号化三值逻辑(Region-based Symbolic Three-Valued Logic, RSTVL)描述内存对象的存储状态。RSTVL使用抽象的区域模拟内存对象所分配的内存块,用区域上的符号表达式表示内存对象的取值,用区间域表示符号表达式中的每个符号的取值,并进而将对可寻址表达式的各种操作映射为在区域上的操作。RSTVL作为一种可靠的抽象内存模型,能够描述C程序运行时内存中数据结构的形态信息与内存对象的存储状态,以及可寻址表达式间的各种关联,包括指向关系、层次关系与取值逻辑关系。(3)基于RSTVL的数据流分析。本文提出了一种基于RSTVL的流敏感、域敏感的过程内数据流分析方法,该方法将对可寻址表达式的操作映射到对区域上的操作,可满足对值信息与地址信息的一并分析,进而实现在一个统一的框架下进行数据流分析、指针分析与形态分析。本文重点介绍了对赋值语句、分支语句、循环语句的迁移操作处理,并结合抽象解释理论证明了基于RSTVL的数据流分析对这三类语句迁移操作的可靠性,进而证明了本文数据流分析方法的可靠性。(4)基于符号化函数摘要的过程间数据流分析。本文提出了一种基于符号化函数摘要的域敏感、上下文敏感的过程间数据流分析方法,该方法首先基于过程内数据流分析的结果,应用基于RSTVL描述的符号化函数摘要描述函数的行为,在函数调用点基于调用点处由RSTVL描述的上下文信息对符号化函数摘要进行实例化,实现域敏感、上下文敏感的过程间数据流分析。(5)空指针引用缺陷的充分检测。基于可寻址表达式充分识别的结果,介绍基于抽象语法树充分识别出被引用的指针的方法；为空指针引用缺陷检测的需要,提出了指针指向属性的概念,及基于指针指向属性的指针引用判定规则；为实现过程间空指针引用的缺陷检测,将指向属性未知的指针所关联的外部指针添加到函数摘要的空指针引用缺陷的前置约束中,在函数调用点,基于由RSTVL描述的调用点处上下文信息,获得前置约束中的指针对应的调用点处的空指针引用缺陷检测对象,基于指针引用判定规则实现对过程间空指针引用缺陷的检测。综上所述,本文针对C程序的数据流分析与空指针引用缺陷检测的几个关键性问题进行了研究,取得了一定的理论研究成果。上述技术已经在缺陷检测工具DTSC RSTVL中实现,大量的测试结果表明该工具能够实现对C程序中的空指针引用缺陷实现充分检测。