Skip to content

Latest commit

 

History

History
15 lines (12 loc) · 884 Bytes

README.md

File metadata and controls

15 lines (12 loc) · 884 Bytes
Raw

Verification of CRDTs with Isabelle

The theory files can be checked with Isabelle 2013-2. Isabelle 2013-1 and other older verisions are not compatible.

Code structure:

  • all.thy: theory which imports all other theory-files ( can be used to find unused theorems in all files and to load everything at once)
  • src/framework/: Contains the general framework which applies to all CRDTs
  • src/crdts/: Contains the different verified CRDTs. For each CRDT there are several files with the following postfixes:
    • [crdt-name]_spec: the specification of the data type
    • [crdt-name]_[implementation-name]: an implementation of the data type
    • [crdt-name]_[implementation-name]_convergence: convergence proofs for the implementation
    • [crdt-name]_[implementation-name]_valid: proofs that the implementation is conform to its specification