一句话：提出值对称与数据饱和归约，将双重无界分布式一致性系统验证降至小有限状态模型检测，并实现工具 Venus。
分布式一致性协议（如共识）的验证因其进程数与数据域双重无界而十分困难，已有工作仅能将进程无界的 DAB 系统归约为小有限状态模型检测。本文回答双重无界 DAB 系统是否也可归约的问题，并给出肯定答案。作者提出一种新归约，利用值对称与数据饱和概念，将同时具有无界进程和无界数据域的 DAB 系统验证化归为小有限状态系统的模型检测，从而扩展了可自动高效验证的 DAB 系统类。实现工具 Venus，并成功验证联盟区块链仲裁机制、分布式寄存器及简单键值存储等复杂 DAB 系统模型，表明方法可行且高效。
The ubiquity of distributed agreement protocols, such as consensus, has galvanized interest in verification of such protocols as well as applications built on top of them. The complexity and unboundedness of such systems, however, makes their verification onerous in general, and, particularly prohibitive for full automation. An exciting, recent breakthrough reveals that, through careful modeling, it becomes possible to reduce verification of interesting distributed agreement-based (DAB) systems, that are unbounded in the number of processes, to model checking of small, finite-state systems. It is an open question if such reductions are also possible for DAB systems that are doubly-unbounded , in particular, DAB systems that additionally have unbounded data domains. We answer this question in the affirmative in this work thereby broadening the class of DAB systems which can be automatically and efficiently verified. We present a novel reduction which leverages value symmetry and a new notion of data saturation to reduce verification of doubly-unbounded DAB systems to model checking of small, finite-state systems. We develop a tool, Venus, that can efficiently verify sophisticated DAB system models such as the arbitration mechanism for a consortium blockchain, a distributed register, and a simple key-value store.
@article{paperbot2025,
title = {Enabling Bounded Verification of Doubly-Unbounded Distributed Agreement-Based Systems via Bounded Regions},
author = {Christopher Wagner and Nouraldin Jaber and Roopsha Samanta},
journal = {Proceedings of the ACM on Programming Languages},
volume = {7},
number = {OOPSLA1},
year = {2023},
doi = {10.1145/3586033}
}