Abstract
Capsule endoscopy has emerged as a non-invasive alternative to traditional gastrointestinal inspection procedures, such as endoscopy and colonoscopy. Removing sedation risks, it is a patient-friendly and hospital-free procedure, which allows small bowel assessment, region not easily accessible by traditional methods. Recently, deep learning techniques have been employed to analyse capsule endoscopy images, with a focus on lesion classification and/or capsule location along the gastrointestinal tract. This research work presents a novel approach for testing the generalization capacity of deep learning techniques in the lesion location identification process using capsule endoscopy images. To achieve that, AlexNet, InceptionV3 and ResNet-152 architectures were trained exclusively in normal frames and later tested in lesion frames. Frames were sourced from KID and Kvasir-Capsule open-source datasets. Both RGB and grayscale representations were evaluated, and experiments with complete images and patches were made. Results show that the generalization capacity on lesion location of models is not so strong as their capacity for normal frame location, with colon being the most difficult organ to identify.

Abstract
Breast cancer is the most common type of cancer in women worldwide. Because of high survival rates, there has been an increased interest in patient Quality of Life after treatment. Aesthetic results play an important role in this aspect, as these treatments can leave a mark on a patient's self-image. Despite that, there are no standard ways of assessing aesthetic outcomes. Commonly used software such as BCCT.core or BAT require the manual annotation of keypoints, which makes them time-consuming for clinical use and can lead to result variability depending on the user. Recently, there have been attempts to leverage both traditional and Deep Learning algorithms to detect keypoints automatically. In this paper, we compare several methods for the detection of Breast Endpoints across two datasets. Furthermore, we present an extended evaluation of using these models as input for full contour prediction and aesthetic evaluation using the BCCT.core software. Overall, the YOLOv9 model, fine-tuned for this task, presents the best results considering both accuracy and usability, making this architecture the best choice for this application. The main contribution of this paper is the development of a pipeline for full breast contour prediction, which reduces clinician workload and user variability for automatic aesthetic assessment.

Abstract
Unmanned Aerial Vehicles (UAVs) are increasingly employed to enable wireless communications, serving as communications nodes. In previous work, we proposed the Sustainable multi-UAV Performance-aware Placement (SUPPLY) algorithm, which focuses on the energy-efficient placement of multiple UAVs acting as Flying Access Points (FAPs). We also developed the Multi-UAV Energy Consumption (MUAVE) simulator to evaluate UAV energy consumption. However, MUAVE was designed to compute the energy consumption for rotary-wing UAVs only. In this paper, we propose eMUAVE, an enhanced version of the MUAVE simulator that enables the evaluation of the energy consumption for both rotary-wing and fixed-wing UAVs. We then use eMUAVE to evaluate the energy consumption of rotary-wing and fixed-wing UAVs in reference and random networking scenarios. The results show that rotary-wing UAVs are typically more energy-efficient than fixed-wing UAVs when following SUPPLY-defined trajectories.

Abstract
High-performance computing is pivotal for processing large datasets and executing complex simulations, ensuring faster and more accurate results. Improving the performance of software and scientific workflows in such environments requires careful analysis of their computational behavior and energy consumption. Therefore, maximizing computational throughput in these environments, through adequate software configuration and resource allocation, is essential for improving performance. The work presented in this paper focuses on leveraging regression-based machine learning and decision trees to analyze and optimize resource allocation in high-performance computing environments based on application's performance and energy metrics. Applied to a bioinformatics case study, these models enable informed decision-making by selecting the appropriate computing resources to enhance the performance of a phylogenomics software. Our contribution is to better explore and understand the efficient resource management of supercomputers, namely Santos Dumont. We show that the predictions for application's execution time using the proposed method are accurate for various amounts of computing nodes, while energy consumption predictions are less precise. The application parameters most relevant for this work are identified and the relative importance of each application parameter to the accuracy of the prediction is analysed.

Abstract
SPHINCS+ is a post-quantum signature scheme that, at the time of writing, is being standardized as SLH-DSA. It is the most conservative option for post-quantum signatures, but the original tight proofs of security were flawed- as reported by Kudinov, Kiktenko and Fedorov in 2020. In this work, we formally prove a tight security bound for SPHINCS+ using the EasyCrypt proof assistant, establishing greater confidence in the general security of the scheme and that of the parameter sets considered for standardization. To this end, we reconstruct the tight security proof presented by Hulsing and Kudinov (in 2022) in a modular way. A small but important part of this effort involves a complex argument relating four different games at once, of a form not yet formalized in EasyCrypt (to the best of our knowledge). We describe our approach to overcoming this major challenge, and develop a general formal verification technique aimed at this type of reasoning. Enhancing the set of reusable EasyCrypt artifacts previously produced in the formal verification of stateful hash-based cryptographic constructions, we (1) improve and extend the existing libraries for hash functions and (2) develop new libraries for fundamental concepts related to hash-based cryptographic constructions, including Merkle trees. These enhancements, along with the formal verification technique we develop, further ease future formal verification endeavors in EasyCrypt, especially those concerning hash-based cryptographic constructions.

Abstract
The proliferation of wireless devices requires flexible network infrastructures to meet the increasing Quality of Service (QoS) requirements. Mobile Robotic Platforms (MRPs) acting as mobile communications cells are a promising solution to provide on-demand wireless connectivity in dynamic networking scenarios. However, the energy consumption of MRPs is a challenge that must be considered to maximize the availability of the wireless networks created. The main contribution of this paper is the experimental evaluation of the energy consumption of an MRP acting as a mobile communications cell. The evaluation considers different actions performed by a real MRP, demonstrating that energy consumption varies significantly with the type of action performed. The results obtained pave the way for optimizing MRP movement in dynamic networking scenarios, maximizing wireless network's availability while minimizing the MRP energy consumption.