Proving the safety of highly-available distributed objects

DOI10.1007/978-3-030-44914-8_20MaRDI QIDQ5041111zbMATH OpenOpenAlexFDO

Authors Sreeja S. Nair, Gustavo Petri, Marc Shapiro

Publication date 13 October 2022

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

Copyright license Creative Commons Attribution 4.0 International

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

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)

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

Cites work

• scientific article; zbMATH DE number 3574936 (Why is no real title available?)
• 'Cause I'm strong enough: reasoning about consistency choices in distributed systems
• Composition in state-based replicated data types
• Convergent and commutative replicated data types
• Eventual consistency for CRDTs
• Replicated data types, specification, verification, optimality

Cited in

(4)

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

Describes a project that uses

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)