基于交互式定理证明的并发程序验证工作综述

并发程序与并发系统可以拥有非常高的执行效率和相对串行系统较快的响应速度，在现实中有着非常广泛的应用。但是并发程序与并发系统往往难以保证其实现的正确性，实际应用程序运行中的错误会带来严重的后果。同时，并发程序执行时的不确定性会给其正确性验证带来巨大的困难。在形式化验证方法中，人们可以通过交互式定理证明器严格地对并发程序进行验证。本文对在交互式定理证明中可用于描述并发程序正确性的验证目标进行总结，它们包括霍尔三元组、可线性化、上下文精化和逻辑原子性。交互式定理证明方法中常用程序逻辑对程序进行验证，本文分析了基于并发分离逻辑、依赖保证逻辑、关系霍尔逻辑等理论研究的系列成果与相应形式化方案，并对使用了这些方法的程序验证工具和程序验证成果进行了总结。

A Survey of Interactive Theorem Proving Based Concurrent Program Verifications

Concurrent programs and concurrent systems are usually highly efficient and are widely used in practice. However, concurrent programs and systems are often prone to error, which could bring fatal consequences in real world applications. Moreover, the non-determinism brought by concurrency is a major difficulty in the verification of concurrent programs. But with formal verification, people could use interactive theorem provers to rigorously prove the correctness of a concurrent program. We present several correctness criteria for concurrent programs, which can be verified using interactive theorem proof techniques. They include Hoare triple, linearizability, contextual refinement, and logical atomicity. Researchers usually use program logics to verify programs in an interactive theorem prover. We summarize the usage of concurrent separation logic, rely-guarantee based logic, and relational Hoare logic in concurrent program verifications. We also surveyed existing foundational verification tools and verification results using these techniques.