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
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.

Abstract

Abstract
The digitalisation of the public sphere is an ongoing process accelerated by the ubiquitousness of the internet. For the over a billion people estimated to live with an impairment, this digitalisation comes with barriers that can represent an altogether exclusion from the digital realm, hindering their full participation in society. This context should compel stakeholders involved in the development of digital products to consider accessibility as an essential requirement. However, that may not always be the case. This work is the product of a scoping literature review guided by the overarching topic of accessibility in the context of the web. After arguing that disability as a phenomenon might be more prevalent than one would think, it frames web accessibility as a human right that benefits all individuals, while also having important dimensions that businesses would regret ignoring.