Reachability in parameterized systems: all flavors of threshold automata
From MaRDI portal
Recommendations
- 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
- \(\text{Para}^2\): parameterized path reduction, acceleration, and SMT for reachability in threshold-guarded distributed algorithms
- Complexity of Verification and Synthesis of Threshold Automata
- Automated Technology for Verification and Analysis
Cites work
- \(\text{Para}^2\): parameterized path reduction, acceleration, and SMT for reachability in threshold-guarded distributed algorithms
- A decompositional approach for computing least fixed-points of datalog programs with \(\mathcal Z\)-counters
- A logic-based framework for verifying consensus algorithms
- A short counterexample property for safety and liveness verification of fault-tolerant distributed algorithms
- A tight lower bound for randomized synchronous consensus
- Abstracting and counting synchronizing processes
- Accuracy of message counting abstraction in fault-tolerant distributed algorithms
- All for the price of few (parameterized verification through view abstraction)
- Automated Technology for Verification and Analysis
- Cutoff bounds for consensus algorithms
- Decidability of parameterized verification
- scientific article; zbMATH DE number 1223619 (Why is no real title available?)
- scientific article; zbMATH DE number 1059894 (Why is no real title available?)
- scientific article; zbMATH DE number 3310089 (Why is no real title available?)
- 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
- Parameterized model checking of synchronous distributed algorithms by abstraction
- Proving liveness of parameterized programs
- Reversal-Bounded Multicounter Machines and Their Decision Problems
- SMT and POR beat counter abstraction: parameterized model checking of threshold-based distributed algorithms
- Synthesis of distributed algorithms with parameterized threshold guards
- The Heard-Of model: computing in distributed systems with benign faults
- The part-time parliament
- Tolerating corrupted communication
Cited in
(12)- \(\text{Para}^2\): parameterized path reduction, acceleration, and SMT for reachability in threshold-guarded distributed algorithms
- Eliminating message counters in synchronous threshold automata
- Attacking the Dimensionality Problem of Parameterized Systems via Bounded Reachability Graphs
- On the completeness of bounded model checking for threshold-based distributed algorithms: reachability
- Characterizing Consensus in the Heard-Of Model
- Verification of randomized consensus algorithms under round-rigid adversaries
- Survey on Parameterized Verification with Threshold Automata and the Byzantine Model Checker
- Coefficient synthesis for threshold automata
- Complexity of Verification and Synthesis of Threshold Automata
- Eliminating Message Counters in Threshold Automata
- Parameterized complexity of safety of threshold automata
- On the completeness of bounded model checking for threshold-based distributed algorithms: reachability
This page was built for publication: Reachability in parameterized systems: all flavors of threshold automata
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5009433)
