M. Aguilera and S. Toueg, The correctness proof of Ben-Or's randomized consensus algorithm, Distributed Computing, pp.1-11, 2012.

C. Baier and J. P. Katoen, Principles of model checking, 2008.

M. Ben-or, Another advantage of free choice: Completely asynchronous agreement protocols (extended abstract), In: PODC. pp, pp.27-30, 1983.

N. Bertrand and P. Fournier, Parameterized verification of many identical probabilistic timed processes, FSTTCS. LIPIcs, vol.24, pp.501-513, 2013.
URL : https://hal.archives-ouvertes.fr/hal-00914263

G. Bracha, Asynchronous byzantine agreement protocols, Inf. Comput, vol.75, issue.2, pp.130-143, 1987.

T. Elrad and N. Francez, Decomposition of distributed programs into communicationclosed layers, Sci. Comput. Program, vol.2, issue.3, pp.155-173, 1982.

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. Lazic, 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, vol.51, issue.2, pp.270-307, 2017.

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

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 and J. Widder, Bymc: Byzantine model checker, ISoLA (3), vol.11246, pp.327-342, 2018.
URL : https://hal.archives-ouvertes.fr/hal-01909653

M. Z. Kwiatkowska and G. Norman, Verifying randomized byzantine agreement, pp.194-209, 2002.

M. Z. Kwiatkowska, G. Norman, and D. Parker, PRISM 4.0: Verification of probabilistic real-time systems, CAV. pp, pp.585-591, 2011.
URL : https://hal.archives-ouvertes.fr/hal-00648035

M. Z. Kwiatkowska, G. Norman, and R. Segala, Automated verification of a randomized distributed consensus protocol using cadence SMV and PRISM, CAV. pp, pp.194-206, 2001.

D. J. Lehmann and M. O. Rabin, On the advantages of free choice: A symmetric and fully distributed solution to the dining philosophers problem, POPL. pp, pp.133-138, 1981.

O. Lengál, A. Lin, R. Majumdar, and P. Rümmer, Fair termination for parameterized probabilistic concurrent systems, TACAS. LNCS, vol.10205, pp.499-517, 2017.

A. Lin and P. Rümmer, Liveness of randomised parameterised systems under arbitrary schedulers, CAV. LNCS, vol.9780, pp.112-133, 2016.

A. Mostéfaoui, H. Moumen, and M. Raynal, Randomized k-set agreement in crashprone and byzantine asynchronous systems, Theor. Comput. Sci, vol.709, pp.80-97, 2018.

A. Pnueli and L. Zuck, Verification of multiprocess probabilistic protocols, Distributed Computing, vol.1, issue.1, pp.53-72, 1986.

Y. J. Song and R. Van-renesse, Bosco: One-step Byzantine asynchronous consensus, DISC. LNCS, vol.5218, pp.438-450, 2008.