Abstract
The objective of this paper is to delineate the ongoing doctoral research work that is focused on the development of a digital model intended to emulate the real-time operation of an electrolyzer that is powered by a DC/DC converter. The digital model of the converter and the proton exchange membrane (PEM) electrolyzer (EL) is presented, and it is based on an electrical equivalent model. A primary contribution of this study is the analysis of the errors resulting from the discretization process. Furthermore, the implementation and development of the digital model requires a comprehensive study of the errors and key affecting factors. Additionally, the formulation of a mechanism to reduce these errors is essential for advancing this topic. Preliminary results obtained using the digital emulator developed demonstrated its capacity to reproduce the voltage and current response applied to the electrolyzer with a reduced error compared to the continuous-time model.

Abstract
The increasing integration of Artificial Intelligence (AI) across various sectors of society raises complex ethical challenges requiring systematic and scalable oversight mechanisms. While tools such as AIF360 and Aequitas address specific dimensions, namely fairness, there remains a lack of comprehensive frameworks capable of auditing multiple ethical principles simultaneously. This paper introduces a multidimensional AI auditing tool designed to evaluate systems across key dimensions: fairness, explainability, robustness, transparency, bias, sustainability, and legal compliance. Unlike existing tools, our framework enables simultaneous assessment of these dimensions, supporting more holistic and accountable AI deployment. We demonstrate the tool’s applicability through use cases and discuss its implications for building trust and aligning AI development with fundamental ethical standards.

Abstract
Modelling complex information systems often entails the need for dealing with scenarios of inconsistency in which several requirements either reinforce or contradict each other. This lecture summarises recent joint work with Juliana Cunha, Alexandre Madeira and Ana Cruz on a variant of transition systems endowed with positive and negative accessibility relations, and a metric space over the lattice of truth values. Such structures are called paraconsistent transition systems, the qualifier stressing a connection to paraconsistent logic, a logic taking inconsistent information as potentially informative. A coalgebraic perspective on this family of structures is also discussed.

Abstract

Abstract
Jasmin is a programming language for high-speed and high-assurance cryptography. Correctness proofs of Jasmin programs are typically carried out deductively in EasyCrypt. This allows generality, modularity and composable reasoning, but does not scale well for low-level architecture-specific routines. CryptoLine offers a semi-automatic approach to formally verify algebraically-rich low-level cryptographic routines. CryptoLine proofs are self-contained: they are not integrated into higher-level formal verification developments. This paper shows how to soundly use CryptoLine to discharge subgoals in functional correctness proofs for complex Jasmin programs. We extend Jasmin with annotations and provide an automatic translation into a CryptoLine model, where most complex transformations are certified. We also formalize and implement the automatic extraction of the semantics of a CryptoLine proof to EasyCrypt. Our motivating use-case is the X-Wing hybrid KEM, for which we present the first formally verified implementation. © 2025 Copyright held by the owner/author(s).

Abstract
Carbon dioxide (CO2) plays a crucial role in the biosphere, acting as an indicator of anthropogenic activity. Its monitoring is fundamental for controlling air and water quality, preserving the environment and optimizing industrial processes. The preparation of a bright fluorescent scaffold, named rhodol, was optimized by employing microwave heating as an alternative heating source, achieving shorter reaction times and higher yields. Structural characterization was performed by nuclear magnetic resonance (NMR) and high-resolution mass spectrometry (HRMS-ESI). Its application to produce a fluorescent optical membrane for monitoring CO2 in gas (gCO2) and in water (dCO2) was explored. Two different setups are used for this purpose, and in both, the same optical response is observed: the membrane's fluorescence intensity decreases as the CO2 concentration increases. The sensor's reliability for dCO2 is demonstrated through testing concentrations ranging from 1 ppm to 100 ppm with minimal photobleaching (0.0026 dB) over 7500 data points with an integration time of 200 ms each. The sensor performance for dCO2 evaluation exhibits an experimental error of +/- 1.81 ppm, a response time of 2 min, a limit of detection of 0.6 ppm and a Stokes-shift of 90 nm for concentrations between 1 and 100 ppm. Monitoring of gCO2 using this membrane is hindered by changes in relative humidity (RH), hence the results for concentration between 0.3 % and 100 % of gCO2 were achieved by maintaining a consistent high value of RH. Our findings highlight the effectiveness of the optimized rhodol synthesis and its application in an optical membrane for reliable monitoring of CO2 in various environmental conditions.