Accuracy of message counting abstraction in fault-tolerant distributed algorithms

DOI10.1007/978-3-319-52234-0_19MaRDI QIDQ2961576zbMATH OpenOpenAlexFDO

Authors

Publication date 21 February 2017

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

Full work available at URL http://resolver.obvsg.at/urn:nbn:at:at-ubtuw:3-2936

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Distributed algorithms (68W15)

Recommendations

• Theorem Proving in Higher Order Logics
• Parameterized model checking of synchronous distributed algorithms by abstraction
• A short counterexample property for safety and liveness verification of fault-tolerant distributed algorithms
• SMT and POR beat counter abstraction: parameterized model checking of threshold-based distributed algorithms
• Tutorial on parameterized model checking of fault-tolerant distributed algorithms

Cites work

• scientific article; zbMATH DE number 176728 (Why is no real title available?)
• scientific article; zbMATH DE number 5585443 (Why is no real title available?)
• A logic-based framework for verifying consensus algorithms
• A short counterexample property for safety and liveness verification of fault-tolerant distributed algorithms
• A theory of timed automata
• All for the price of few (parameterized verification through view abstraction)
• Analysis of timed systems using time-abstracting bisimulations
• Asynchronous consensus and broadcast protocols
• Booting clock synchronization in partially synchronous systems with hybrid process and link failures
• Bosco: One-Step Byzantine Asynchronous Consensus
• Counterexample-guided abstraction refinement for symbolic model checking
• Counting constraints in flat array fragments
• Efficient on-the-fly algorithm for checking alternating timed simulation
• Impossibility of distributed consensus with one faulty process
• Liveness of parameterized timed networks
• Model checking of systems with many identical timed processes
• On Verifying Fault Tolerance of Distributed Protocols
• On the completeness of bounded model checking for threshold-based distributed algorithms: reachability
• Parameterized model checking of rendezvous systems
• Reaching Agreement in the Presence of Faults
• Reconciling fault-tolerant distributed computing and systems-on-chip
• SMT and POR beat counter abstraction: parameterized model checking of threshold-based distributed algorithms
• The Theta-Model: achieving synchrony without clocks
• The theory of timed I/O automata
• Tight cutoffs for guarded protocols with fairness
• Uncovering symmetries in irregular process networks
• Verification of consensus algorithms using satisfiability solving
• What you always wanted to know about model checking of fault-tolerant distributed algorithms

Cited in

(6)

• Counting protocols for reliable end-to-end transmission
• Scalable eventually consistent counters over unreliable networks
• Synthesis of distributed algorithms with parameterized threshold guards
• Reachability in parameterized systems: all flavors of threshold automata
• Parameterized model checking of networks of timed automata with Boolean guards
• Ability to Count Messages Is Worth Θ(Δ) Rounds in Distributed Computing

This page was built for publication: Accuracy of message counting abstraction in fault-tolerant distributed algorithms

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