Abstract
This paper reports on the development and validation of a formal model for an automotive adaptive exterior lights system (ELS) with multiple variants in Alloy 6, which is the most recent version of the Alloy lightweight formal specification language that supports mutable relations and temporal logic. We explore different strategies to address variability, one in pure Alloy and another through an annotative language extension. We then show how Alloy and its Analyzer can be used to validate systems of this nature, namely by checking that the reference scenarios are admissible, and to automatically verify whether the established requirements hold. A prototype was developed to translate the provided validation sequences into Alloy and back to further automate the validation process. The resulting ELS model was validated against the provided validation sequences and verified for most of requirements for all variants.

Abstract

Abstract
User studies are paramount for advancing science. In particular, the empirical evaluation of programmer-oriented tools is important to validate research ideas and prototypes, as well as production-ready tools. Previous research has collected several tools used by the software engineering and behavioral science communities to design and run studies. In this work, we study tools used in software engineering studies and identify their features. Furthermore, we analyze three behavioral science experiment tools to identify design ideas that might be adapted to programmer user studies. With this work, we present the set of features currently offered by software engineering tools to support researchers in the design and execution of programmer user studies. We also present the characteristics of some tools used in behavioral science experiments to identify design ideas that can be adapted to programmer user studies.

Abstract
Ensuring the reproducibility of computational scientific experiments is crucial for advancing research and fostering scientific integrity. However, achieving reproducibility poses significant challenges, particularly in the absence of appropriate software tools to help. This paper addresses this issue by comparing existing tools designed to assist researchers across various fields in achieving reproducibility in their work. We were able to successfully run eight tools and execute them to reproduce three existing experiments from different domains. Our findings show the critical role of technical choices in shaping the capabilities of these tools for reproducibility efforts. By evaluating these tools for replicating experiments, we contribute insights into the current landscape of reproducibility support in scientific research. Our analysis offers guidance for researchers seeking appropriate tools to enhance the reproducibility of their experiments, highlighting the importance of informed technical decisions in facilitating reproducibility across diverse domains.

Abstract

Abstract
High-performance computing relies on performance-oriented infrastructures with access to powerful computing resources to complete tasks that contribute to solve complex problems in society. The intensive use of resources and the increase in service demand due to emerging fields of science, combined with the exascale paradigm, climate change concerns, and rising energy costs, ultimately means that the decarbonization of these centers is key to improve their environmental and financial performance. Therefore, a review on the main opportunities and challenges for the decarbonization of high-performance computing centers is essential to help decision-makers, operators and users contribute to a more sustainable computing ecosystem. It was found that state-of-the-art supercomputers are growing in computing power, but are combining different measures to meet sustainability concerns, namely going beyond energy efficiency measures and evolving simultaneously in terms of energy and information technology infrastructure. It was also shown that policy and multiple entities are now targeting specifically HPC, and that identifying synergies with the energy sector can reveal new revenue streams, but also enable a smoother integration of these centers in energy systems. Computing-intensive users can continue to pursue their scientific research, but participating more actively in the decarbonization process, in cooperation with computing service providers. Overall, many opportunities, but also challenges, were identified, to decrease carbon emissions in a sector mostly concerned with improving hardware performance.