Abstract
Conflict-free Replicated Data Types (CRDTs) allow optimistic replication in a principled way. Different replicas can proceed independently, being available even under network partitions and always converging deterministically: Replicas that have received the same updates will have equivalent state, even if received in different orders. After a historical tour of the evolution from sequential data types to CRDTs, we present in detail the two main approaches to CRDTs, operation-based and state-based, including two important variations, the pure operation-based and the delta-state based. Intended for prospective CRDT researchers and designers, this article provides solid coverage of the essential concepts, clarifying some misconceptions that frequently occur, but also presents some novel insights gained from considerable experience in designing both specific CRDTs and approaches to CRDTs.

Abstract
This document presents the outcomes of the Dagstuhl Seminar Roadmap for Responsible Robotics, held in September 2023 at the Leibniz Center for Informatics, Schloss Dagstuhl, Germany. The seminar brought together researchers from the fields of robotics, computer science, social and cognitive sciences, and philosophy with the aim of charting a path toward improving responsibility in robotic systems. Through intensive interdisciplinary discussions centered on the various values at stake as robotics increasingly integrates into human life, the participants identified key priorities to guide future research and regulatory efforts. The resulting road map outlines actionable steps to ensure that robotic systems coevolve with human societies, promoting human agency and humane values rather than undermining them. Designed for diverse stakeholders-researchers, policy makers, industry leaders, practitioners, nongovernmental organizations (NGOs), and civil society groups-this road map provides a foundation for collaborative efforts toward responsible robotics.

Abstract
Distributed Hash Tables (DHTs) remain to this day a central component of modern peer-to-peer (P2P) systems, which rely on complex DHT protocols to scale to millions of nodes. The correct operation of DHTs is therefore essential for the proper functioning of these systems. For this reason, formal methods have been employed to model and verify a range of correctness properties of various DHT protocols. However, these verification efforts have focused on protocol-specific properties, such as topological invariants, instead of functional properties. This focus limits our understanding of the precise guarantees offered by each protocol. We propose a protocol-independent axiomatization of DHT properties using Allen Temporal Logic (ATL). To validate our axiomatization, we have implemented it in the Alloy analyser and used our implementation both to establish a number of DHT-derived properties and to generate a set of DHT execution traces that cover an exhaustive list of DHT corner case behaviours.

Abstract
TLA(+) is one of the most popular formal methods for designing concurrent and distributed systems. TLA(+) specifications can be verified with the TLC model checker, but unfortunately only one user-specified configuration of the system is verified at a time. If configurations are simple (e.g. the number of processes in a concurrent algorithm) it is viable to run TLC for several configurations to gain confidence that the system indeed works correctly for all of them. However, for complex configurations it is difficult to do so, and critical configurations can easily be missed. This paper introduces Blast, a tool that simplifies this task, by enabling the user to easily verify a TLA(+) specification for all configurations inside a given scope. Our evaluation using a large benchmark of TLA(+) examples, shows that Blast can be effectively used in a wide range of specifications and helped us uncover issues in several of them.

Abstract
Platforms to support novices learning to program are often accompanied by automated next-step hints that guide them towards correct solutions. Many of those approaches are data-driven, building on historical data to generate higher quality hints. Formal specifications are increasingly relevant in software engineering activities, but very little support exists to help novices while learning. Alloy is a formal specification language often used in courses on formal software development methods, and a platform-Alloy4Fun-has been proposed to support autonomous learning. While non-data-driven specification repair techniques have been proposed for Alloy that could be leveraged to generate next-step hints, no data-driven hint generation approach has been proposed so far. This paper presents the first data-driven hint generation technique for Alloy and its implementation as an extension to Alloy4Fun, being based on the data collected by that platform. This historical data is processed into graphs that capture past students' progress while solving specification challenges. Hint generation can be customized with policies that take into consideration diverse factors, such as the popularity of paths in those graphs successfully traversed by previous students. Our evaluation shows that the performance of this new technique is competitive with non-data-driven repair techniques. To assess the quality of the hints, and help select the most appropriate hint generation policy, we conducted a survey with experienced Alloy instructors.

Abstract