Many fault-tolerant distributed algorithms are designed for synchronous or round-based semantics. In this work, we introduce the synchronous variant of threshold automata, study their applicability and limitations for the verification of synchronous distributed algorithms.

We show that many synchronous fault-tolerant distributed algorithms have a bounded diameter, although the algorithms are parameterized by the number of processes. Hence, we use bounded model checking for verifying these algorithms.

We compute the diameter of several algorithms and check their safety properties, using SMT queries that contain quantifiers for dealing with the parameters symbolically. Surprisingly, the performance of SMT solvers on these queries is very good, reflecting recent progress in dealing with quantified queries. We found that the diameter bounds of synchronous algorithms in the literature are tiny (from 1 to 4), which makes our approach applicable in practice. For a class of algorithms we establish a theoretical result on the existence of a diameter, providing a first explanation for our experiments.