2026-08-17T19:25:26Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:23344 2025-06-25T13:23:37Z ddc:004 open_access

Ensuring Convergence and Invariants Without Coordination (Artifact) Borrego, Dina Preguiça, Nuno Gonzalez Boix, Elisa Ferreira, Carla distributed systems conflict resolution RDTs invariant preservation Our related paper introduces the No-Op framework, a generic approach for enforcing consistency without coordination while guaranteeing both convergence and invariant preservation. We implemented the core of the No-Op replication protocol in VeriFx [De Porre et al., 2023], a programming language for RDTs with automated proof capabilities. Alongside the algorithm implementation, we developed formal proofs to automatically verify the algorithm’s correctness properties when applied to specific data types or application implementations. This artifact bundles the implementation of the No-Op framework, various CRDTs [Marc Shapiro et al., 2011], and an eBay-like auction system akin to the RUBiS system [Emmanuel Cecchet et al., 2002] described in Section 5 of the paper. The artifact also provides a Dockerfile that can be used to reproduce the verification results (Section 4 of the paper). Schloss Dagstuhl – Leibniz-Zentrum für Informatik Dina Borrego and Nuno Preguiça and Elisa Gonzalez Boix and Carla Ferreira 2025 Is Part Of DARTS, Volume 11, Issue 2, Special Issue of the 39th European Conference on Object-Oriented Programming (ECOOP 2025) Article Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/DARTS.11.2.1 urn:nbn:de:0030-drops-233447 https://drops.dagstuhl.de/entities/document/10.4230/DARTS.11.2.1 eng https://creativecommons.org/licenses/by/4.0/legalcode