Document Open Access Logo

VeriFx: Correct Replicated Data Types for the Masses (Artifact)

Authors Kevin De Porre , Carla Ferreira , Elisa Gonzalez Boix

PDF

Artifact Description

Thumbnail PDF
PDF
DARTS.9.2.19.pdf
  • Filesize: 0.54 MB
  • 2 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Software and its engineering → Domain specific languages
  • Computing methodologies → Distributed programming languages
  • Theory of computation → Distributed algorithms
Keywords
  • distributed systems
  • eventual consistency
  • replicated data types
  • verification

Metrics

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

Our related article presents our novel verification language, called VeriFx. We used VeriFx to implement and verify 51 Conflict-Free Replicated Data Types (CRDTs) and 9 Operational Transformation (OT) functions.
This artifact bundles the implementation of the various CRDTs and OT functions described in the article. The artifact also contains a Docker file that can be used to reproduce the verification results (Table 1 and 2 in the article). In addition, the artifact can also be used to run custom VeriFx programs and verify their correctness.

Cite As Get BibTex

Kevin De Porre, Carla Ferreira, and Elisa Gonzalez Boix. VeriFx: Correct Replicated Data Types for the Masses (Artifact). In Special Issue of the 37th European Conference on Object-Oriented Programming (ECOOP 2023). Dagstuhl Artifacts Series (DARTS), Volume 9, Issue 2, pp. 19:1-19:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023) https://doi.org/10.4230/DARTS.9.2.19

Author Details

Kevin De Porre
  • Vrije Universiteit Brussel, Belgium
Carla Ferreira
  • NOVA School of Science and Technology, Caparica, Portugal
Elisa Gonzalez Boix
  • Vrije Universiteit Brussel, Belgium

Funding

  • De Porre, Kevin: Funded by the Research Foundation - Flanders. Project number 1S98519N.
  • Ferreira, Carla: Partly funded by EU Horizon Europe under Grant Agreement no. 101093006 (TaRDIS), and FCT-Portugal under grants UIDB/04516/2020 and PTDC/CCI-INF/32081/2017.

Related Article

  • Kevin De Porre, Carla Ferreira, and Elisa Gonzalez Boix, "VeriFx: Correct Replicated Data Types for the Masses", in 37th European Conference on Object-Oriented Programming (ECOOP 2023), LIPIcs, Vol. 263, pp. 9:1-9:45, 2023. https://doi.org/10.4230/LIPIcs.ECOOP.2023.9

References

  1. C. A. Ellis and S. J. Gibbs. Concurrency control in groupware systems. In Proceedings of the 1989 ACM SIGMOD International Conference on Management of Data, SIGMOD '89, pages 399-407, New York, NY, USA, 1989. Association for Computing Machinery. URL: https://doi.org/10.1145/67544.66963.
  2. Marc Shapiro, Nuno Preguiça, Carlos Baquero, and Marek Zawirski. Conflict-free Replicated Data Types. In Xavier Défago, Franck Petit, and Vincent Villain, editors, 13th Int. Symp. on Stabilization, Safety, and Security of Distributed Systems, SSS'11, pages 386-400, Grenoble, France, 2011. Springer-Verslag. 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