Principles of model checking, 2008. ,
Another advantage of free choice: Completely asynchronous agreement protocols (extended abstract), In: PODC. pp, pp.27-30, 1983. ,
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. ,
Randomized k-set agreement in crashprone and byzantine asynchronous systems, Theor. Comput. Sci, vol.709, pp.80-97, 2018. ,
Modeling consensus in a process calculus, CONCUR. pp, pp.393-407, 2003. ,
Bosco: One-step Byzantine asynchronous consensus, DISC. LNCS, vol.5218, pp.438-450, 2008. ,