\textsc{PSync}: a partially synchronous language for fault-tolerant distributed algorithms

DOI10.1145/2837614.2837650MaRDI QIDQ2828285zbMATH OpenOpenAlexFDO

Authors Cezara Drăgoi, Damien Zufferey, Thomas A. Henzinger

Publication date 24 October 2016

Published in Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1145/2837614.2837650

zbMATH Keywords

automated verificationconsensusfault-tolerant distributed algorithmspartial synchronyround model

Mathematics Subject Classification ID

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

Recommendations

• Parameterized model checking of synchronous distributed algorithms by abstraction
• scientific article; zbMATH DE number 222692
• Synthesis of self-stabilising and Byzantine-resilient distributed systems
• Formal Verification of Distributed Algorithms
• Synthesis of distributed algorithms with parameterized threshold guards

Cited in

(13)

• Cardinality constraints for arrays (decidability results and applications)
• \(\text{Para}^2\): parameterized path reduction, acceleration, and SMT for reachability in threshold-guarded distributed algorithms
• A modular framework for verifying versatile distributed systems
• Synchronizing the asynchronous
• Protocol combinators for modeling, testing, and execution of distributed systems
• Derivation of heard-of predicates from elementary behavioral patterns
• Characterizing Consensus in the Heard-Of Model
• Characterizing asynchronous message-passing models through rounds
• scientific article; zbMATH DE number 7407798 (Why is no real title available?)
• Survey on Parameterized Verification with Threshold Automata and the Byzantine Model Checker
• Quorum tree abstractions of consensus protocols
• A behavioral theory for distributed systems with weak recovery
• A Theory of Architectural Design Patterns

Describes a project that uses

Uses Software

• Nuprl
• Erlang
• PSync
• Distal

This page was built for publication: \textsc{PSync}: a partially synchronous language for fault-tolerant distributed algorithms

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