DARTS.9.2.15.pdf
- Filesize: 0.54 MB
- 5 pages
Document
Modular Verification of State-Based CRDTs in Separation Logic (Artifact)
Authors
Abel Nieto 
,
Arnaud Daby-Seesaram ,
Léon Gondelman ,
Amin Timany ,
Lars Birkedal
-
Part of:
Issue:
Special Issue of the 37th European Conference on Object-Oriented Programming (ECOOP 2023)
Volume: DARTS, Volume 9 (ECOOP 2023)
Conference: European Conference on Object-Oriented Programming (ECOOP)
Journal: Dagstuhl Artifacts Series (DARTS) - License:
Creative Commons Attribution 4.0 International license
- Publication Date: 2023-07-11
Artifact Description
Document Identifiers
Author Details
Cite AsGet BibTex
Abel Nieto, Arnaud Daby-Seesaram, Léon Gondelman, Amin Timany, and Lars Birkedal. Modular Verification of State-Based CRDTs in Separation Logic (Artifact). In Special Issue of the 37th European Conference on Object-Oriented Programming (ECOOP 2023). Dagstuhl Artifacts Series (DARTS), Volume 9, Issue 2, pp. 15:1-15:5, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/DARTS.9.2.15
https://doi.org/10.4230/DARTS.9.2.15
Artifact
DARTS-9-2-15-artifact-806cc18ae49047142453ecbc47175c8e.ova
(Filesize: 5.45 GB)
Artifact Evaluation Policy
The artifact has been evaluated as described in the ECOOP 2023 Call for Artifacts and the ACM Artifact Review and Badging Policy
Abstract
This is the documentation of the artifact for the paper "Modular Verification of State-Based CRDTs in Separation Logic". The artifact consists of a Coq formalization of the safety proofs for state-based CRDTs described in the paper. The Coq proofs are written in the Aneris distributed separation logic.
Subject Classification
ACM Subject Classification
- Theory of computation → Program verification
- Theory of computation → Distributed algorithms
- Theory of computation → Separation logic
Keywords
- separation logic
- distributed systems
- CRDT
- replicated data type
- formal verification
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads
References
-
Abel Nieto, Léon Gondelman, Alban Reynaud, Amin Timany, and Lars Birkedal. Modular verification of op-based crdts in separation logic. Proc. ACM Program. Lang., 6(OOPSLA2):1788-1816, 2022.
