ByMC: Byzantine Model Checker.

In recent work [10, 12], we have introduced a technique for automatic verification of threshold-guarded distributed algorithms that have the following features: (1) up to t of processes may crash or behave Byzantine; (2) the correct processes count messages and progress when they receive sufficiently many messages, e.g., at least (t+1); (3) the number n of processes in the system is a parameter, as well as t; (4) and the parameters are restricted by a resilience condition, e.g., (n u003e 3t).