Accuracy of Message Counting Abstraction in Fault-Tolerant Distributed Algorithms
From MaRDI portal
Publication:2961576
DOI10.1007/978-3-319-52234-0_19zbMath1484.68321OpenAlexW2568409254MaRDI QIDQ2961576
No author found.
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
Specification and verification (program logics, model checking, etc.) (68Q60) Distributed algorithms (68W15)
Related Items
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
Cites Work
- Unnamed Item
- Unnamed Item
- Reconciling fault-tolerant distributed computing and systems-on-chip
- Verification of consensus algorithms using satisfiability solving
- A theory of timed automata
- SMT and POR beat counter abstraction: parameterized model checking of threshold-based distributed algorithms
- Model checking of systems with many identical timed processes
- Booting clock synchronization in partially synchronous systems with hybrid process and link failures
- The Theta-Model: achieving synchrony without clocks
- Tight Cutoffs for Guarded Protocols with Fairness
- Counting Constraints in Flat Array Fragments
- All for the Price of Few
- Uncovering Symmetries in Irregular Process Networks
- A Logic-Based Framework for Verifying Consensus Algorithms
- The Theory of Timed I/O Automata, Second Edition
- What You Always Wanted to Know About Model Checking of Fault-Tolerant Distributed Algorithms
- Parameterized Model Checking of Rendezvous Systems
- On the Completeness of Bounded Model Checking for Threshold-Based Distributed Algorithms: Reachability
- Liveness of Parameterized Timed Networks
- Counterexample-guided abstraction refinement for symbolic model checking
- Bosco: One-Step Byzantine Asynchronous Consensus
- Efficient on-the-fly Algorithm for Checking Alternating Timed Simulation
- Asynchronous consensus and broadcast protocols
- Impossibility of distributed consensus with one faulty process
- Reaching Agreement in the Presence of Faults
- A short counterexample property for safety and liveness verification of fault-tolerant distributed algorithms
- On Verifying Fault Tolerance of Distributed Protocols
- Analysis of timed systems using time-abstracting bisimulations