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.