并发分离逻辑族的元理论

Concurrent programs are complicated and they are usually hard to debug. Traditional code review and unit test cannot ensure that a concurrent program is 100% bug free; thus, software developers and software companies need program verification tools to certify program's correctness. In the past decades, concurrent separation logics have become one major theoretical foundation of those verification tools. For now, researchers have designed variant concurrent separation logics for different verification problems. However, these logics are not compatible with each other. New and even more complicated program logics are still needed for more complicated verification problems...In this project, we propose to study concurrent program logics on a higher point of view. Specifically, we aim to develop one unified metatheory for all concurrent separation logics, which have similar proof theories but incompatible semantics. This research project will be especially meaningful for revealing the instinct connection among concurrent separation logics---it is helpful for generalizing theoretic research results from one logic to another; and it is also helpful for deploying different techniques from one verification tool to another.

由于并发程序逻辑复杂且不易调试，传统的人工代码审查和单元测试已无法100%地保证其正确性，因此，人们往往需要寻求程序正确性证明/检验工具的帮助以保障并发程序的正确性。近年来，并发分离逻辑已成为各并发程序正确性证明/检验工具的主要理论基础之一。经过多年发展，学者们已经根据不同的程序证明/检验需求设计了不同的并发分离逻辑。然而，各并发分离逻辑之间并不兼容，现在的学者还需根据更复杂的程序验证需求新程序逻辑。..本项目希望站在更高的视角将并发分离逻辑族作为一个整体进行研究，统一“推理系统高度相似但语义学不兼容”的各并发分离逻辑，提出统一的并发分离逻辑可靠性证明方案，这对揭示各并发分离逻辑之间的内在联系有着重要意义。本项目的研究成果将有助于在各并发分离逻辑中推广某一个特定并发分离逻辑中的理论研究成果，也将为各并发程序正确性证明/检验工具之间的技术移植提供理论依据。

对于大规模软件而言，传统的人工代码审查和单元测试已无法100%地保证程序的正确性。而程序正确性证明/检验技术正是保障程序正确性并向第三方自证程序正确性的重要手段。基于交互式定理证明技术以及程序逻辑理论特别是分离逻辑理论的研究已经成为程序语言与形式化方法领域的热点之一。..本项目侧重研究分离逻辑的元理论，即研究所有分离逻辑的共同性质，挖掘不同分离逻辑之间的理论联系，并基于这些理论研究成果，本项目研究人员对分离逻辑族的元理论在交互式定理证明器Coq中进行了模块化的形式化，并将其运用于程序验证的工具中。