动态数据结构的形状性质与数据约束：基于分离逻辑的自动分析与验证

The correctness of computer software is vital for the smooth operation of information society. Since dynamic data structures are widely used in fundamental software codes, ensuring the correctness of programs with dynamic data structures is critical for the correctness of software systems.Separation logic is an extension of Hoare logic proposed around the year 2000, with the virtue of the local reasoning of the properties of programs with dynamic data structures. Separation logic has become a research hotpot of the program analysis and verification field in the last decades. Although most of the known work of separation logic focuses on shape properties (topology), the scalar data stored in the cells are also essential for the behavior of programs. The goal of this project is to analyze and verify automatically both shape properties and data constraints of programs with dynamic data structures. At first, we plan to extend separation logic with data constraints, and identify the fragments which achieve a good balance between expressiveness and decidability/complexity. Then, we consider to establish a framework of abstract interpretation by taking as the abstract domain the set of formulas in the identified decidable fragments, in order to analyze and verify automatically the behavior of programs. Meanwhile, we plan to investigate the integration of abstract interpretation with abstraction and refinement technique, as well as consider the modular verification of the programs containing procedure calls.

计算机软件的正确性对于保证信息社会的正常运行至关重要。动态数据结构在各种基础软件代码中被广泛使用，保证具有动态数据结构的程序的正确性对于保证软件的正确性非常关键。分离逻辑是2000年左右由研究人员提出的Hoare逻辑的一种扩展，其优点是可以对具有动态数据结构的程序的行为进行局部化的推理。分离逻辑近十年来成为程序分析与验证领域的一个研究热点。虽然分离逻辑已有的大部分工作集中在形状性质（拓扑结构）方面，但程序的行为也与存储单元中的标量数据密切相关。本项目拟基于分离逻辑对含有动态数据结构的程序的形状性质与数据约束同时进行自动的分析与验证。首先我们对分离逻辑进行扩展以包含数据约束，寻找在表达能力与可判定性/复杂性方面取得良好平衡的子集。然后，以得到的可判定子集的公式集为抽象域，建立抽象解释的框架来对程序进行自动的分析与验证。同时，考虑引入抽象求精技术，并探讨对含有过程调用的程序进行模块化的验证。

计算机软件的正确性对于保证信息社会的正常运行至关重要。动态数据结构在各种基础软件代码中被广泛使用，保证具有动态数据结构的程序的正确性对于保证软件的正确性非常关键。.分离逻辑是2000年左右由研究人员提出的Hoare逻辑的一种扩展，其优点是可以对具有动态数据结构的程序的行为进行局部化的推理。分离逻辑近十年来成为程序分析与验证领域的一个研究热点。虽然分离逻辑已有的大部分工作集中在形状性质（拓扑结构）方面，但程序的行为也与存储单元中的标量数据密切相关。本项目基于分离逻辑对含有动态数据结构的程序的形状性质与数据约束同时进行自动的分析与验证。.首先，我们寻找能描述数据约束的、在表达能力与可判定性/复杂性方面取得良好平衡的分离逻辑的子集，取得了以下成果：.-- 我们探讨了分离逻辑蕴涵问题证明过程中的引理自动生成问题，提出了分离逻辑的可组合归纳谓词的概念，从而大大简化了分离逻辑公式的蕴涵问题的求解.-- 我们提出了可以描述线性数据结构的算术数据约束和集合数据约束的含有线性可组合归纳谓词的分离逻辑的子集，设计了其可满足性问题和蕴涵问题的判定算法，并实现了分离逻辑求解器COMPSPEN，并参加了分离逻辑求解器竞赛SL-COMP 2018；.-- 我们为树结构上的分离逻辑的带算术数据约束扩展的子集基于自动机理论设计了判定算法；.-- 我们证明了含有双链表片段的分离逻辑子集的可满足性问题是NP完全的，而Cook等人关于单链表片段的分离逻辑子集的多项式可解性结果可以扩展到树结构上。.而且，我们以得到的可判定子集的公式集为抽象域，初步建立了抽象解释的框架来对程序进行自动的分析与验证。