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.

翻译：验证精细的乐观同步程序仍然是一个尚未解决的问题。 现代程序逻辑提供了抽象机制和构思推理原则,以应对内在的复杂性。 但是,它们的使用大多局限于铅笔和纸或机械化的证明。 我们设计了一种新的分离逻辑,以适应缺乏自动化的情况。 虽然已知本地推理对于自动化至关重要,但我们是第一个展示如何保留这个地点的(一) 无需幽灵代码的感应属性推理,和(二) 后视计算历史的推理。 我们在一个工具中应用了我们的新逻辑,并用它自动核实同时存在的搜索结构,这些结构需要感应特性和后视推理,如哈里斯集。