Abstract
Maintaining frequency stability is one of the biggest challenges facing future power systems, due to the increasing penetration levels of inverter-based renewable resources. This investigation experimentally validates the frequency provision capabilities of a real Polymer Electrolyte Membrane (PEM) hydrogen electrolyser (HE) using a power hardware-in-the-loop (PHIL) setup. The PHIL consists of a custom 3-level interleaved buck converter and a hardware platform for real-time control of the converter and conducting grid simulation, associated with the modelling of the future Iberian Peninsula (IP) and Continental Europe (CE) systems. The investigation had the aim of validating earlier simulation work and testing new responses from the electrolyser when providing different frequency services at different provision volumes. The experimental results corroborate earlier simulation results and capture extra electrolyser dynamics as the double-layer capacitance effect, which was absent in the simulations. Frequency Containment Reserve (FCR) and Fast Frequency Response (FFR) were provided successfully from the HE at different provision percentages, enhancing the nadir and the rate of change of frequency (RoCoF) in the power system when facing a large disturbance compared to conventional support only. The results verify that HE can surely contribute to frequency services, paving the way for future grid support studies beyond simulations.

Abstract
This work focuses on designing nonlinear control algorithms for dual half-bridge converters (DHBs). We propose a two-layer controller to regulate the current and voltage of the DHB. The first layer utilizes a change in the control variable to obtain a quasi-linear representation of the DHB, allowing for the application of simple linear controllers to regulate current and power flow. The second layer employs a nonlinear control allocation algorithm to select control actions that fulfill (pseudo) power setpoints specified by the first control layer; it also minimizes peak-to-peak currents in the DHB and enforces voltage balance constraints. We apply the DHB and this new control strategy to manage power flow in a hybrid energy storage system comprising of a battery and supercapacitors. Numerical simulation results demonstrate that, in comparison with state-of-the-art approaches, our control algorithm is capable of maintaining good transient behavior over a wide operating range, while reducing peak-to-peak current by up to 80%.

Abstract
Students in computing education increasingly use large language models (LLMs) such as ChatGPT. Yet, the role of LLMs in supporting cognitively demanding tasks, like deductive program verification, remains poorly understood. This paper investigates how students interact with an LLM when solving formal verification exercises in Dafny, a language that supports functional correctness by allowing programmers to write formal specifications and automatically verifying that the implementation satisfies the specification. We conducted a mixed-methods study with master’s students enrolled in a formal methods course. Each participant completed two verification problems, one with access to a custom ChatGPT interface that logged all interactions and the other without. We identified strategies used by successful students and assessed the level of trust students place in LLMs. Our findings show that students perform significantly better when using ChatGPT; however, performance gains are tied to prompt quality. We conclude with practical recommendations for integrating LLMs into formal methods courses more effectively, including designing LLM-aware challenges that promote learning.

Abstract
It is widely recognized that the well-being, health, and productivity of office workers can be influenced by indoor environmental quality (IEQ) conditions in the workplace. This study aimed to investigate associations between multi-domain IEQ in offices and workers' well-being, health, productivity, and perceived IEQ in 30 open office spaces (6 buildings) located in the urban area of Porto, Portugal. This cross-sectional study included 277 office workers and used a combination of methods to assess their perceptions and physiological responses. Data were collected through questionnaires (covering self-reported well-being, health, productivity, and IEQ satisfaction), pupillometry (autonomic nervous system activity), and concurrent monitoring of IEQ. Correlation, comparative, and regression methods were used to explore associations and differences between IEQ indicators and participants' outcomes. The findings showed that offices typically met acceptable IEQ standards. However, a higher prevalence of health problems and symptoms was observed in offices with higher levels of carbon dioxide (CO2), ozone (O3), particulate matter (PM10), and ultrafine particles (UFP). Interestingly, offices with higher COQ, PM2.5, and volatile organic compounds concentrations were linked to a reduced likelihood of participants reporting asthma, dry cough, and allergies. Additionally, thermal discomfort due to high temperatures, increased PM2.5, UFP, CO2, and O3, and low illuminance appear to reduce eye response in office workers. Higher CO2 and noise levels, and temperatures outside the comfortable range, were linked to lower productivity. The multi-domain analysis showed that perception of multiple IEQ factors significantly explained both self-reported productivity and overall satisfaction with work environment. Overall, ensuring proper IEQ and enhancing workers' satisfaction are essential for creating healthy and productive workplaces.

Abstract

Abstract
In healthcare, diagnoses usually rely on physician expertise. However, complex cases may benefit from consulting similar past clinical reports cases. In this paper, we present MedLink (http://medlink.inesctec.pt), a tool that given a free-text medical report, retrieves and ranks relevant clinical case reports published in health conferences and journals, aiming to support clinical decision-making, particularly in challenging or complex diagnoses. To this regard, we trained two BERT models on the sentence similarity task: a bi-encoder for retrieval and a cross-encoder for reranking. To evaluate our approach, we used 10 medical reports and asked a physician to rank the top 10 most relevant published case reports for each one. Our results show that MedLink’s ranking model achieved NDCG@10 of 0.747. Our demo also includes the visualization of clinical entities (using a NER model) and the production of a textual explanation (using a LLM) to ease comparison and contrasting between reports. © The Author(s), under exclusive license to Springer Nature Switzerland AG 2025.