Abstract
Recent verification tools aim to make formal verification more accessible for software engineers by automating most of the verification process. However, the manual work and expertise required to write verification helper code, such as loop invariants and auxiliary lemmas and assertions, remains a barrier. This paper explores the use of Large Language Models (LLMs) to automate the generation of loop invariants for programs in Dafny. We tested the approach on a curated dataset of 100 programs in Dafny involving arrays, strings, and numeric types. Using a multimodel approach that combines GPT-4o and Claude 3.5 Sonnet, correct loop invariants (passing the Dafny verifier) were generated at the first attempt for 92% of the programs, and in at most five attempts for 95% of the programs. Additionally, we developed an extension to the Dafny plugin for Visual Studio Code to incorporate automatic loop invariant generation into the IDE. Our work stands out from related approaches by handling a broader class of problems and offering IDE integration.

Abstract
The electrification of transportation, driven by the widespread adoption of electric vehicles and increased integration of renewable energy, is critical to decarbonizing mobility and society. Demand response strategies, such as dynamic pricing, enable indirect control of charging processes, but their success relies on accurately estimating consumer responses to tariff changes. Observational data can provide insights into consumer behavior, but the presence of confounding variables motivates the use of causal inference techniques for a reliable elasticity estimation. This study proposes a data-driven framework for optimizing day-ahead charging tariffs, leveraging causal discovery and inference algorithms validated on a synthetically generated dataset. A sensitivity analysis explores the impact of data availability on elasticity estimation and the performance of the resulting demand response strategy. The findings highlight the potential of causal machine learning to characterize consumers and, ultimately, the need for regular characterization to improve the efficiency of demand-side management.

Abstract
Spatio-temporal prediction tasks play a crucial role in facilitating informed decision-making through anticipatory insights. By accurately predicting future outcomes, the ability to strategize, preemptively address risks, and minimize their potential impact is enhanced. The precision in forecasting spatial and temporal patterns holds significant potential for optimizing resource allocation, land utilization, and infrastructure development. While existing review and survey papers predominantly focus on specific forecasting domains such as intelligent transportation, urban planning, pandemics, disease prediction, climate and weather forecasting, environmental data prediction, and agricultural yield projection, limited attention has been devoted to comprehensive surveys encompassing multiple objects concurrently. This article addresses this gap by comprehensively analyzing techniques employed in traffic, pandemics, disease forecasting, climate and weather prediction, agricultural yield estimation, and environmental data prediction. Furthermore, it elucidates challenges inherent in spatio-temporal forecasting and outlines potential avenues for future research exploration.

Abstract
Algorithmic bias in healthcare mirrors existing data biases. However, the factors driving unfairness are not always known. Medical devices capture significant amounts of data but are prone to errors; for instance, pulse oximeters overestimate the arterial oxygen saturation of darker-skinned individuals, leading to worse outcomes. The impact of this bias in machine learning (ML) models remains unclear. This study addresses the technical challenges of quantifying the impact of medical device bias in downstream ML. Our experiments compare a perfect world, without pulse oximetry bias, using SaO(2) (blood-gas), to the actual world, with biased measurements, using SpO(2) (pulse oximetry). Under this counterfactual design, two models are trained with identical data, features, and settings, except for the method of measuring oxygen saturation: models using SaO(2) are a control and models using SpO(2) a treatment. The blood-gas oximetry linked dataset was a suitable testbed, containing 163,396 nearly-simultaneous SpO(2) - SaO(2) paired measurements, aligned with a wide array of clinical features and outcomes. We studied three classification tasks: in-hospital mortality, respiratory SOFA score in the next 24 h, and SOFA score increase by two points. Models using SaO(2) instead of SpO(2) generally showed better performance. Patients with overestimation of O-2 by pulse oximetry of >= 3% had significant decreases in mortality prediction recall, from 0.63 to 0.59, P < 0.001. This mirrors clinical processes where biased pulse oximetry readings provide clinicians with false reassurance of patients' oxygen levels. A similar degradation happened in ML models, with pulse oximetry biases leading to more false negatives in predicting adverse outcomes.

Abstract
Pain is a highly subjective phenomenon that depends on multiple factors. The common methods used to evaluate pain require the person to be awakened and cooperative, which may not always be possible. Moreover, such methods are subject to non-quantifiable influences, namely the impact of an individual's emotional state on how pain is perceived or how negative emotions may exacerbate pain perception, while positive emotions may attenuate it. The goal of this study was to conduct a novel protocol for pain induction with emotional elicitation and assess its feasibility. In this protocol, the physiological responses were monitored, and collected, through Electrocardiogram, Electrodermal Activity, and surface Electromyogram signals. Along the protocol, the pain perception was evaluated using a 0-10 numerical rating scale and by registering the time from the pain stimulus beginning to the Pain and Tolerance Thresholds. This study comprised three emotional sessions, negative, positive, and neutral, which were performed through videos of excerpts of terror, comedy, and documentary films, respectively, followed by pain induction using the Cold Pressor Task (CPT). A total of 56 participants performed the study, with a CPT mean time of about 91.70 +/- 39.64 s among all the sessions. The conducted protocol was considered feasible and safe as it allowed the collection of physiological data, pain, and questionnaires' reports from 56 participants, without any harm to them. Moreover, the collected data can be further used to assess how emotional conditions influence pain perception and to provide better emotion-calibrated pain recognition systems based on physiological signals.

Abstract
Increased electrification of various critical infrastructures has been recognized as a key to achieving decarbonization targets worldwide. This creates a need to better understand the risks associated with future power systems and how such risks can be defined, assessed, and mitigated. This paper surveys prior work on power system risk assessment and management and explores the various approaches to risk definition, assessment, and mitigation. As a result, the paper proposes how future grid developments should be assessed in terms of risk causes, what methodology may be used to reduce the risk impacts, and how such approaches can increase grid resilience. While we attempt to generalize and classify various approaches to solving the problem of risk assessment and mitigation, we also provide examples of how specific approaches undertaken by the authors in the past may be expanded in the future to address the design and operation of the future electricity system to manage the risk more effectively. The importance of the metrics for risk assessment and methodology for quantification of risk reduction are illustrated through the examples. The paper ends with recommendations on addressing the risk and resilience of the electricity system in the future resilient implementation while achieving decarbonization goals through massive electrification.