Tutorial on Parameterized Model Checking of Fault-Tolerant Distributed Algorithms
From MaRDI portal
Publication:5175774
DOI10.1007/978-3-319-07317-0_4zbMath1445.68133OpenAlexW1799788669MaRDI QIDQ5175774
No author found.
Publication date: 25 February 2015
Published in: Lecture Notes in Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-319-07317-0_4
Specification and verification (program logics, model checking, etc.) (68Q60) Distributed algorithms (68W15)
Related Items (8)
Formal verification of mobile robot protocols ⋮ Survey on Parameterized Verification with Threshold Automata and the Byzantine Model Checker ⋮ Parameterized model checking of rendezvous systems ⋮ What You Always Wanted to Know About Model Checking of Fault-Tolerant Distributed Algorithms ⋮ Finding Cut-Offs in Leaderless Rendez-Vous Protocols is Easy ⋮ \(\text{Para}^2\): parameterized path reduction, acceleration, and SMT for reachability in threshold-guarded distributed algorithms ⋮ The polynomial complexity of vector addition systems with states ⋮ Finding cut-offs in leaderless rendez-vous protocols is easy
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Consensus in the presence of mortal Byzantine faulty processes
- Verification of consensus algorithms using satisfiability solving
- Synchronous consensus under hybrid process and link failures
- Reasoning about networks with many identical finite state processes
- 25 years of model checking. History, achievements, perspectives
- 3-valued abstraction: More precision at less cost
- Proving properties of a ring of finite-state machines
- Control and data abstraction: The cornerstones of practical formal verification
- Checking cache-coherence protocols with TLA\(^+\)
- Verifying programs with unreliable channels
- Booting clock synchronization in partially synchronous systems with hybrid process and link failures
- Proving Approximate Implementations for Probabilistic I/O Automata
- On k -set consensus problems in asynchronous systems
- The Theory of Timed I/O Automata, Second Edition
- The PlusCal Algorithm Language
- Counterexample-guided abstraction refinement for symbolic model checking
- Mixing Lossy and Perfect Fifo Channels
- Reaching approximate agreement in the presence of faults
- Asynchronous consensus and broadcast protocols
- Impossibility of distributed consensus with one faulty process
- Reaching Agreement in the Presence of Faults
- Reasoning about systems with many processes
- Unreliable failure detectors for reliable distributed systems
- CONCUR 2004 - Concurrency Theory
- Tolerating corrupted communication
- Model Checking Synchronized Products of Infinite Transition Systems
- Proving Ptolemy Right: The Environment Abstraction Framework for Model Checking Concurrent Systems
- On Verifying Fault Tolerance of Distributed Protocols
- Formal Methods in Computer-Aided Design
- On Reasoning About Rings
- Verification, Model Checking, and Abstract Interpretation
This page was built for publication: Tutorial on Parameterized Model Checking of Fault-Tolerant Distributed Algorithms
