Abstract
Planar surfaces are commonly found in man-made underwater environments and can be employed to support underwater SLAM. This work focuses on 3D plane extraction, building on two-dimensional acoustic scans collected from an imaging sonar. The novel contribution of our algorithm exploits the sonar's wider beamwidth and ability to collect secondary echoes from these structures to extract a three-dimensional surface from the acquired acoustic image. Building on a Hough Transform-based algorithm adapted to polar-based acoustic imagery, line feature detection supports plane representation segmentation. An inverse sensor model is subsequently employed to estimate additional plane parameters: inclination, length, and height. Experimental assessment in a confined controlled environment is introduced, validating the accuracy of the algorithm. Additional results from a dam shaft scenario are also presented to assess the potential of the developed tool.

Abstract
This study aims to explore the complexities of digital accessibility, focusing on the essential tasks of evaluating and monitoring the accessibility of digital content. It seeks to identify the main challenges encountered by practitioners on the field and to reveal best practices and research opportunities for enhancing digital accessibility. Using a mixed-methods approach, the study combines an online survey and in-depth interviews, gathering insights from 27 practitioners across 16 countries. The findings underscore substantial gaps in education and professional training within accessibility. Challenges identified include ensuring technical compliance while addressing user needs, limitations of current automated tools, especially for mobile accessibility, and the disparity between formal compliance and user-centric accessibility. The study highlights best practices such as comprehensive training, effective project management, and innovative testing strategies. This research underscores the need for refined evaluation methodologies and a deeper understanding of accessibility principles among stakeholders. It advocates for collaborative efforts to address the nuanced challenges of making digital spaces universally accessible. Future research should leverage emerging technologies, particularly Artificial Intelligence, to enhance accessibility evaluations and bridge the gap between technical compliance and user experience.

Abstract
Deep learning has been extensively applied to medical imaging tasks over the past years, achieving outstanding results. However, the obscure reasoning of the models and the lack of supportive evidence causes both clinicians and patients to distrust the models' predictions, hindering their adoption in clinical practice. In recent years, the research community has focused on developing explanations capable of revealing a model's reasoning. Among various types of explanations, example-based explanations emerged as particularly intuitive for medical practitioners. Despite the intuitiveness and wide development of example-based explanations, no work provides a comprehensive review of existing example-based explainability works in the medical image domain. In this work, we review works that provide example-based explanations for medical imaging tasks, reflecting on their strengths and limitations. We identify the absence of objective evaluation metrics, the lack of clinical validation and privacy concerns as the main issues that hinder the deployment of example-based explanations in clinical practice. Finally, we reflect on future directions contributing towards the deployment of example-based explainability in clinical practice.

Abstract
We propose a hybrid formal verification approach that combines high-level deductive reasoning and circuit-based reasoning and apply it to highly optimized cryptographic assembly code. Our approach permits scaling up formal verification in two complementary directions: 1) it reduces the proof effort required for low-level functions where the computation logics are obfuscated by the intricate use of architecture-specific instructions and 2) it permits amortizing the effort of proving one implementation by using equivalence checking to propagate the guarantees to other implementations of the same computation using different optimizations or targeting different architectures. We demonstrate our approach via an extension to the EasyCrypt proof assistant and by revisiting formally verified implementations of ML-KEM in Jasmin. As a result, we obtain the first formally verified implementation of ML-KEM that offers performance comparable to the fastest non-verified implementation in x86-64 architectures.

Abstract
This article aims to explore menopausal women's views on empowerment in menopause-related femvertising on social media and to examine its outcomes for both women and brands. It includes a qualitative study comprising in-depth interviews with menopausal women who were active social media users (n = 15). The data were subject to content analysis using NVIVO software. The results reveal that menopause empowerment strategies on social media are perceived by women as a source of knowledge, facilitating social support, focusing on self-worth enhancement, and deconstructing stereotypes and taboos. Despite positive impacts such as self-esteem and self-confidence, these messages can also induce discomfort and feelings of segregation. Although the study highlights potential benefits for brands, including improved image and engagement, it also identifies risks such as skepticism, distrust, and customer loss. This research contributes to the femvertising and branding literature by addressing the largely overlooked segment of menopausal women. It highlights knowledge dissemination as a critical and previously underexplored dimension of femvertising and demonstrates that menopause empowerment carries distinct dynamics and consequences for both women and advertising brands, shedding light on the complexity of femvertising strategies. The findings can assist brands and social organizations aiming to develop more effective strategies for engaging menopausal audiences.

Abstract
Explainable AI (xAI) emerged as one of the ways of addressing the interpretability issues of the so-called black-box models. Most of the xAI artifacts proposed so far were designed, as expected, for human users. In this work, we posit that such artifacts can also be used by computer systems. Specifically, we propose a set of metrics derived from LIME explanations, that can eventually be used to ascertain the quality of each output of an underlying image classification model. We validate these metrics against quantitative human feedback, and identify 4 potentially interesting metrics for this purpose. This research is particularly useful in concept drift scenarios, in which models are deployed into production and there is no new labelled data to continuously evaluate them, becoming impossible to know the current performance of the model.