Abstract
Debugging and repairing faults when programs fail to formally verify can be complex and time-consuming. Automated Program Repair (APR) can ease this burden by automatically identifying and fixing faults. However, traditional APR techniques often rely on test suites for validation, but these may not capture all possible scenarios. In contrast, formal specifications provide strong correctness criteria, enabling more effective automated repair. In this paper, we present an APR tool for Dafny, a verification-aware programming language that uses formal specifications — including pre-conditions, post-conditions, and invariants — as oracles for fault localization and repair. Assuming the correctness of the specifications and focusing on arithmetic bugs, we localize faults through a series of steps, which include using Hoare logic to determine the state of each statement within the program, and applying Large Language Models (LLMs) to synthesize candidate fixes. The models considered are GPT-4o mini, Llama 3, Mistral 7B, and Llemma 7B. We evaluate our approach using DafnyBench, a benchmark of real-world Dafny programs. Our tool achieves 89.7% fault localization success rate and GPT-4o mini yields the highest repair success rate of 74.18%. These results highlight the potential of combining formal reasoning with LLM-based program synthesis for automated program repair.

Abstract
The transition to the water circular economy (WCE) requires several stakeholders' awareness, articulation, and action involving complex governance concerns. As a participatory approach to identifying problems, designing solutions, and implementing strategic actions, the co-creation process should support stakeholder involvement to adjust existing institutional arrangements to foster the WCE. This article designs and applies a co-creation process to analyse the perception of key stakeholders about institutional challenges for water reuse and explore their contributions to innovate policy, planning, and governance for the implementation of new water reuse technology in Almendralejo (Spain), Lecce (Italy), Omis (Croatia), and Eilat (Israel). The findings indicate that implementing a new water loop encounters complex institutional and production-related obstacles, which different stakeholders address in varying ways. Moreover, the proposed solutions to the on-site issues identified emphasise the need for actions that foster engagement and collaboration, particularly to enhance awareness, training, and regulation. Addressing these challenges associated with adopting new water loops, even when technical, may depend on non-technical solutions regarding the institutional framework. The co-creation processes highlight the importance of focusing on institutional arrangements and stakeholder awareness while implementing new water loops to ensure and promote symbiotic territories that consider the policy, producers', and users' strategies.

Abstract
The textile industry is a complex and dynamic system where structured decision-making processes are essential for efficient supply chain management. In this context, mathematical programming models offer a powerful tool for modeling and optimizing the textile supply chain. This systematic review explores the application of mathematical programming models, including linear programming, nonlinear programming, stochastic programming, robust optimization, fuzzy programming, and multi-objective programming, in optimizing the textile supply chain. The review categorizes and analyzes 163 studies across the textile manufacturing stages, from fiber production to integrated supply chains. Key results reveal the utility of these models in solving a wide range of decision-making problems, such as blending fibers, production planning, scheduling orders, cutting patterns, transportation optimization, network design, and supplier selection, considering the challenges found in the textile sector. Analyzing those models, we point out that sustainability considerations, such as environmental and social aspects, remain underexplored and present significant opportunities for future research. In addition, this study emphasizes the importance of incorporating multi-objective approaches and addressing uncertainties in decision-making to advance sustainable and efficient textile supply chain management.

Abstract
The rise of environmental crimes has become a major concern globally as they cause significant damage to ecosystems, public health and result in economic losses. The availability of vast sensor data provides an opportunity to analyze environmental data proactively. This helps to detect irregularities and uncover potential criminal activities. This paper highlights the critical role played by machine learning (ML) and remote sensing technologies in the continuously evolving scenarios of environmental crime. By examining some case studies on detecting illegal fishing, illegal oil spills, illegal landfills, and illegal logging, we delve into the practical implementation of data-driven approaches for environmental crime detection. Our goal with this study is to provide an overview of the existing research in this area and foster the use of ML and data science techniques to enhance environmental crime detection.

Abstract
Electronic Health Records store extensive patient health data, playing a crucial role in healthcare management. Extracting information from these text-heavy records is difficult due to their domain-specific vocabulary, which challenges applying general-domain techniques. Recent advancements in Large Language Models (LLMs) and an increasing interest in the field have sparked considerable progress in solving Clinical Information Extraction (IE) tasks. We review these applications in Clinical IE, highlighting the most common tasks, most successful methods, and most used datasets and evaluation criteria. Examining 85 studies, we synthesize and organize the current research trends, highlighting common points between papers. The presence of LLMs can be felt in the most common tasks, with novel approaches being attempted and showing promising results. However, breakthroughs are still necessary in designing reliable end-to-end systems that can perform all the Clinical IE tasks within a single system.

Abstract
The Constant Bandwidth Server (CBS) is a mechanism used in real-time systems to enable aperiodic soft realtime tasks with unknown execution parameters to run under a dynamic scheduling policy such as Earliest Deadline First (EDF), while still ensuring schedulability by using a bandwidth reservation strategy. This paper proposes an approach to extend the Zephyr open-source real-time operating system, currently maintained by the Linux Foundation, to support aperiodic tasks with CBS. The paper provides the proposed architecture and the design and implementation of the CBS mechanisms in the operating system, which are then evaluated in two test cases in an embedded platform. © 2025 Elsevier B.V., All rights reserved.