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.

Abstract
Conventional localization systems typically rely on fixed transmission parameters and signal types, limiting their effectiveness in variable and dynamic underwater environments. The present work investigates the potential of adaptable transmission strategies to enhance signal detection estimation for localization purposes. Two widely used signal types, Linear Frequency Modulated (LFM) chirps and BPSK-modulated Msequences, are selected due to their strong autocorrelation properties and robustness to noise. A matched-filter detection approach based on peak correlation is implemented and evaluated. The analysis examines the impact of varying transmission parameters, namely transmission power and signal duration, on detection performance, which inherently influences time-based localization. Results demonstrate that reconfiguring signal parameters significantly reduces estimation dispersion. Moreover, the optimal signal type is shown to depend on the acoustic scenario, with no single waveform consistently outperforming the other. These findings highlight the value of reconfigurable acoustic systems capable of adapting acoustic systems characteristics based on environmental or system feedback, thereby improving localization performance in navigation tasks and dynamic underwater conditions. © 2025 Marine Technology Society.

Abstract