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

DOI10.7561/SACS.2016.2.157MaRDI QIDQ4621204zbMATH OpenOpenAlexFDO

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

zbMATH Keywords

distributed algorithmformal proofproof assistantrandomized algorithm

Mathematics Subject Classification ID

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

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

Cited in

(6)

• Layered reasoning for randomized distributed algorithms
• Certified impossibility results and analyses in Coq of some randomised distributed algorithms
• scientific article; zbMATH DE number 1324651 (Why is no real title available?)
• RDA
• scientific article; zbMATH DE number 1884413 (Why is no real title available?)
• Validation of Stochastic Systems

Describes a project that uses

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)