P. A. Abdulla, K. Cerans, B. Jonsson, and Y. Tsay, General decidability theorems for infinite-state systems, LICS, pp.313-321, 1996.

B. Aminof, S. Rubin, I. Stoilkovska, J. Widder, and F. Zuleger, Parameterized model checking of synchronous distributed algorithms by abstraction, Verification, Model Checking, and Abstract Interpretation, vol.10747, pp.1-24, 2018.

B. Aminof, S. Rubin, F. Zuleger, and F. Spegni, Liveness of parameterized timed networks, ICALP 2015, vol.9135, pp.375-387, 2015.

H. Attiya and J. Welch, Distributed Computing, 2004.

S. Bardin, J. Leroux, and G. Point, FAST extended release, CAV 2006, vol.4144, pp.63-66, 2006.
URL : https://hal.archives-ouvertes.fr/hal-00344195

C. Barrett, CAV 2011, vol.6806, pp.171-177, 2011.

P. Berman, J. A. Garay, and K. J. Perry, Asymptotically optimal distributed consensus, 1989.

P. Berman, J. A. Garay, and K. J. Perry, Towards optimal distributed consensus, pp.410-415, 1989.

M. Biely, U. Schmid, and B. Weiss, Synchronous consensus under hybrid process and link failures, Theor. Comput. Sci, vol.412, issue.40, pp.5602-5630, 2011.

A. Biere, A. Cimatti, E. M. Clarke, and Y. Zhu, Symbolic model checking without BDDs, TACAS 1999, vol.1579, pp.193-207

, , 1999.

R. Bloem, Decidability of Parameterized Verification. Synthesis Lectures on Distributed Computing Theory, 2015.

S. Chaudhuri, M. Herlihy, N. A. Lynch, and M. R. Tuttle, Tight bounds for k-set agreement, J. ACM, vol.47, issue.5, pp.912-943, 2000.

E. M. Clarke, D. Kroening, J. Ouaknine, and O. Strichman, Completeness and complexity of bounded model checking, 2004.

, LNCS, vol.2937, pp.85-96, 2004.

C. Dr?goi, T. A. Henzinger, H. Veith, J. Widder, and D. Zufferey, A logic-based framework for verifying consensus algorithms, VMCAI 2014, vol.8318, pp.161-181, 2014.

E. A. Emerson and K. S. Namjoshi, Automatic verification of parameterized synchronous systems, CAV 1996, vol.1102, pp.87-98, 1996.

E. A. Emerson and K. S. Namjoshi, On reasoning about rings, Int. J. Found. Comput. Sci, vol.14, issue.4, pp.527-550, 2003.

M. J. Fischer, N. A. Lynch, and M. S. Paterson, Impossibility of distributed consensus with one faulty process, J. ACM, vol.32, issue.2, pp.374-382, 1985.

I. Konnov, M. Lazi?, H. Veith, and J. Widder, A short counterexample property for safety and liveness verification of fault-tolerant distributed algorithms, pp.719-734, 2017.

I. Konnov, H. Veith, and J. Widder, SMT and POR beat counter abstraction: parameterized model checking of threshold-based distributed algorithms, CAV 2015, vol.9206, pp.85-102, 2015.

I. V. Konnov, H. Veith, and J. Widder, On the completeness of bounded model checking for threshold-based distributed algorithms: reachability, Inf. Comput, vol.252, pp.95-109, 2017.

D. Kroening, O. Strichman, L. D. Zuck, P. C. Attie, and A. Cortesi, Efficient computation of recurrence diameters, VMCAI 2003, vol.2575, pp.298-309, 2003.

J. Kukovec, I. Konnov, and J. Widder, Reachability in parameterized systems: all flavors of threshold automata, CONCUR, pp, vol.19, p.17, 2018.
URL : https://hal.archives-ouvertes.fr/hal-01871142

M. Lazi?, I. Konnov, J. Widder, and R. Bloem, Synthesis of distributed algorithms with parameterized threshold guards, OPODIS. LIPIcs, vol.95, p.20, 2017.

J. Leroux and G. Sutre, Flat counter automata almost everywhere!, ATVA 2005, vol.3707, pp.489-503, 2005.
URL : https://hal.archives-ouvertes.fr/hal-00346310

N. Lynch, Distributed Algorithms, 1996.

O. Mari?, C. Sprenger, and D. A. Basin, Cutoff bounds for consensus algorithms, CAV 2017, vol.10427, pp.217-237

, , 2017.

M. L. Minsky, Computation: Finite and Infinite Machines, 1967.

L. De-moura and N. Bjørner, Z3: an efficient SMT solver, TACAS 2008, vol.4963, pp.337-340, 2008.

M. Raynal, Fault-Tolerant Agreement in Synchronous Message-Passing Systems, Synthesis Lectures on Distributed Computing Theory, 2010.
URL : https://hal.archives-ouvertes.fr/inria-00543049

T. K. Srikanth and S. Toueg, Optimal clock synchronization, J. ACM, vol.34, issue.3, pp.626-645, 1987.

T. Srikanth and S. Toueg, Simulating authenticated broadcasts to derive simple faulttolerant algorithms, Distrib. Comput, vol.2, pp.80-94, 1987.

I. Stoilkovska, I. Konnov, J. Widder, and F. Zuleger, Artifact and instructions to generate experimental results for TACAS 2019 paper: Verifying Safety of Synchronous Fault-Tolerant Algorithms by Bounded Model Checking (artifact), 2019.