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.

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.

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.

U. Nestmann, R. Fuzzati, and M. Merro, Modeling consensus in a process calculus, CONCUR. pp, pp.393-407, 2003.

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