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
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
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

Abstract
Although recent studies have recognised that sustainability and resilience should be considered part of the same efforts in the context of a transformative perspective, research combining both constructs is still scarce. This study adopts a comprehensive perspective that acknowledges that maintaining business continuity (through persisting, adapting or transforming), to reduce long-term risks is a common aspect of sustainability and resilience. It aims to identify strategies to be applied by companies and SCs in order to increase their social, environmental and economic sustainability, as well as their ability to be ready, respond and recover from unexpected events. Considering that the actions and strategies to deal with sustainability and resilience can be different and eventually paradoxical, this work applies the organizational ambidexterity approach as a theoretical background.

Abstract