Description

This our work on the formal specification and analysis of randomised distributed algorithms.

Documentation

Manual

Download

A first draft implementation in Coq8.4 and ssreflect1.4, using Alea Library, developed by A. Fontaine and A. Zemmari is available here:

RDA.tar

This is clearly a work in progress. Many definitions and proofs are too long and are being improved little by little.