package coq-chapar

  1. Overview
  2. No Docs
A framework for verification of causal consistency for distributed key-value stores and their clients in Coq

Install

Dune Dependency

github.com Edit opam file Versions (9)

Authors

  1. M
    Mohsen Lesani
  2. C
    Christian J. Bell
  3. A
    Adam Chlipala

Maintainers

  1. P
    palmskog@gmail.com

Sources

v8.15.0.tar.gz
sha512=3a808e7b6be2fa10c806498c119a74fa3791fa49ed4a686b0fdbd02ad867046dfa2b430074747511298a4ee54c4aac400bb346ab9dc32d6dab9eea98a10141f3

Description

A framework for modular verification of causal consistency for replicated key-value store implementations and their client programs in Coq. Includes proofs of the causal consistency of two key-value store implementations and a simple automatic model checker for the correctness of client programs.

Tags

category:Computer Science/Concurrent Systems and Protocols/Theory of concurrent systems keyword:causal consistency keyword:key-value stores keyword:distributed algorithms keyword:program verification logpath:Chapar date:2023-02-05

Published: 05 Feb 2023

Dependencies (1)

  1. coq >= "8.14" & < "8.18~"

Dev Dependencies

None

Used by

None

Conflicts

None