Many techniques for automated inference of inductive invariants for distributed protocols have been developed over the past several years, but their performance can still be unpredictable and their failure modes opaque for large-scale verification tasks. In this paper, we present inductive proof slicing, a new automated, compositional technique for inductive invariant inference that scales effectively to large distributed protocol verification tasks. Our technique is built on a core, novel data structure, the inductive proof graph, which explicitly represents the lemma and action dependencies of an inductive invariant and is built incrementally during the inference procedure, backwards from a target safety property. We present an invariant inference algorithm that integrates localized syntax-guided lemma synthesis routines at nodes of this graph, which are accelerated by computation of localized grammar and state variable slices. Additionally, in the case of failure to produce a complete inductive invariant, maintenance of this proof graph structure allows failures to be localized to small sub-components of this graph, enabling fine-grained failure diagnosis and repair by a user. We evaluate our technique on several complex distributed and concurrent protocols, including a large scale specification of the Raft consensus protocol, which is beyond the capabilities of modern distributed protocol verification tools, and also demonstrate how its interpretability features allow effective diagnosis and repair in cases of initial failure.

翻译：在过去几年中，针对分布式协议归纳不变量的自动推理技术得到了广泛发展，但这些方法在大规模验证任务中仍存在性能不稳定和失败原因不透明的问题。本文提出归纳证明切片——一种新型自动化组合归纳不变量推理技术，可有效扩展至大规模分布式协议验证任务。该技术基于核心创新数据结构"归纳证明图"，通过显式表示归纳不变量的引理与动作依赖关系，并采用从目标安全属性逆向构建的方式，在推理过程中增量生成该图结构。我们提出一种不变量推理算法，在图中各节点集成基于局部语法引导的引理综合例程，并通过局部语法与状态变量切片计算加速该过程。此外，当无法生成完整归纳不变量时，维护该证明图结构可将失败定位至图的微小子组件，使用户能够进行细粒度故障诊断与修复。我们在多个复杂分布式及并发协议上评估该方法，包括超出当前分布式协议验证工具能力范围的大规模Raft共识协议规范，同时展示其可解释性特征如何在初始失败场景下实现有效诊断与修复。