Document Open Access Logo

Modular Verification of State-Based CRDTs in Separation Logic (Artifact)

Authors Abel Nieto , Arnaud Daby-Seesaram , Léon Gondelman , Amin Timany , Lars Birkedal

PDF

Artifact Description

Thumbnail PDF
PDF
DARTS.9.2.15.pdf
  • Filesize: 0.54 MB
  • 5 pages

Document Identifiers

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)
    0
    PDF Downloads
    0
    Metadata Views

Artifact

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.

Cite As Get 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

Author Details

Abel Nieto
  • Aarhus University, Denmark
Arnaud Daby-Seesaram
  • ENS Paris-Saclay, France
Léon Gondelman
  • Aarhus University, Denmark
Amin Timany
  • Aarhus University, Denmark
Lars Birkedal
  • Aarhus University, Denmark

Funding

This work was supported in part by a Villum Investigator grant (no. 25804), Center for Basic Research in Program Verification (CPV), from the VILLUM Foundation.

Related Article

  • Abel Nieto, Arnaud Daby-Seesaram, Léon Gondelman, Amin Timany, and Lars Birkedal, "Modular Verification of State-Based CRDTs in Separation Logic", in 37th European Conference on Object-Oriented Programming (ECOOP 2023), LIPIcs, Vol. 263, pp. 22:1-22:27, 2023. https://doi.org/10.4230/LIPIcs.ECOOP.2023.22

References

  1. 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. Google Scholar
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact