C. [. Audebaud and . Paulin-mohring, Proofs of randomized algorithms in Coq, Science of Computer Programming, vol.74, issue.8, pp.568-589, 2009.
DOI : 10.1016/j.scico.2007.09.002
URL : https://hal.archives-ouvertes.fr/inria-00431771

G. Barthe, J. M. Crespo, B. Grégoire, C. Kunz, and S. Z. Béguelin, Computer-aided cryptographic proofs, In ITP, pp.11-27, 2012.
DOI : 10.1007/978-3-642-32347-8_2
URL : https://hal.archives-ouvertes.fr/hal-00765869

]. D. Can and . Cansell, A development in Event-B of a distributed algorithm for building a spanning tree

V. [. Castéran and . Filou, Loco : A Coq Library on Local Computation Systems

V. [. Castéran and . Filou, Tasks, types and tactics for local computation systems, Studia Informatica Universalis, vol.91, pp.39-86, 2011.

V. [. Castéran, M. Filou, and . Mosbah, Certifying Distributed Algorithms by Embedding Local Computation Systems in the Coq Proof Assistant, Proceedings of Symbolic Computation in Software Science Tunisie, 2009.

A. [. Castéran, A. Fontaine, and . Zemmari, Rda : A Coq Library on Randomised Distributed Algorithms

]. Cho95 and . Chou, Mechanical verification of distributed algorithms in higher-order logic, The Computer Journal, vol.38, issue.2, pp.152-161, 1995.

D. [. Cansell and . Méry, Logics of Specification Languages, chapter The Event-B Modelling Method : Concepts and Case Studies, pp.47-152, 2007.

C. Derman, Finite state Markovian decision processes Mathematics in science and engineering, 1970.

G. Gonthier, A. Mahboubi, and E. Tassi, A Small Scale Reflection Extension for the Coq system, 2008.
URL : https://hal.archives-ouvertes.fr/inria-00258384

J. Hurd, Formal Verification of Probabilistic Algorithms, 2002.

M. Z. Kwiatkowska, G. Norman, and D. Parker, PRISM: Probabilistic Symbolic Model Checker, Computer Performance Evaluation / TOOLS, pp.200-204, 2002.
DOI : 10.1007/3-540-46029-2_13
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.100.2142

]. C. Lav94 and . Lavault, Orientation of distributed networks : Graph-and group-theoretic modelling, SIROCCO, pp.49-70, 1994.

E. [. Métivier and . Sopena, Graph relabelling systems : A general overview, Computers and Artificial Intelligence, vol.16, issue.2, 1997.

N. [. Métivier, A. Saheb, and . Zemmari, Analysis of a randomized rendezvous algorithm, Information and Computation, vol.184, issue.1, pp.109-128, 2003.
DOI : 10.1016/S0890-5401(03)00054-3

M. [. Milner, R. Tofte, and . Harper, The Definition of Standard ML. Computational Models of Cognition and Perception Series, 1990.

G. Norman, Analysing Randomized Distributed Algorithms, Validation of Stochastic Systems, pp.384-418, 2004.
DOI : 10.1007/978-3-540-24611-4_11
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.103.9635

A. Pogosyants and R. Segala, Formal verification of timed properties of randomized distributed algorithms, Proceedings of the fourteenth annual ACM symposium on Principles of distributed computing , PODC '95, pp.174-183, 1995.
DOI : 10.1145/224964.224984

]. K. Ros and . Rosen, Handbook of discrete and combinatorial mathematics

G. Tel, Introduction to distributed algorithms, 2000.
DOI : 10.1017/CBO9781139168724