Bounded Verification of Doubly-Unbounded Distributed Agreement-Based Systems

TL;DR

This paper introduces a symmetry-based reduction technique and a tool called Venus for automatically verifying doubly-unbounded distributed agreement systems, extending the scope of automated verification to more complex models.

Contribution

It demonstrates that verification of doubly-unbounded DAB systems with unbounded data domains is possible through symmetry reduction, broadening the class of verifiable distributed systems.

Findings

Successfully verified complex DAB models using Venus

Extended reduction techniques to systems with unbounded data domains

Enhanced automation in distributed system verification

Abstract

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 for verification of interesting distributed agreement-based (DAB) systems, that are unbounded in the number of processes, to be reduced 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 for models of DAB systems, thereby broadening the class of DAB systems which can be automatically verified. We present a new symmetry-based reduction and develop a tool, Venus, that can efficiently verify sophisticated DAB system models.