A. Parosh, F. Abdulla, L. Haziza, and . Holík, Parameterized verification through view abstraction, STTT, vol.18, issue.5, pp.495-516, 2016.

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

Z. Bar, -. , and M. Ben-or, A tight lower bound for randomized synchronous consensus, Proceedings of the seventeenth annual ACM symposium on Principles of distributed computing, pp.193-199, 1998.

S. Bardin, A. Finkel, J. Leroux, and L. Petrucci, Fast: acceleration from theory to practice, STTT, vol.10, issue.5, pp.401-424, 2008.
URL : https://hal.archives-ouvertes.fr/hal-00345968

M. Biely, B. Charron-bost, A. Gaillard, M. Hutle, A. Schiper et al., Tolerating corrupted communication, PODC, pp.244-253, 2007.

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

R. Bloem, S. Jacobs, A. Khalimov, I. Konnov, S. Rubin et al., Decidability of Parameterized Verification, Synthesis Lectures on Distributed Computing Theory, 2015.
DOI : 10.2200/s00658ed1v01y201508dct013

A. Bouajjani, M. Emmi, C. Enea, and J. Hamza, On reducing linearizability to state reachability, ICALP, pp.95-107, 2015.
DOI : 10.1007/978-3-662-47666-6_8
URL : http://arxiv.org/pdf/1502.06882

B. Charron, -. , and A. Schiper, The heard-of model: computing in distributed systems with benign faults, Distributed Computing, vol.22, issue.1, pp.49-71, 2009.

H. Comon and Y. Jurski, Multiple counters automata, safety analysis and Presburger arithmetic, CAV, pp.268-279, 1998.
DOI : 10.1007/bfb0028751
URL : http://www.lsv.ens-cachan.fr/Publis/PAPERS/ComJur-cav98.ps

G. Delzanno, A unified view of parameterized verification of abstract models of broadcast communication, STTT, vol.18, issue.5, pp.475-493, 2016.

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

A. Durand-gasselin, J. Esparza, P. Ganty, and R. Majumdar, Model checking parameterized asynchronous shared-memory systems, Formal Methods in System Design, vol.50, issue.2-3, pp.140-167, 2017.
DOI : 10.1007/978-3-319-21690-4_5
URL : http://arxiv.org/pdf/1505.06588

C. Dwork, N. Lynch, and L. Stockmeyer, Consensus in the presence of partial synchrony, J. ACM, vol.35, issue.2, pp.288-323, 1988.

E. A. Emerson and K. S. Namjoshi, Reasoning about rings, POPL, pp.85-94, 1995.
DOI : 10.1145/199448.199468

J. Esparza, Petri nets, commutative context-free grammars, and basic parallel processes, Fundam. Inform, vol.31, issue.1, pp.13-25, 1997.
DOI : 10.1007/3-540-60249-6_54
URL : http://wwwbrauer.informatik.tu-muenchen.de/gruppen/theorie/publications/ftp/esparza/FUND.ps.gz

A. Farzan, Z. Kincaid, and A. Podelski, Proving liveness of parameterized programs, LICS, pp.185-196, 2016.
DOI : 10.1145/2933575.2935310
URL : http://arxiv.org/pdf/1605.02350

L. Fribourg and H. Olsén, A decompositional approach for computing least fixedpoints of datalog programs with z-counters, Constraints, vol.2, issue.3/4, pp.305-335, 1997.

Z. Ganjei, A. Rezine, P. Eles, and Z. Peng, Counting dynamically synchronizing processes, STTT, vol.18, issue.5, pp.517-534, 2016.
DOI : 10.1007/s10009-015-0411-0
URL : http://liu.diva-portal.org/smash/get/diva2:898584/FULLTEXT01

O. H. Ibarra, Reversal-bounded multicounter machines and their decision problems, J. ACM, vol.25, issue.1, pp.116-133, 1978.
DOI : 10.1145/322047.322058

I. Konnov, M. Lazi?, H. Veith, and J. Widder, Para 2 : Parameterized path reduction, acceleration, and SMT for reachability in threshold-guarded distributed algorithms. Formal Methods in System Design, 2017.
DOI : 10.1007/978-3-319-21690-4_6

J. Kukovec, I. Konnov, and J. Widder, , vol.19, p.17

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

I. Konnov, H. Veith, and J. Widder, On the completeness of bounded model checking for threshold-based distributed algorithms: Reachability, CONCUR, vol.8704, pp.125-140, 2014.

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

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

I. Konnov, J. Widder, F. Spegni, and L. Spalazzi, Accuracy of message counting abstraction in fault-tolerant distributed algorithms, VMCAI, pp.347-366, 2017.

J. Kukovec, Generalizing threshold automata for reachability in parameterized systems, 2016.

L. Lamport, The part-time parliament, ACM Trans. Comput. Syst, vol.16, issue.2, pp.133-169, 1998.
DOI : 10.1145/279227.279229

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

J. Leroux and G. Sutre, Flat counter automata almost everywhere! In ATVA, vol.5, pp.489-503, 2005.
DOI : 10.1007/11562948_36
URL : http://hal.archives-ouvertes.fr/docs/00/34/63/10/PDF/LerouxSutre-ATVA05.pdf

O. Maric, C. Sprenger, and D. A. Basin, Cutoff bounds for consensus algorithms, CAV, Part II, pp.217-237, 2017.

. Marvin-l-minsky, Computation: finite and infinite machines, 1967.

I. Moraru, D. G. Andersen, and M. Kaminsky, There is more consensus in egalitarian parliaments, SOSP, pp.358-372, 2013.
DOI : 10.1145/2517349.2517350
URL : http://dl.acm.org/ft_gateway.cfm?id=2517350&type=pdf

M. Brian, B. Oki, and . Liskov, Viewstamped replication: A general primary copy, PODC, pp.8-17, 1988.