QuickSilver: A Modeling and Parameterized Verification Framework for Systems with Distributed Agreement.

Fully-automated parameterized verification of distributed systems, i.e., verification of systems instantiated with an arbitrary number of processes, suffers from scalability challenges, even when it is decidable. This paper seeks to push the boundaries of parameterized verification in the types of systems that can be verified automatically as well as practically, by incorporating abstractions into the verification pipeline. We develop a framework---QuickSilver---for modeling and automated parameterized reasoning about systems that build on distributed agreement protocols, such as consensus or leader election. QuickSilver includes a modeling language, Mercury, with primitives for abstracting distributed agreement, syntactic conditions for decidable and practical parameterized verification of systems modeled in Mercury, and an implementation that has been demonstrably used for efficient, automated parameterized verification of several benchmarks.