RDA: a Coq library to reason about randomised distributed algorithms in the message passing model

DOI10.7561/SACS.2016.2.157zbMATH Open1424.68147OpenAlexW2727697810MaRDI QIDQ4621204FDOQ4621204

Authors: A. Fontaine, A. Zemmari 

Publication date: 8 February 2019

Published in: Scientific Annals of Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.7561/sacs.2016.2.157

Recommendations

• Certified impossibility results and analyses in Coq of some randomised distributed algorithms
• Proofs of Randomized Algorithms in Coq
• Validation of Stochastic Systems
• Proofs of randomized algorithms in Coq
• scientific article; zbMATH DE number 1786476

zbMATH Keywords

randomized algorithmdistributed algorithmformal proofproof assistant

Mathematics Subject Classification ID

Randomized algorithms (68W20) Distributed algorithms (68W15)

Cited In (3)

• Validation of Stochastic Systems
• RDA
• Title not available (Why is that?)

Uses Software

• Coq
• PRISM
• Isabelle/HOL
• Haskell
• DAMPAS

This page was built for publication: RDA: a Coq library to reason about randomised distributed algorithms in the message passing model

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4621204)