SMT and POR beat counter abstraction: parameterized model checking of threshold-based distributed algorithms
From MaRDI portal
Publication:1702911
DOI10.1007/978-3-319-21690-4_6zbMath1381.68172OpenAlexW1021521453MaRDI QIDQ1702911
Publication date: 1 March 2018
Full work available at URL: https://doi.org/10.1007/978-3-319-21690-4_6
Specification and verification (program logics, model checking, etc.) (68Q60) Distributed algorithms (68W15)
Related Items (11)
Survey on Parameterized Verification with Threshold Automata and the Byzantine Model Checker ⋮ What You Always Wanted to Know About Model Checking of Fault-Tolerant Distributed Algorithms ⋮ Synthesis of distributed algorithms with parameterized threshold guards ⋮ Cardinality constraints for arrays (decidability results and applications) ⋮ \(\text{Para}^2\): parameterized path reduction, acceleration, and SMT for reachability in threshold-guarded distributed algorithms ⋮ Process algebras and flocks of birds ⋮ Accuracy of Message Counting Abstraction in Fault-Tolerant Distributed Algorithms ⋮ Reachability in Parameterized Systems: All Flavors of Threshold Automata ⋮ On the completeness of bounded model checking for threshold-based distributed algorithms: reachability ⋮ Counting Constraints in Flat Array Fragments ⋮ Characterizing Consensus in the Heard-Of Model
This page was built for publication: SMT and POR beat counter abstraction: parameterized model checking of threshold-based distributed algorithms
