Abstract
We present a formally verified proof of the correctness and IND-CCA security of ML-KEM, the Kyber-based Key Encapsulation Mechanism (KEM) undergoing standardization by NIST. The proof is machine-checked in EasyCrypt and it includes: 1) A formalization of the correctness (decryption failure probability) and IND-CPA security of the Kyber base public-key encryption scheme, following Bos et al. at Euro S&P 2018; 2) A formalization of the relevant variant of the Fujisaki-Okamoto transform in the Random Oracle Model (ROM), which follows closely (but not exactly) Hofheinz, Hovelmanns and Kiltz at TCC 2017; 3) A proof that the IND-CCA security of the ML-KEM specification and its correctness as a KEM follows from the previous results; 4) Two formally verified implementations of ML-KEM written in Jasmin that are provably constant-time, functionally equivalent to the ML-KEM specification and, for this reason, inherit the provable security guarantees established in the previous points. The top-level theorems give self-contained concrete bounds for the correctness and security of ML-KEM down to (a variant of) Module-LWE. We discuss how they are built modularly by leveraging various EasyCrypt features.

Abstract
The Web of Things (WoT) is an essential component within the Internet of Things (IoT) domain, offering a standardized method for describing, consuming, and orchestrating the functions of IoT devices. WoT plays a crucial role in promoting interoperability and streamlining the development of applications for IoT solutions. Recent research focusing on IoT solutions for ambient assisted living (AAL) has highlighted WoT as a key framework for integrating diverse smart devices and services to enhance the quality of life for older adults and individuals with specific health conditions. However, a closer look at recent literature reviews reveals a deficiency in comprehensive research regarding the interplay between WoT, AAL, and the health and wellbeing of older adults. To address this question, a comprehensive mapping review is performed to delve into the existing literature and pinpoint the most pertinent themes and topics within WoT. This analysis aims to uncover evidence of the correlation between WoT, AAL, and active and healthy aging (AHA) to support future research in this area.

Abstract
The advantages of Virtual Reality (VR) over traditional training, together with the development of VR technology, have contributed to an increase in the body of literature on training professionals with VR. However, there is a gap in the literature concerning the comparison of training in a Virtual Environment (VE) with the same training in a Real Environment (RE), which would contribute to a better understanding of the capabilities of VR in training. This paper presents a study with firefighters (N = 12) where the effect of a firefighter training exercise in a VE was evaluated and compared to that of the same exercise in a RE. The effect of environments was evaluated using psychophysiological measures by evaluating the perception of stress and fatigue, transfer of knowledge, sense of presence, cybersickness, and the actual stress measured through participants' Heart Rate Variability (HRV). The results showed a similar perception of stress and fatigue between the two environments; a positive, although not significant, effect of the VE on the transfer of knowledge; the display of moderately high presence values in the VE; the ability of the VE not to cause symptoms of cybersickness; and finally, obtaining signs of stress in participants' HRV in the RE and, to a lesser extent, signs of stress in the VE. Although the effect of the VE was shown to be non-comparable to that of the RE, the authors consider the results encouraging and discuss some key factors that should be addressed in the future to improve the results of the training VE.

Abstract
This study introduces the development of a client-based software layer within the FGPE project, aimed at enhancing the usability of the FGPE programming learning environment through client-side processing. The primary goal is to enable the evaluation of programming exercises and the application of gamification rules directly on the client-side, thereby facilitating offline functionality. This approach is particularly beneficial in regions with unreliable internet connectivity, as it allows continuous student interaction and feedback without the need for a constant server connection. The implementation promises to reduce server load significantly by shifting the evaluation workload to the client-side. This not only improves response times but also alleviates the burden on server resources, enhancing overall system efficiency. Two main strategies are explored: 1) caching the gamification service interface on the client-side, and 2) implementing a complete client-side gamification service that synchronizes with the server when online. Each approach is evaluated in terms of its impact on user experience, system performance, and potential security concerns. The findings suggest that while client-side processing offers considerable benefits in terms of scalability and user engagement, it also introduces challenges such as increased system complexity and potential data synchronization issues. The study concludes with recommendations for balancing these factors to optimize the design and implementation of client-based systems for educational environments. © Ricardo Queirós, Robertas Damaševicius, Rytis Maskeliunas, and Jakub Swacha;

Abstract
Wikipedia is the world's largest online encyclopedia, but maintaining article quality through collaboration is challenging. Wikipedia designed a quality scale, but with such a manual assessment process, many articles remain unassessed. We review existing methods for automatically measuring the quality of Wikipedia articles, identifying and comparing machine learning algorithms, article features, quality metrics, and used datasets, examining 149 distinct studies, and exploring commonalities and gaps in them. The literature is extensive, and the approaches follow past technological trends. However, machine learning is still not widely used by Wikipedia, and we hope that our analysis helps future researchers change that reality.

Abstract
Local electricity markets are emerging as a viable solution to overcome the challenges brought by the large penetration of distributed renewable generation and the need to put consumers as central players in the system, with an active and dynamic role. Although there is significant literature addressing the topic of local electricity markets, this is still a rather new and emerging topic. Hence, this study provides an overall view of this domain and a perspective on future needs and challenges that must be addressed. This review introduces the most important concepts in the local electricity market domain, provides an analysis on the different policy and regulatory framework, exposes the most relevant worldwide initiatives related to the field implementation, and scrutinizes the alternative local market models proposed in the literature. The discussion puts forth the main benefits and barriers of the currently proposed local market models, and the expected impact of their widespread implementation. The review is concluded with the wrap-up and discussion on the most relevant paths for future research and development in this field of study.