一句话：提出面向细粒度乐观并发程序的分离逻辑，支持无需幽灵代码的归纳性质与事后历史推理，并实现自动化验证。
细粒度乐观并发程序的验证仍是难题；现有程序逻辑虽提供抽象与组合推理，但多用于纸笔或机器化证明，缺乏自动化。本文提出一种新的分离逻辑，旨在弥补自动化缺口。作者首次在保持局部推理的同时，支持（i）无需幽灵代码推理归纳性质，以及（ii）事后推理计算历史。该逻辑已实现为工具，并自动验证了需要归纳性质与事后推理的挑战性并发搜索结构，如 Harris 集合。
Verifying fine-grained optimistic concurrent programs remains an open problem. Modern program logics provide abstraction mechanisms and compositional reasoning principles to deal with the inherent complexity. However, their use is mostly confined to pencil-and-paper or mechanized proofs. We devise a new separation logic geared towards the lacking automation. While local reasoning is known to be crucial for automation, we are the first to show how to retain this locality for (i) reasoning about inductive properties without the need for ghost code, and (ii) reasoning about computation histories in hindsight. We implemented our new logic in a tool and used it to automatically verify challenging concurrent search structures that require inductive properties and hindsight reasoning, such as the Harris set.
@article{paperbot1468,
title = {A concurrent program logic with a future and history},
author = {Roland Meyer and Thomas Wies and Sebastian Wolff},
journal = {Proceedings of the ACM on Programming Languages},
volume = {6},
number = {OOPSLA2},
year = {2022},
doi = {10.1145/3563337}
}