一句话：提出时间插值证明原则，在并发分离逻辑中自动化后见推理，验证并发数据结构线性一致性。
并发数据结构线性一致性的自动验证仍是难题。本文提出时间插值（temporal interpolation）作为一种新的证明原则，用于在并发分离逻辑中指导基于后见论证（hindsight arguments）的自动证明搜索；它可替代预言变量（prophecy variables），并把证明组织为易于消解的假设。作者进一步将后见理论集成到程序逻辑中，赋予其形式严谨性和互补证明机制。该原则已在工具中实现，并用于自动验证 Logical Ordering tree。该证明因未来依赖的线性化点和复杂结构覆盖而困难，是首个对该数据结构的形式化证明；形式化还揭示了一个未知缺陷，并表明已有非形式证明有误。
Automatically proving linearizability of concurrent data structures remains a key challenge for verification. We present temporal interpolation as a new proof principle to guide automated proof search using hindsight arguments within concurrent separation logic. Temporal interpolation offers an easy-to-automate alternative to prophecy variables and has the advantage of structuring proofs into easy-to-discharge hypotheses. Additionally, we advance hindsight theory by integrating it into a program logic, bringing formal rigor and complementary proof machinery. We substantiate the usefulness of temporal interpolation by implementing it in a tool and using it to automatically verify the Logical Ordering tree. The proof is challenging due to future-dependent linearization points and complex structure overlays. It is the first formal proof of this data structure. Interestingly, our formalization revealed an unknown bug and an existing informal proof as erroneous.
@article{paperbot1944,
title = {Embedding Hindsight Reasoning in Separation Logic},
author = {Roland Meyer and Thomas Wies and Sebastian Wolff},
journal = {Proceedings of the ACM on Programming Languages},
volume = {7},
number = {PLDI},
year = {2023},
doi = {10.1145/3591296}
}