License: 
Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/DARTS.9.2.15
URN: urn:nbn:de:0030-drops-182553
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2023/18255/
Nieto, Abel ;
Daby-Seesaram, Arnaud ;
Gondelman, Léon ;
Timany, Amin ;
Birkedal, Lars
Modular Verification of State-Based CRDTs in Separation Logic (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.
BibTeX - Entry
@Article{nieto_et_al:DARTS.9.2.15,
author = {Nieto, Abel and Daby-Seesaram, Arnaud and Gondelman, L\'{e}on and Timany, Amin and Birkedal, Lars},
title = {{Modular Verification of State-Based CRDTs in Separation Logic (Artifact)}},
pages = {15:1--15:5},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2023},
volume = {9},
number = {2},
editor = {Nieto, Abel and Daby-Seesaram, Arnaud and Gondelman, L\'{e}on and Timany, Amin and Birkedal, Lars},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2023/18255},
URN = {urn:nbn:de:0030-drops-182553},
doi = {10.4230/DARTS.9.2.15},
annote = {Keywords: separation logic, distributed systems, CRDT, replicated data type, formal verification}
}
|
Keywords: |
|
separation logic, distributed systems, CRDT, replicated data type, formal verification |
|
Collection: |
|
DARTS, Volume 9, Issue 2, Special Issue of the 37th European Conference on Object-Oriented Programming (ECOOP 2023) |
|
Issue Date: |
|
2023 |
|
Date of publication: |
|
11.07.2023 |
