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
Detecting anomalies in Waste transportation networks is vital for uncovering illegal or unsafe activities, that can have serious environmental and regulatory consequences. Identifying anomalies in such networks presents a significant challenge due to the limited availability of labeled data and the subtle nature of illicit activities. Moreover, traditional anomaly detection methods relying solely on individual transaction data may overlook deeper, network-level irregularities that arise from complex interactions between entities, especially in the absence of labeled data. This study explores anomaly detection in a waste transport network using unsupervised learning, enhanced by limited supervision and enriched with network structure information. Initially, unsupervised models like Isolation Forest, K-Means, LOF, and Autoencoders were applied using statistical and graph-based features. These models detected outliers without prior labels. Later, information on a few confirmed anomalous users enabled weak supervision, guiding feature selection through statistical tests like Kolmogorov-Smirnov and Anderson-Darling. Results show that models trained on a reduced, graph-focused feature set improved anomaly detection, particularly under extreme class imbalance. Isolation Forest notably ranked known anomalies highly. Ego network visualizations supported these findings, demonstrating the value of integrating structural features and limited labels for identifying subtle, relational anomalies.

Abstract
Capricious data streams make no assumptions on feature space dynamics and are mainly handled based on feature correlation, linear classifier or ensemble of trees. There exist deficiencies such as limited learning capacity, high time cost and low interpretability. To enhance effectiveness and efficiency, capricious data streams are handled through a single tree in this paper, and the proposed algorithm is named OCFHT (Online learning from Capricious data streams with Flexible Hoeffding Tree). OCFHT does not rely on the correlation pattern among features and can achieve non-linear modeling. Its performance is verified by various experiments on 18 public datasets, showing that it is not only more accurate than state-of-the-art algorithms, but also runs faster.

Abstract
This article presents the development of a tethered fixed-wing tail-sitter VTOL (Vertical Take-Off and Landing) Unmanned Aerial Vehicle system. The design focuses on improving energy efficiency by utilizing the wings to harness wind power, similar to a kite, while maintaining VTOL functionality. A distinguishing feature is the purpose-built autopilot system, with custom hardware and software components specifically engineered for this application. The study presents the system identification process for obtaining five MIMO (Multiple-Input Multiple-Output) transfer functions that characterize the dynamics between roll-yaw commands and responses, including the tether angle feedback. To address the inherent coupling effects and uncertainties in the system, robust mixed sensitivity (H-infinity) MIMO controllers are developed. The controllers were validated through both simulations and experimental flights, demonstrating effective performance in handling cross-coupling effects and maintaining stability under various operating conditions. According to flight test findings, the system can precisely manage the tether angle while adjusting for ground effect disturbances. This allows for accurate tethered navigation, a stable attitude, and the maintenance of an adequate yaw heading.

Abstract
Despite their extreme sensitivity, speckle-based fiber optical sensors are typically limited by the camera frame rate and dynamic range. In this context, recent developments in event-based sensors make them a promising and affordable tool for high-speed interrogation for such class of sensors, offering a low-latency approach to detecting dynamic changes in illumination patterns, well-suited for fast interrogation with frequency response up to the MHz range. In this manuscript, we investigate the potential of using an event-based vision sensor (EVS) as an interrogator for a speckle-based optical fiber sensor operating at 532nm to detect vibrations induced by an off-the-shelf sound speaker. In contact with the fiber, these vibrations induce dynamic changes in the speckle pattern, which are tracked by the EVS and processed to construct temporal frames with timestamps below 100 mu s. Approximating the differential operator of the deformation in the linear regime, we show a successful reconstruction of the acoustic signal for two illustrative case studies: i)a single-frequency signal at 1.2 KHz and ii)a linear ramp between 300 Hz to 2.5 kHz. The results demonstrate the ability to accurately identify not only the fundamental frequencies but also their harmonics generated by the speaker up to 5 KHz, paving an innovative path to harness the potential of speckle-based sensors in multiple scenarios of optical metrology and dynamic sensing applications.

Abstract
Software testing is an integral part of modern software development. Testing frameworks are part of the toolset of any software language allowing programmers to test their programs in order to detect bugs. Unfortunately, there is no work on testing in attribute grammars. In this paper we combine the powerful property-based testing technique with the attribute grammar formalism. In such property-based attribute grammars, properties are defined on attribute instances. Properties are tested on large sets of randomly generated (abstract syntax) trees by evaluating their attributes. We present an implementation that relies on strategies to express property-based attribute grammars. Strategies are tree-based recursion patterns that are used to encode logic quantifiers defining the properties.