Parameterized model checking of synchronous distributed algorithms by abstraction

DOI10.1007/978-3-319-73721-8_1MaRDI QIDQ3296318zbMATH OpenOpenAlexFDO

Authors Benjamin Aminof, Sasha Rubin, Ilina Stoilkovska, Josef Widder, Florian Zuleger

Publication date 7 July 2020

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL http://resolver.obvsg.at/urn:nbn:at:at-ubtuw:3-3417

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Distributed algorithms (68W15)

Recommendations

• Tutorial on parameterized model checking of fault-tolerant distributed algorithms
• SMT and POR beat counter abstraction: parameterized model checking of threshold-based distributed algorithms
• What you always wanted to know about model checking of fault-tolerant distributed algorithms
• Parameterized verification and model checking for distributed broadcast protocols
• \(\text{Para}^2\): parameterized path reduction, acceleration, and SMT for reachability in threshold-guarded distributed algorithms

Cited in

(21)

• Design and verification of distributed phasers
• \(\text{Para}^2\): parameterized path reduction, acceleration, and SMT for reachability in threshold-guarded distributed algorithms
• SMT and POR beat counter abstraction: parameterized model checking of threshold-based distributed algorithms
• Parameterized model checking of networks of timed automata with Boolean guards
• Verification of agent navigation in partially-known environments
• Eliminating message counters in synchronous threshold automata
• \textsc{PSync}: a partially synchronous language for fault-tolerant distributed algorithms
• Accuracy of message counting abstraction in fault-tolerant distributed algorithms
• What you always wanted to know about model checking of fault-tolerant distributed algorithms
• Parameterized verification and model checking for distributed broadcast protocols
• An abstraction technique for parameterized model checking of leader election protocols: application to FTSP
• A method for the verification of a distributed and synchronized algorithm
• Declarative parameterized verification of distributed protocols via the Cubicle model checker
• Reachability in parameterized systems: all flavors of threshold automata
• Characterizing Consensus in the Heard-Of Model
• Tutorial on parameterized model checking of fault-tolerant distributed algorithms
• Proving Ptolemy Right: The Environment Abstraction Framework for Model Checking Concurrent Systems
• On Verifying Fault Tolerance of Distributed Protocols
• A case study on parametric verification of failure detectors
• Communication-closed asynchronous protocols
• Thread-modular counter abstraction: automated safety and termination proofs of parameterized software by reduction to sequential program verification

This page was built for publication: Parameterized model checking of synchronous distributed algorithms by abstraction

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3296318)