随着计算机技术应用的日益普及,软件系统的规模和复杂性急剧增大,软件在越来越多的系统中成为主要的组成部分。在安全攸关的应用领域,软件系统的可靠性至关重要,这些软件的失效将导致灾难性的后果。因此,验证程序的正确性是非常必要的。然而,对程序的人工验证通常是枯燥、困难的。因此,提高程序验证的自动化程度、减少人工依赖是软件验证中的重要研究内容。程序中常常对复杂数据结构进行操作。典型的复杂数据结构包括数组、链表、图、甚至递归的数据结构等。验证这类程序的正确性需要分析和使用数据结构(及其中的元素)具有的性质。然而,自动/半自动地对这类程序进行推理和验证是一个很有挑战的问题:首先,它们具有复杂的语义;其次,程序中复杂数据结构的大小可以非常大甚至未知,这意味着非常大数量或者未知数量的变量。本文基于数据流分析/逻辑推理等技术针对复杂数据结构程序的分析和验证问题展开研究,在提高验证的自动化程度方面取得以下结果:●提出了一种自动化地发现数组程序中全称量词不变式的方法。数组大小可以非常大甚至未知,因此验证数组程序经常需要使用和处理全称量词性质。该方法能够分析按照特定顺序访问一维或者多维数组的程序,然后合成不变式。该方法将性质(包括全称量词性质和原子性质)集合作为抽象域,通过前向迭代数据流分析合成数组性质。我们证明了该方法的正确性和收敛性。该方法具有相当的灵活性,它可以通过扩展传播规则来发现更多更准确的全称量词不变式。我们开发了一个原型工具。该工具在各种数组程序(包括Competition on Software Verification中的array-examples benchmark)上的实验展示了方法的可行性和有效性。●提出了一个利用不包含量词的性质分析发现数组和链表程序中量词(全称和存在量词)和析取不变式的框架。该框架能够将不包含量词的抽象域提升到包含了量词(全称和存在量词)和析取运算的抽象域。人们已经研究设计了很多不包含量词的抽象域,这个框架可以利用它们来发现更加复杂的性质。我们证明了框架的正确性和收敛性。各种实验展示(包括Linux操作系统的字符串库函数Linux/lib/string.c中的真实程序)方法的可行性和有效性。●提出了一个交互式迭代数据流分析框架。该框架扩展了一般的迭代数据流分析框架。通过程序点上的逻辑公式,多种数据流分析技术、验证技术和用户之间可以进行协作交互。该框架可以与程序验证相结合,提高程序验证的自动化程度,同时提高分析的精度。框架中的各种数据流分析可以交互,可以容易地将若干数据流分析组合成一个新的分析,从而提高分析精度。该框架可以与用户交互,从而获取必要的性质并产生更加精确的结果。考虑到了用户给出的信息可能出错的情况,我们给出两个解决方案:冲突检测和构建依赖关系。我们基于该框架实现了元素属于,容器相交,容器内互异分析。这些分析相互依赖,他们之间需要交互才能产生更精确的结果。这些分析展示了框架的可行性。●针对一些更复杂的数据结构程序(如图程序等),提出了利用抽象程序辅助证明具体程序的方法。抽象程序指使用抽象数据结构(Abstract Data Type)如set、list、map及其上的操作的程序。具体程序即用程序设计语言编写的程序,比如C语言程序。利用抽象程序,该方法将具体程序的证明分成两步:首先证明抽象程序满足规约;然后证明具体程序和抽象程序满足一致性。抽象程序和具体程序一致性证明需要用户给出抽象变量和具体变量的关系,抽象程序程序点和具体程序程序点的对应关系。基于这些对应关系,抽象程序和具体程序一致性证明可以分解,从而容易并可能被自动化证明工具处理。