Automated verification of a randomized distributed consensus protocol using cadence SMV and PRISM
From MaRDI portal
Recommendations
- Verification of the randomized consensus algorithm of Aspnes and Herlihy: a case study
- scientific article; zbMATH DE number 1973984
- Using Bounded Model Checking to Verify Consensus Algorithms
- Verification of randomized distributed algorithms
- Randomized Consensus in Expected O(N\log ^2 N) Operations Per Processor
Cited in
(14)- Error bounds for stochastic shortest path problems
- ExplicitPRISMSymm: symmetry reduction technique for explicit models in PRISM
- Certified impossibility results and analyses in Coq of some randomised distributed algorithms
- Using Bounded Model Checking to Verify Consensus Algorithms
- Compositional probabilistic verification through multi-objective model checking
- scientific article; zbMATH DE number 1973984 (Why is no real title available?)
- Verification of randomized distributed algorithms
- Farkas certificates and minimal witnesses for probabilistic reachability constraints
- Verification of the randomized consensus algorithm of Aspnes and Herlihy: a case study
- Verification of randomized consensus algorithms under round-rigid adversaries
- Automated verification of multi-party agreements and scheduling of sending messages in distributed ledger systems
- Verification of consensus algorithms using satisfiability solving
- Quantitative analysis with the probabilistic model checker PRISM
- Protocol conformance through refinement mappings in cadence SMV
This page was built for publication: Automated verification of a randomized distributed consensus protocol using cadence SMV and PRISM
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4551150)
