Formally Verified Conflict-Free Replicated Data Types

Class: CS-550, Formal Verification (EPFL Website)

Setup

This project uses the Isabelle/HOL proof assistant. The project can be run as follows:

# Builds and checks the theories
isabelle build -D . CRDT

# Generates the browser info
isabelle build -D . -o browser_info -v

Structure

Here's a short rundown of the files from this repository:

• ROOT: the Isabelle/HOL root file.
• CvRDT.thy: the CvRDT locale, and its lemmas.
• Export.thy: Scala export for the CvRDTs.
• Set-based CvRDTs theories:
  • USet;
  • Log; and
  • PNSet.
• Vector-based CvRDTs theories:
  • IntegerVector; and
  • GCounter.
• The generated Scala code can be found in the scala folder.
• Work-in-progress theories are available in the wip folder.

Team

Name	Email
Alexandre Piveteau	alexandre.piveteau@epfl.ch
Patrick Gilliard	patrick.gilliard@epfl.ch
Victor Schneuwly	victor.schneuwly@epfl.ch