Abstract
Since the publication of the 2020 paper, “Finding the Gaps About Uses of Immersive Learning Environments: A Survey of Surveys,” the landscape of immersive learning environments (ILEs) has continued to evolve rapidly. This update aims to revisit the gaps identified in that previous research and explore emerging trends. We conducted an extensive review of new surveys published after that paper’s cut date. Our findings reveal a significant amount of new published reviews (n?=?64), more than doubling the original corpus (n?=?47). The results highlighted novel themes of usage of immersive environments, helping bridge some 2020 research gaps. This paper discusses those developments and presents a consolidated perspective on the uses of immersive learning environments. © 2025 Elsevier B.V., All rights reserved.

Abstract
In this paper, we introduce a novel approach for rigorously verifying safety properties of state machine specifications. Our method leverages an auto-active verifier and centers around the use of action functions annotated with contracts. These contracts facilitate inductive invariant checking, ensuring correctness during system execution. Our approach is further supported by the Why3-do library, which extends the Why3 tool's capabilities to verify concurrent and distributed algorithms using state machines. Two distinctive features of Why3-do are: (i) it supports specification refinement through refinement mappings, enabling hierarchical reasoning about distributed algorithms; and (ii) it can be easily extended to make verifying specific classes of systems more convenient. In particular, the library contains models allowing for message-passing algorithms to be described with programmed handlers, assuming different network semantics. A gallery of examples, all verified with Why3 using SMT solvers as proof tools, is also described in the paper. It contains several auto-actively verified concurrent and distributed algorithms, including the Paxos consensus algorithm.

Abstract
Subgroup discovery aims to identify interpretable segments of a dataset where model behavior deviates from global trends. Traditionally, this involves uncovering patterns among data instances with respect to a target property, such as class labels or performance metrics. For example, classification accuracy can highlight subpopulations where models perform unusually well or poorly. While effective for model auditing and failure analysis, accuracy alone provides a limited view, as it does not reflect model confidence or sources of uncertainty. This work proposes a complementary approach: subgroup discovery using model uncertainty. Rather than identifying where the model fails, we focus on where it is systematically uncertain, even when predictions are correct. Such uncertainty may arise from intrinsic data ambiguity (aleatoric) or poor data representation in training (epistemic). It can highlight areas of the input space where the model’s predictions are less robust or reliable. We evaluate the feasibility of this approach through controlled experiments on the classification of synthetic data and the Iris dataset. While our findings are exploratory and qualitative, they suggest that uncertainty-based subgroup discovery may uncover interpretable regions of interest, providing a promising direction for model auditing and analysis. © 2025 Elsevier B.V., All rights reserved.

Abstract
One strategy for constructing an artificial neural network with multiple hidden layers is to insert layers incrementally in stages. However, for this approach to be effective, each newly added layer must be properly aligned with the previous layers to avoid degradation of the network output and preserve the already learned knowledge. Ideally, inserting new layers should expand the network’s search space, enabling it to explore more complex representations and ultimately improve overall performance. In this work, we present a novel method for layer insertion in stacked autoencoder networks. The method developed maintains the learning obtained before the layer insertion and allows the acquisition of new knowledge; therefore, it is denoted collaborative. This approach allows this kind of neural network to evolve and learn effectively, while significantly reducing the design time. Unlike traditional methods, it addresses the common challenges associated with manually defining the number of layers and the number of neurons in each layer. By automating this aspect of network design, the proposed method promotes scalability and adaptability between tasks. The effectiveness of the approach was validated on multiple binary classification datasets using neural networks initialized with various architectures. The experimental results demonstrate that the method maintains performance while streamlining the architectural design process. © 2025 Elsevier B.V., All rights reserved.

Abstract
This chapter explores the potential of thermal energy storage (TES) systems towards the decarbonization of industry and energy networks, considering its coordinated management with electrochemical energy storage and renewable energy sources (RES). It covers various TES technologies, including sensible heat storage (SHS), latent heat storage (LHS), and thermochemical energy storage (TCS), each offering unique benefits and facing specific challenges. The integration of TES into industrial parks is highlighted, showing how these systems can optimize energy manage-ment and reduce reliance on external sources. A district heating use case also demonstrates the economic and environmental advantages of a multi-energy management strategy over single-energy approaches. Overall, TES technologies are presented as a promising pathway to greater energy effi-ciency and sustainability in industrial processes.

Abstract
[No abstract available]