chapar

Distributed store verifier

A framework for verifying causal consistency in distributed key-value stores and their clients using the Coq proof assistant

A framework for verification of causal consistency for distributed key-value stores and their clients in Coq [maintainer=@palmskog]

GitHub

32 stars
13 watching
7 forks
Language: Coq
last commit: over 2 years ago
causal-consistencycoqcoq-extractiondistributed-systemsdocker-coq-actionkey-valuenix-actionocaml

Related projects:

RepositoryDescriptionStars
coq-community/coq-program-verification-templateA template project for verifying the correctness of C programs in Coq29
coq/platformA multi-platform distribution of the Coq proof assistant and its libraries, providing a standardized setup for development and teaching191
coq-community/paramcoqA Coq plugin providing commands for generating parametricity statements used in data refinement proofs.45
coq-community/parsequeA Coq library that provides a total parser combinator library with support for building parsers and grammars in the language of Coq.42
coq-community/reglangProvides definitions and verified translations between various representations of regular languages in the Coq proof assistant41
coq-community/cornA comprehensive formalization of mathematical structures and concepts for verified computation in Coq.111
distributedcomponents/diselA framework for implementing and verifying distributed systems using Coq95
coq-community/fav-ssrA comprehensive library of verified data structures and algorithms in Coq45
coq-community/lemma-overloadingA Coq library demonstrating design patterns for automated proof automation and canonical structures26
coq-community/coq-ext-libA collection of reusable Coq definitions and theorems for building software development tools129
coq-community/dblibA Coq library for manipulating binding structures in syntax with binders.30
coq-community/coqtail-mathA collection of mathematical theorems and tools within the Coq proof assistant15
coq-community/docker-coqProvides pre-configured Docker images for building and testing the Coq proof assistant37
coq-community/manifestoA collaborative effort to maintain and promote Coq packages and tools.68
josefgit/concertA framework for verifying smart contracts in Coq, a proof assistant language.0