The Consensus Verifier
What is the Consensus Verifier and how does it work?
The Consensus Verifier is a model checking tool for consensus algorithms formulated in the ConsL language. The cut-off result reported in our CAV 2017 paper allows us to verify these algorithms for a single, small number of processes (5 or 7 for our case studies) and conclude that the verification results hold for an arbitrary number of processes. In addition, the tool applies a sound and complete counter abstraction to exploit the symmetry present in these systems.
- Ognjen Maric, Christoph Sprenger, and David Basin. Cutoff Bounds for Consensus Algorithms. CAV 2017.
Consensus Verifier download
- The sources of the tool including the case studies from the paper are accessible here (GZ, 19 KB).