Abstract
Records are a composite data type available in most programming and specification languages, but they are not natively supported by Alloy. As a consequence, users often find themselves having to simulate records in ad hoc ways, a strategy that is error prone and often encumbers the analysis procedures. This paper proposes a conservative extension to the Alloy language to support record signatures. Uniqueness and completeness is imposed on the atoms of such signatures, while still supporting Alloy's flexible signature hierarchy. The Analyzer has been extended to internally expand such record signatures as partial knowledge for the solving procedure. Evaluation shows that the proposed approach is more efficient than commonly used idioms.

Abstract
We extend and consolidate the security justification for the Dilithium signature scheme. In particular, we identify a subtle but crucial gap that appears in several ROM and QROM security proofs for signature schemes that are based on the Fiat-Shamir with aborts paradigm, including Dilithium. The gap lies in the CMA-to-NMA reduction and was uncovered when trying to formalize a variant of the QROM security proof by Kiltz, Lyubashevsky, and Schaffner (Eurocrypt 2018). The gap was confirmed by the authors, and there seems to be no simple patch for it. We provide new, fixed proofs for the affected CMA-to-NMA reduction, both for the ROM and the QROM, and we perform a concrete security analysis for the case of Dilithium to show that the claimed security level is still valid after addressing the gap. Furthermore, we offer a fully mechanized ROM proof for the CMA-security of Dilithium in the EasyCrypt proof assistant. Our formalization includes several new tools and techniques of independent interest for future formal verification results.

Abstract
Modern online platforms for user modeling and recommendation require complex data infrastructures to collect and process data. Some of this data has to be kept to later be used in batches to train personalization models. However, since user activity data can be generated at very fast rates it is also useful to have algorithms able to process data streams online, in real time. Given the continuous and potentially fast change of content, context and user preferences or intents, stream-based models, and their synchronization with batch models can be extremely challenging. Therefore, it is important to investigate methods able to transparently and continuously adapt to the inherent dynamics of user interactions, preferably over long periods of time. Models able to continuously learn from such flows of data are gaining attention in the recommender systems community, and are being increasingly deployed in online platforms. However, many challenges associated with learning from streams need further investigation. The objective of this workshop is to foster contributions and bring together a growing community of researchers and practitioners interested in online, adaptive approaches to user modeling, recommendation and personalization, and their implications regarding multiple dimensions, such as reproducibility, privacy, fairness, diversity, transparency, auditability, and compliance with recently adopted or upcoming legal frameworks worldwide. © 2023 Owner/Author.

Abstract

Abstract
In this article the influence of the maximum partition size on the performance of a discrete version of the Bat Algorithm (BA) is studied. The Bat Algorithm is a population-based meta-heuristic based on swarm intelligence developed for continuous problems with exceptional results. Thus, it has a set of parameters that must be studied in order to enhance the performance of the meta-heuristic. This paper aims to investigate whether the maximum size of the partitions used for the search operations throughout the algorithm should not also be considered as a parameter. First, a literature review was conducted, with special focus on the parameterization of the meta-heuristics and each of the parameters currently used in the algorithm, followed by its implementation in VBA in Microsoft Excel. After a thorough parameterization of the discrete algorithm, different maximum partition sizes were applied to 30 normally distributed instances to draw broader conclusions. In addition, they were also tested for different sizes of the problem to see if they had an influence on the results obtained. Finally, a statistical analysis was carried out, where it was possible to conclude that there was no maximum partition value for which superiority could be proven, and so the size of the partition should be considered a parameter in the bat algorithm and included in the parametrization of BA. © 2023, The Author(s), under exclusive license to Springer Nature Switzerland AG.

Abstract
Sectorization is the partition of a set or region into smaller parts, taking into account certain objectives. Sectorization problems appear in real-life situations, such as school or health districting, logistic planning, maintenance operations or transportation. The diversity of applications, the complexity of the problems and the difficulty in finding good solutions warrant sectorization as a relevant research area. Decision Support Systems (DSS) are computerised information systems that may provide quick solutions to decision-makers and researchers and allow for observing differences between various scenarios. The paper is an overview of the development of a DSS for Sectorization, its extent, architecture, implementation steps and benefits. It constitutes a quite general system, for it handles various types of problems, which the authors grouped as (i) basic sectorization problems; (ii) sectorization problems with service centres; (iii) re-sectorization problems; and (iv) dynamic sectorization problems. The new DSS is expected to facilitate the resolution of various practitioners’ problems and support researchers, academics and students in sectorization. © 2023, The Author(s), under exclusive license to Springer Nature Switzerland AG.