Randomised Distributed Algorithms Library in Coq
Allyx Fontaine and Akka Zemmari

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.