Chapar: certified causally consistent distributed key-value stores

DOI10.1145/2837614.2837622MaRDI QIDQ2828279zbMATH OpenOpenAlexFDO

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

zbMATH Keywords

causal consistencytheorem provingverification

Mathematics Subject Classification ID

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

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

Cited in

(9)

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

Describes a project that uses

Uses Software

• OCaml
• Coq

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)