Chapar: certified causally consistent distributed key-value stores

DOI10.1145/2837614.2837622zbMATH Open1347.68117OpenAlexW2288327952MaRDI QIDQ2828279FDOQ2828279

Authors: Mohsen Lesani, Christian J. Bell, Adam Chlipala 

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.2837622

Recommendations

• On verifying causal consistency
• Checking causal consistency of distributed databases
• scientific article; zbMATH DE number 7327945
• Causal memory: definitions, implementation, and programming
• 'Cause I'm strong enough: reasoning about consistency choices in distributed systems

zbMATH Keywords

verificationtheorem provingcausal consistency

Mathematics Subject Classification ID

Information storage and retrieval of data (68P20) Specification and verification (program logics, model checking, etc.) (68Q60) Semantics in the theory of computing (68Q55)

Cited In (9)

• 'Cause I'm strong enough: reasoning about consistency choices in distributed systems
• On verifying causal consistency
• Chapar
• Checking causal consistency of distributed databases
• Survey on Parameterized Verification with Threshold Automata and the Byzantine Model Checker
• \(\text{Para}^2\): parameterized path reduction, acceleration, and SMT for reachability in threshold-guarded distributed algorithms
• Aneris: a mechanised logic for modular reasoning about distributed systems
• Synthesis of distributed algorithms with parameterized threshold guards
• Byzantine-tolerant causal broadcast

Uses Software

• Coq
• OCaml

This page was built for publication: Chapar: certified causally consistent distributed key-value stores

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