The Consensus Verifier

Main content

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.

Related publications  

  • 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).

 

 
 
Page URL: http://www.infsec.ethz.ch/research/software/consl-verifier.html
Tue Jun 27 14:01:22 CEST 2017
© 2017 Eidgenössische Technische Hochschule Zürich