The correctness proof of Ben-Or's randomized consensus algorithm, Distributed Computing, pp.1-11, 2012. ,
Principles of model checking, 2008. ,
Another advantage of free choice: Completely asynchronous agreement protocols (extended abstract), In: PODC. pp, pp.27-30, 1983. ,
Parameterized verification of many identical probabilistic timed processes, FSTTCS. LIPIcs, vol.24, pp.501-513, 2013. ,
URL : https://hal.archives-ouvertes.fr/hal-00914263
Asynchronous byzantine agreement protocols, Inf. Comput, vol.75, issue.2, pp.130-143, 1987. ,
Decomposition of distributed programs into communicationclosed layers, Sci. Comput. Program, vol.2, issue.3, pp.155-173, 1982. ,
Impossibility of distributed consensus with one faulty process, J. ACM, vol.32, issue.2, pp.374-382, 1985. ,
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. ,
A short counterexample property for safety and liveness verification of fault-tolerant distributed algorithms, POPL. pp, pp.719-734, 2017. ,
On the completeness of bounded model checking for threshold-based distributed algorithms, Reachability. Information and Computation, vol.252, pp.95-109, 2017. ,
Bymc: Byzantine model checker, ISoLA (3), vol.11246, pp.327-342, 2018. ,
URL : https://hal.archives-ouvertes.fr/hal-01909653
Verifying randomized byzantine agreement, pp.194-209, 2002. ,
PRISM 4.0: Verification of probabilistic real-time systems, CAV. pp, pp.585-591, 2011. ,
URL : https://hal.archives-ouvertes.fr/hal-00648035
Automated verification of a randomized distributed consensus protocol using cadence SMV and PRISM, CAV. pp, pp.194-206, 2001. ,
On the advantages of free choice: A symmetric and fully distributed solution to the dining philosophers problem, POPL. pp, pp.133-138, 1981. ,
Fair termination for parameterized probabilistic concurrent systems, TACAS. LNCS, vol.10205, pp.499-517, 2017. ,
Liveness of randomised parameterised systems under arbitrary schedulers, CAV. LNCS, vol.9780, pp.112-133, 2016. ,
Randomized k-set agreement in crashprone and byzantine asynchronous systems, Theor. Comput. Sci, vol.709, pp.80-97, 2018. ,
Verification of multiprocess probabilistic protocols, Distributed Computing, vol.1, issue.1, pp.53-72, 1986. ,
Bosco: One-step Byzantine asynchronous consensus, DISC. LNCS, vol.5218, pp.438-450, 2008. ,