Scalable, Interpretable Distributed Protocol Verification by Inductive Proof Slicing

过去几年中，已经开发了许多自动推理归纳不变量的技术用于分布式协议，但是它们的性能仍然不可预测，而且在大规模验证任务中它们的失败模式不透明。本文提出了归纳证明分割技术，这是一种新的自动组合技术，用于归纳不变量推理，可以有效地应用于大规模分布式协议验证任务。我们的技术基于核心的、新颖的数据结构——归纳证明图，它明确地表示归纳不变量的引理和动作依赖关系，并在推理过程中从目标安全属性向后增量构建。我们提出了一种不变量推理算法，它在这个图的节点上集成了本地化的语法引导引理综合例程，并通过计算本地化的语法和状态变量切片来加速。此外，如果无法生成完整的归纳不变量，维护这个证明图结构可以将故障定位到这个图的小子组件，使用户能够进行精细的故障诊断和修复。我们在几个复杂的分布式和并发协议上评估了我们的技术，包括Raft一致性协议的大规模规范，这超出了现代分布式协议验证工具的能力，并展示了它的可解释性特征如何在初始失败的情况下进行有效的诊断和修复。

论文旨在提出一种新的自动化、组合的技术，称为归纳证明切片，用于归纳不变量推理，并能有效地扩展到大规模分布式协议验证任务中。

论文的关键思路是建立归纳证明图这一核心数据结构，它能够显式地表示归纳不变量的引理和行动依赖，并在推理过程中逐步构建。同时，该论文还将局部语法引导引理综合例程集成到该图的节点中，并通过计算局部语法和状态变量切片来加速。

该论文的亮点包括：1. 提出了一种新的技术——归纳证明切片，能够有效地扩展到大规模分布式协议验证任务中；2. 建立了归纳证明图这一核心数据结构，能够显式地表示归纳不变量的引理和行动依赖；3. 在几个复杂的分布式和并发协议上进行了评估，包括Raft共识协议的大规模规范；4. 该技术具有解释性特征，能够有效地诊断和修复失败。

最近在该领域中的相关研究包括：1. Automated Invariant Inference for Distributed Programs Using Abstraction and Symmetry; 2. Automated Invariant Generation for Weakly Consistent Transactions via Conflict Serializability; 3. Compositional Verification of Distributed Systems with Mechanized Proof Assistants.