Byzantizing Paxos by refinement

DOI10.1007/978-3-642-24100-0_22zbMATH Open1350.68281OpenAlexW87932605MaRDI QIDQ3095328FDOQ3095328

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

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)

Mathematics Subject Classification ID

Distributed algorithms (68W15)

Cites Work

• The existence of refinement mappings
• Impossibility of distributed consensus with one faulty process
• The PlusCal Algorithm Language
• Title not available (Why is that?)
• Fast Paxos
• Refined quorum systems

Cited In (7)

• 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
• Analysis of the Blockchain Protocol in Asynchronous Networks

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)