Proving the safety of highly-available distributed objects

DOI10.1007/978-3-030-44914-8_20OpenAlexW2997905744MaRDI QIDQ5041111FDOQ5041111

Authors: Sreeja S. Nair, Gustavo Petri, Marc Shapiro 

Publication date: 13 October 2022

Published in: Programming Languages and Systems (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-030-44914-8_20

Recommendations

• Parallel Processing and Applied Mathematics
• Observable behavior of distributed systems: component reasoning for concurrent objects
• A technique for constructing highly available services
• Distributed Computing
• 'Cause I'm strong enough: reasoning about consistency choices in distributed systems

zbMATH Keywords

consistencytool supportautomatic verificationdistributed application designreplicated objects

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Cites Work

• Title not available (Why is that?)
• Convergent and commutative replicated data types
• Replicated data types, specification, verification, optimality
• Composition in state-based replicated data types
• 'Cause I'm strong enough: reasoning about consistency choices in distributed systems
• Eventual consistency for CRDTs

Cited In (4)

• A technique for constructing highly available services
• Safety-liveness exclusion in distributed computing
• Optimal stateless model checking for causal consistency
• Safety of a Client-Based Version Vector Consistency Protocol of Session Guarantees

Uses Software

• Boogie
• Archive Formal Proofs
• GitHub
• CRDT

This page was built for publication: Proving the safety of highly-available distributed objects

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