Randomised Distributed Algorithms Library

Description This is our work on the formal specification and analysis of randomised distributed algorithms. It aims to be integrated in Loco library.
Download A first draft implementation in Coq8.4 and ssreflect1.4, using Alea Library, developed by A. Fontaine and A. Zemmari is available here.
This is clearly a work in progress. Many definitions and proofs are too long and are being improved little by little.