论文标题
部分可观测时空混沌系统的无模型预测
A Concurrent Program Logic with a Future and History
论文作者
论文摘要
验证细粒度的乐观并发程序仍然是一个空旷的问题。现代程序逻辑提供了抽象机制和组成推理原则，以应对固有的复杂性。但是，它们的使用主要仅限于铅笔和纸或机械化的证明。我们设计了一种针对缺乏自动化的新分离逻辑。虽然已知本地推理对于自动化至关重要，但我们是第一个展示如何保留该位置的（i）在不需要幽灵代码的情况下（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.
