Abstract
We present an imperative refinement language for the development of backtracking programs and discuss its semantic foundations. For expressivity, our language includes prospective values and preference - the latter being a variant of Nelson's biased choice that backtracks from infeasibility of a continuation. Our key contribution is to examine feasibility-preserving refinement as a basis for developing backtracking programs, and several key refinement laws that enable compositional refinement in the presence of non -monotonic program combinators.

Abstract
Cities worldwide have agreed on ambitious goals regarding carbon neutrality; thus, smart cities face challenges regarding active and shared mobility due to public transportation's low attractiveness and lack of real-time multimodal information. These issues have led to a lack of data on the community's mobility choices, traffic commuters' carbon footprint and corresponding low motivation to change habits. Besides, many consumers are reluctant to use some software tools due to the lack of data privacy guarantee. This paper presents a methodology developed in the FranchetAI project that addrebes these issues by providing distributed privacy-preserving machine learning models that identify travel behaviour patterns and respective GHG emissions to recommend alternative options. Also, the paper presents the developed FranchetAI mobile prototype. © 2023 The Authors. Published by ELSEVIER B.V. This is an open access article under the CC BY-NC-ND license (https://creativecommons.org/licenses/by-nc-nd/4.0)

Abstract

Abstract
The Software-Defined Storage (SDS) paradigm has emerged as a way to ease the orchestration and management complexities of storage systems. This work aims to mitigate the storage performance issues that large-scale HPC infrastructures are currently facing by developing a scalable and dependable control plane that can be integrated into an SDS design to take full advantage of the tools this paradigm offers. The proposed solution will enable system administrators to define storage policies (e.g., I/O prioritization, rate limiting) and, based on them, the control plane will orchestrate the storage system to provide better QoS for data-centric applications.

Abstract
HEP-Frame is a new C++ package designed to efficiently perform analyses of datasets from a very large number of events, like those available at the Large Hadron Collider (LHC) at CERN, Geneva. It mainly targets high-performance servers and mini-clusters, and it was designed for natural science researchers with a user-friendly interface to access structured databases. HEP-Frame automatically evaluates the underlying computing resources and builds an adequate code skeleton when creating a data analysis application. At run-time, HEP-Frame analyses a sequence of datasets exploring the available parallelism in the code and hardware resources: it concurrently reads inputs from a user-defined data structure and processes them, following the user-specific sequence of requirements to select relevant data; it manages the efficient execution of that sequence; and it outputs results in userdefined objects (e.g., ROOT structures), stored together with the used input dataset. This paper shows how a domain expert software development can benefit from HEP-Frame, and how it significantly improved the performance of analyses of large datasets produced in proton-proton collisions at the LHC. Two case studies are discussed: the associated production of top quarks together with a Higgs boson (t (t) over barH) at the LHC, and a double- and single-top quark productions at the high-luminosity phase of the LHC (HL-LHC). Results show that the HEP-Frame awareness of the analysis code behaviour and structure, and the underlying hardware system, provides powerful and transparent parallelization mechanisms that largely improve the execution time of data analysis applications.

Abstract
[No abstract available]