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

randomized algorithmdistributed algorithmformal proofproof assistant

Mathematics Subject Classification ID

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

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

(5)

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

Describes a project that uses

Uses Software

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

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)