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

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

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.