Neem

Neem is a framework for automated verification of mergeable replicated data types (MRDTs) and state-based convergent replicated data types (CRDTs). See https://dl.acm.org/doi/10.1145/3720452.

Development Environment

Easiest way to get started is to use the devcontainer.

$ git clone https://github.com/prismlab/neem
$ cd neem
$ code . # Start VSCode

VSCode will notify that there is a devcontainer associated with this repo and whether to open this repo in a devcontainer.

Click "Reopen in Container".

Choose "from DockerHub" option. The repo will be opened in a devcontainer. This will take a while when you do it for the first time to download the Docker image.

You can check whether everything works correctly by running

$ ./verify_crdts.sh

to confirm that everything works fine. This will verify CRDT implementations and produce a table at the end summarising the verification time.

<snip>
Verification Results:
CRDT                           Verification Time (s)
------------------------------ --------------------
Increment-only_counter         2                   
PN_counter                     5                   
Grow-only_set                  2                   
Grow-only_map                  4                   
OR-Set                         4                   
2P-Set                         3                   
Multi-valued_register          2