堆内存为现代计算机软件提供了灵活方便、功能强大的支持,在类C的编程语言中,程序员大量采用递归数据结构操作堆内存。其中,链表是进行堆内存操作时最经常采用的数据结构之一,在操作系统内核代码及驱动程序编写中广泛应用。但包括链表、二叉树在内的递归数据结构形态复杂多变,且指向这些数据结构的指针使用灵活,这使得堆内存相关操作成为计算机软件中最常见的错误来源之一[1]。形式化分析验证是排除错误、构建可信软件的重要途径,对于航空航天、国防军事、金融交通等安全关键应用尤为重要。然而递归数据结构的大量使用对堆操作程序的分析验证提出了更多的挑战,其抽象模型成为堆操作程序分析验证的一个关键因素。本文针对链表研究了递归数据结构的抽象模型以及堆操作程序分析验证相关技术。主要工作包括:1)提出了一种新的链表抽象模型。该抽象模型采用了一种紧致的链表抽象状态表示方法,并隐式存储链表结点之间的边信息,存储开销较低;模型中同时维护了链表的形态性质与数量性质,精确度较高。文中首先定义了带计数的变量可达向量集,将其作为单向无环链表的抽象模型,然后通过引入“切断”操作以及环扩展标记位,建立了适应于所有单向链表的抽象模型,最后通过为两个链表域分别维护一个带计数的变量可达向量集,以及引入操作良构性限制,建立了双向链表的抽象模型。最后,在符号执行框架中进行了实验,实验结果证明该抽象模型可用于分析验证堆操作程序的各种可信性质。2)设计实现了一个面向堆操作程序数量性质的符号化数值抽象框架。该框架可以将堆操作程序转换成保持数量性质的纯数值程序,避免了形态分析与数值推理融合导致问题复杂度急剧上升的问题。文中基于新提出的链表抽象模型对该框架进行了例化,并基于符号执行技术设计实现了数量形态分析过程,生成核心中间表示——抽象状态迁移图,然后基于程序切片的思想针对指定性质获得数值抽象,最后通过已有的数值推理工具分析验证该性质是否成立。本文基于该框架设计实现了一个原型工具,并对若干重要链表操作程序进行实验,实验结果证明了框架的正确性与有效性。3)基于本文中的链表抽象模型,给出了链表形态数量抽象域。该抽象域可以用于生成形态性质与数量性质结合的不变式,而这些不变式对分析验证堆操作程序至关重要。文中结合区间抽象域与仿射等式抽象域构建了基本的抽象域表示,定义了相关域操作,给出了基本链表操作对应的状态迁移函数。实际分析结果证明该抽象域发现的不变式较强,能够很好地支持堆操作程序分析与验证。4)设计并实现了两个堆内存上界分析工具原型。首先基于文中给出的堆操作程序符号化数值抽象框架,设计实现了一个链表操作程序堆内存上界分析工具。通过在抽象状态迁移图中插桩维护堆内存使用量的语句,获取对应的数值抽象模型,将堆内存上界问题转换成数值程序中的最大值问题。其次,基于符号执行工具KLEE设计实现了一个实用的堆内存上界分析工具,并针对堆内存上界问题的特性设计了循环特殊处理策略,能够分析符号值大小的堆内存分配以及循环次数为符号值的循环。实验结果表明这两个原型工具可以针对很多实际程序给出较精确的堆内存上界。