Para^2: parameterized path reduction, acceleration, and SMT for reachability in threshold-guarded distributed algorithms
From MaRDI portal
Publication:1696580
Recommendations
- SMT and POR beat counter abstraction: parameterized model checking of threshold-based distributed algorithms
- On the completeness of bounded model checking for threshold-based distributed algorithms: reachability
- On the completeness of bounded model checking for threshold-based distributed algorithms: reachability
- Reachability in parameterized systems: all flavors of threshold automata
- Parameterized model checking of synchronous distributed algorithms by abstraction
Cites work
- \textsc{PSync}: a partially synchronous language for fault-tolerant distributed algorithms
- A logic-based framework for verifying consensus algorithms
- A short counterexample property for safety and liveness verification of fault-tolerant distributed algorithms
- An approach to automating the verification of compact parallel coordination programs. I
- Asynchronous consensus and broadcast protocols
- Automated Technology for Verification and Analysis
- Bosco: One-Step Byzantine Asynchronous Consensus
- Chapar: certified causally consistent distributed key-value stores
- CONCUR 2004 - Concurrency Theory
- CONCUR 2004 - Concurrency Theory
- Control and data abstraction: The cornerstones of practical formal verification
- Counterexample-guided abstraction refinement for symbolic model checking
- Decidability of parameterized verification
- Efficient coverability analysis by proof minimization
- scientific article; zbMATH DE number 996442 (Why is no real title available?)
- scientific article; zbMATH DE number 177513 (Why is no real title available?)
- scientific article; zbMATH DE number 1953038 (Why is no real title available?)
- scientific article; zbMATH DE number 1956578 (Why is no real title available?)
- scientific article; zbMATH DE number 1830912 (Why is no real title available?)
- scientific article; zbMATH DE number 1903348 (Why is no real title available?)
- Impossibility of distributed consensus with one faulty process
- Inductive data flow graphs
- Ivy
- Non-blocking atomic commit in asynchronous distributed systems with failure detectors
- On Reasoning About Rings
- On the completeness of bounded model checking for threshold-based distributed algorithms: reachability
- On the completeness of bounded model checking for threshold-based distributed algorithms: reachability
- Proof spaces for unbounded parallelism
- Proving Ptolemy Right: The Environment Abstraction Framework for Model Checking Concurrent Systems
- Reduction
- SMT and POR beat counter abstraction: parameterized model checking of threshold-based distributed algorithms
- Symbolic Counter Abstraction for Concurrent Software
- Time, clocks, and the ordering of events in a distributed system
- Tutorial on parameterized model checking of fault-tolerant distributed algorithms
- Unreliable failure detectors for reliable distributed systems
- Verification, Model Checking, and Abstract Interpretation
- What you always wanted to know about model checking of fault-tolerant distributed algorithms
Cited in
(12)- SMT and POR beat counter abstraction: parameterized model checking of threshold-based distributed algorithms
- Eliminating message counters in synchronous threshold automata
- A reduction theorem for randomized distributed algorithms under weak adversaries
- On the completeness of bounded model checking for threshold-based distributed algorithms: reachability
- Parameterized model checking of synchronous distributed algorithms by abstraction
- Reachability in parameterized systems: all flavors of threshold automata
- Verification of randomized consensus algorithms under round-rigid adversaries
- A case study on parametric verification of failure detectors
- Survey on Parameterized Verification with Threshold Automata and the Byzantine Model Checker
- Complexity of Verification and Synthesis of Threshold Automata
- Eliminating Message Counters in Threshold Automata
- On the completeness of bounded model checking for threshold-based distributed algorithms: reachability
Describes a project that uses
Uses Software
This page was built for publication: \(\text{Para}^2\): parameterized path reduction, acceleration, and SMT for reachability in threshold-guarded distributed algorithms
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1696580)
