Formal Verification of Consensus Algorithms Tolerating Malicious Faults

No abstract is available for this paper.

• Publication year

  2011

• Venue

  Safety-critical Systems Symposium

• Publication date

  2011-10-10

• Fields of study

  Computer Science

• Identifiers
  DOI 10.1007/978-3-642-24550-3_11
• External record

  Open on Semantic Scholar

• Source metadata

  Semantic Scholar

• No claims are published for this paper.

• No concepts are published for this paper.

• Byzantizing Paxos by Refinement

  2011cited by this paper
• Automated implementation of complex distributed algorithms specified in the IOA language

  2009cited by this paper
• Formal Verification of a Consensus Algorithm in the Heard-Of Model

  2009cited by this paper
• The Heard-Of model: computing in distributed systems with benign faults

  2009influential reference
• A Reduction Theorem for the Verification of Round-Based Distributed Algorithms

  2009influential reference
• Using Bounded Model Checking to Verify Consensus Algorithms

  2008influential reference
• Tolerating corrupted communication

  2007influential reference
• Model Checking of Consensus Algorithms

  2006influential reference
• Proving the Correctness of Disk Paxos

  2005cited by this paper
• Isabelle/HOL

  2002cited by this paper
• Isabelle/HOL: A Proof Assistant for Higher-Order Logic

  2002cited by this paper
• A Proof Assistant for Higher-Order Logic

  2002cited by this paper
• Formally verified Byzantine agreement in presence of link faults

  2002cited by this paper
• A Probabilistic Extension of UML Statecharts

  2002cited by this paper
• Isabelle/HOL: A Proof Assistant for Higher-Order Logic

  2002influential reference
• The Verified Incremental Design of a Distributed Spanning Tree Algorithm: Extended Abstract

  1999cited by this paper
• Stutter-Invariant Temporal Properties are Expressible Without the Next-Time Operator

  1997cited by this paper
• Specifying and Verifying Fault-Tolerant Systems

  1994cited by this paper
• Distributed Algorithms

  1992influential reference
• Consensus in the presence of partial synchrony

  1988cited by this paper
• Shifting gears: changing algorithms on the fly to expedite Byzantine agreement

  1987cited by this paper
• Impossibility of distributed consensus with one faulty process

  1985cited by this paper
• What Good is Temporal Logic?

  1983cited by this paper
• Decomposition of Distributed Programs into Communication-Closed Layers

  1982cited by this paper

• Functional Reasoning for Distributed Systems with Failures

  2025cites this paper
• Revisited Convergence of Dolev et al BFS Spanning Tree Algorithm

  2025cites this paper
• Certified Round Complexity of Self-Stabilizing Algorithms

  2023cites this paper
• Formal Modelling of PBFT Consensus Algorithm in Event-B

  2022cites this paper
• Holistic Verification of Blockchain Consensus

  2022cites this paper
• Compositional Verification of Byzantine Consensus

  2021cites this paper
• Characterizing consensus in the Heard-Of model

  2020cites this paper
• Derivation of Heard-of Predicates from Elementary Behavioral Patterns

  2020cites this paper
• Certification of an Exact Worst-Case Self-Stabilization Time

  2020influential citation
• Characterization and Derivation of Heard-Of Predicates for Asynchronous Message-Passing Models

  2020cites this paper
• Higher-Order Quantifier Elimination, Counter Simulations and Fault-Tolerant Systems

  2020cites this paper
• Verification of customizable blockchain consensus rule using a formal method

  2020cites this paper
• Formal Techniques for Distributed Objects, Components, and Systems: 40th IFIP WG 6.1 International Conference, FORTE 2020, Held as Part of the 15th International Federated Conference on Distributed Computing Techniques, DisCoTec 2020, Valletta, Malta, June 15–19, 2020, Proceedings

  2020cites this paper
• Asphalion: trustworthy shielding against Byzantine faults

  2019cites this paper
• Formal Methods for Mobile Robots

  2019cites this paper
• Certifying Blockchain Byzantine Fault Tolerance

  2019cites this paper
• The Splendors and Miseries of Rounds

  2019cites this paper
• Formal Verification of Blockchain Byzantine Fault Tolerance

  2019cites this paper
• University of Birmingham Asphalion

  2019cites this paper
• University of Birmingham Asphalion

  2019cites this paper
• University of Birmingham Asphalion

  2019cites this paper
• Communication-Closed Layers as Paradigm for Distributed Systems: A Manifesto

  2018cites this paper
• An Ecosystem for Verifying Implementations of BFT protocols

  2018cites this paper
• On the feasibility of multi-leader replication in the early tiers

  2018cites this paper
• University of Birmingham Velisarios

  2018cites this paper
• Velisarios: Byzantine Fault-Tolerant Protocols Powered by Coq

  2018cites this paper
• Communication-Closed Asynchronous Protocols

  2018cites this paper
• EventML: Specification, verification, and implementation of crash-tolerant state machine replication systems

  2017cites this paper
• Verifying strong eventual consistency in distributed systems

  2017cites this paper
• Counter Simulations via Higher Order Quantifier Elimination: a preliminary report

  2017cites this paper
• Formal verification of mobile robot protocols

  2016cites this paper
• PSync: a partially synchronous language for fault-tolerant distributed algorithms

  2016cites this paper
• Electronic Communications of the EASST Volume 72 ( 2015 ) Proceedings of the 15 th International Workshop on Automated Verification of Critical Systems ( AVoCS 2015 ) Formal Specification , Verification , and Implementation of Fault-Tolerant Systems using EventML

  2015cites this paper
• Proceedings of the 15 th International Workshop on Automated Verification of Critical Systems ( AVoCS 2015 ) Formal Specification , Verification , and Implementation of Fault-Tolerant Systems

  2015cites this paper
• Modeling and Verification of Distributed Algorithms in Theorem Proving Environments

  2014cites this paper
• Tutorial on Parameterized Model Checking of Fault-Tolerant Distributed Algorithms

  2014cites this paper
• Verifying Fault-Tolerant Distributed Algorithms in the Heard-Of Model

  2012cites this paper
• A Structural Analysis of Bitcoin

  2012cites this paper
• Formal Verification of Distributed Algorithms - From Pseudo Code to Checked Proofs

  2012cites this paper
• Compositional Verification of Byzantine Consensus

  year unknowncites this paper
• University of Birmingham Asphalion

  year unknowncites this paper