\(\text{Para}^2\): parameterized path reduction, acceleration, and SMT for reachability in threshold-guarded distributed algorithms

DOI10.1007/s10703-017-0297-4zbMath1380.68279OpenAlexW2747225378WikidataQ59607712 ScholiaQ59607712MaRDI QIDQ1696580

Peng Zhang

Publication date: 14 February 2018

Published in: Formal Methods in System Design (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10703-017-0297-4

zbMATH Keywords

reductioncompletenessbounded model checkingByzantine faultsfault-tolerant distributed algorithmsparameterized verificationpartial orders in distributed systems

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Distributed systems (68M14) Reliability, testing and fault tolerance of networks and computer systems (68M15) Distributed algorithms (68W15)

Related Items (5)

A case study on parametric verification of failure detectors ⋮ Survey on Parameterized Verification with Threshold Automata and the Byzantine Model Checker ⋮ Unnamed Item ⋮ A reduction theorem for randomized distributed algorithms under weak adversaries ⋮ Reachability in Parameterized Systems: All Flavors of Threshold Automata

Uses Software

• z3
• Plingeling
• Ivy
• Treengeling
• PSync
• nuXmv
• FAST
• ByMC
• Verdi
• Chapar
• GitHub
• Lingeling
• IronFleet
• Ivy

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• On the completeness of bounded model checking for threshold-based distributed algorithms: reachability
• An approach to automating the verification of compact parallel coordination programs. I
• SMT and POR beat counter abstraction: parameterized model checking of threshold-based distributed algorithms
• Control and data abstraction: The cornerstones of practical formal verification
• Proof Spaces for Unbounded Parallelism
• Chapar: certified causally consistent distributed key-value stores
• PSync: a partially synchronous language for fault-tolerant distributed algorithms
• Efficient Coverability Analysis by Proof Minimization
• Inductive data flow graphs
• A Logic-Based Framework for Verifying Consensus Algorithms
• What You Always Wanted to Know About Model Checking of Fault-Tolerant Distributed Algorithms
• On the Completeness of Bounded Model Checking for Threshold-Based Distributed Algorithms: Reachability
• Counterexample-guided abstraction refinement for symbolic model checking
• Bosco: One-Step Byzantine Asynchronous Consensus
• Symbolic Counter Abstraction for Concurrent Software
• Asynchronous consensus and broadcast protocols
• Impossibility of distributed consensus with one faulty process
• Reduction
• Time, clocks, and the ordering of events in a distributed system
• Unreliable failure detectors for reliable distributed systems
• Decidability of Parameterized Verification
• Non-blocking atomic commit in asynchronous distributed systems with failure detectors
• Tutorial on Parameterized Model Checking of Fault-Tolerant Distributed Algorithms
• CONCUR 2004 - Concurrency Theory
• CONCUR 2004 - Concurrency Theory
• A short counterexample property for safety and liveness verification of fault-tolerant distributed algorithms
• Proving Ptolemy Right: The Environment Abstraction Framework for Model Checking Concurrent Systems
• Automated Technology for Verification and Analysis
• On Reasoning About Rings
• Model checking parameterized asynchronous shared-memory systems
• Verification, Model Checking, and Abstract Interpretation
• Ivy

This page was built for publication: \(\text{Para}^2\): parameterized path reduction, acceleration, and SMT for reachability in threshold-guarded distributed algorithms