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

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)

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)

• '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
• Byzantine-tolerant causal broadcast
• Synthesis of distributed algorithms with parameterized threshold guards

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)