Byzantizing Paxos by refinement

DOI10.1007/978-3-642-24100-0_22MaRDI QIDQ3095328zbMATH OpenOpenAlexFDO

Authors Leslie Lamport

Publication date 28 October 2011

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-24100-0_22

Mathematics Subject Classification ID

Distributed algorithms (68W15)

Recommendations

• Paxos consensus, deconstructed and abstracted
• Formal modeling and verification of Paxos based on Coq
• Fast Paxos
• Model checking Paxos in Spin
• Generalized Paxos made Byzantine (and less complex)

Cites work

• scientific article; zbMATH DE number 1390334 (Why is no real title available?)
• Fast Paxos
• Impossibility of distributed consensus with one faulty process
• Refined quorum systems
• The PlusCal Algorithm Language
• The existence of refinement mappings

Cited in

(7)

• Analysis of the Blockchain Protocol in Asynchronous Networks
• Quorum tree abstractions of consensus protocols
• Bee's strategy against Byzantines. Replacing Byzantine participants (extended abstract)
• Generalized Paxos made Byzantine (and less complex)
• Tasks in modular proofs of concurrent algorithms
• Survey on Parameterized Verification with Threshold Automata and the Byzantine Model Checker
• Tasks in modular proofs of concurrent algorithms

Describes a project that uses

Uses Software

• PlusCal

This page was built for publication: Byzantizing Paxos by refinement

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