在交互式的程序验证中,人们希望自动化地获得一些信息来提高证明效率。数据流分析是一类典型的静态程序分析方法。将这些分析方法应用到代码验证中是一个很好的选择。但是现有数据流分析技术相对孤立,无法将其他数据流分析技术的分析结果加以重新利用。并且由于现有数据流分析技术大部分是完全自动化的分析技术,使用者不能够对分析过程进行干预,不能通过一些关键信息来引导数据流分析过程,阻碍了数据流分析技术在代码验证中发挥更大的作用。因此,为了在交互式代码验证过程中充分发挥数据流分析技术的能力,我们应该使数据流分析技术之间能够相互交流,并且允许使用者在关键点上给予人工干预。本文以发挥数据流分析方法在交互式代码验证中的分析能力作为出发点,提出了一套切实可行的方法和平台,用来整合不同的数据流分析技术。本文实现了一个分析工具原型,它将空指针解引用分析技术、整型变量取值范围分析技术、单链表可达性分析技术整合到一起,并允许使用者进行人工干预。我们通过两个案例展示了本文工作的有效性。本文主要解决了如下问题：·如何对各种不同程序性质进行描述。现有的数据流分析技术关注的程序性质各不相同,为了能够更好的实现综合分析能力,我们十分迫切的需要对程序的性质做统一的描述。本文通过对程序性质的深入分析,使用带有递归函数的逻辑公式来表示程序性质。在清晰表达程序的逻辑性质的基础上,工具还维护了各个性质之间的依赖关系,从而更方便用户的理解。·如何使不同的分析技术能够相互利用其它技术的分析结果。在实现了对程序性质的统一描述后,本文确定了以控制流图作为共享的核心数据结构,并通过引入程序点的概念将程序性质以统一的方式进行存贮。工具中还提供了对程序性质进行增删改操作的接口,各个分析技术在分析时可以提取已有程序性质,并在分析完成后回写分析得到的性质,实现了几种不同分析技术共享程序性质的目标。·如何让使用者方便的实现对分析过程的干预。在实现数据流分析工具的交互后,为了使得使用者能够更好地干预和指导数据流分析过程,本文设计了用户与工具间的一些交互功能。在数据流分析过程中,通过用户补充关键信息可以更好地发挥工具的自动化分析能力。