中文摘要：

验证操作易变数据结构的指针程序仍面临很多挑战.数据结构中严重的指针别名显著地复杂化对操作这些结构的程序的推理.为分析和验证操作易变数据结构的指针程序,文中提出了形状图逻辑.形状图是描述程序中静态声明的堆指针变量和动态分配的结构体中指针域变量的指向的一种有向图,能准确表达指针的有效性和指针之间的相等性,可用于判断两个访问表达式是否是别名.形状图逻辑是Hoare逻辑的一种扩展,是一种直接将形状图作为程序中指针断言集的程序逻辑.该文研究形状图的等价理论和蕴含理论以及它们的判定方法和应用.首先,把形状图及其等价规则和蕴含规则分别类比为代数项及其等式规则和重写规则,像研究代数规范的理论那样来研究形状图理论.该文定义了形状图的语法理论和语义理论,定义了形状图重写系统及其终止性、局部合流性和合流性,然后得到基于形状图重写的形状图等价判定和蕴含判定的方法.其次,提出循环不变形状图和递归函数前后形状图的自动推断方法.借助形状图理论的判定方法,该文把一个基于抽象解释的推断循环不变式的一般方法改编成推断循环不变形状图的方法.由于计算终止的递归函数总有非递归的出口,可以先通过非递归路径得到函数的后形状图的初值,然后再在递归路径上迭代求解.从而,可以像推断循环不变形状图那样来推断递归函数的前后形状图.第三,参照Nelson-Oppen框架,提出形状图理论和整数理论组合的一种判定方法.对易变数据结构,除了关心数据结构各节点是否连成预定的形状外,往往还关心数据在这些节点间的排列等特性,它们不能脱离易变数据结构的形状特征而单独验证.为此,所提出的组合判定方法针对这类程序的验证条件的特点,利用程序分析阶段得到的形状图对验证条件的前件中的符号断?

英文摘要：

Programs manipulating mutable data structures present a challenge for verification. Deep aliasing inside data structures dramatically complicates reasoning statements manipulating these structures. To analyze and verify programs manipulating mutable data structures, we proposed the shape graph logic. Shape graphs describe point-to relations of statically declared heap pointer variables and pointer fields of heap objects. They precisely express the validity of pointers and the equalities between pointers, and can be used to judge whether two access expressions are aliases or not. graphs as pointer The shape graph logic is an extension to Hoare logic, which directly uses shape assertions. This paper studies the equivalence theory and implication theory of shape graphs, as well as their decision procedures and applications. First, we investigate the shape graph theory using analogous methods to those in studying the theory of algebraic specification, where shape graphs and their equivalence rules and implication rules are analogous to algebraic terms and their equality rules and rewriting rules, respectively. Analogously, we define the syntactic theory and semantic theory of shape graphs, and then define the shape graph rewriting system as well as its termination, local confluence and confluence. Based on these definitions, we present decision methods on deciding the equality and implication of shape graphs by rewriting shape graphs. Secondly, we propose methods for automatically inferring loop-invariant shape graphs as well as the pre- and post-shape graphs of recursive functions. With the help of the decision procedures for the shape graph theory, the proposed method for inferring loop-invariant shape graphs has been adapted from a general method for inferring loop invariants based on abstract interpretation. Since a terminal recursive function has at least one non-recursive exit, the initial post-shape graphs of the function can be inferred along the non-recursive path, and then post-shape graphs can be iterative