Neural networks have been adopted in various security-critical systems, prompting interest in verifying their security properties given their vulnerability to attacks and manipulation. This paper relies on a formal approach to verify specific security properties of neural networks. The approach involves three main steps: (1) expressing security objectives as properties of a modeled neural network using a technology-independent specification language, (2) implementing the developed model in a suitable tool language for analysis, and (3) identifying a set of security requirements necessary to realize the target security objectives. We employ first-order and modal logic as abstract, technology-independent formalisms and Alloy as a tool-supported modeling language. To validate our work, we investigate a set of representative security objectives categorized under Confidentiality, Integrity, Availability, and Authenticity. We apply these objectives to a specific use case within the unmanned aircraft domain.
Big data analytics offer opportunities in a variety of domains but require high-performance computing. Mainstream frameworks such as MapReduce and Apache Spark provide programming paradigms where parallelism remains mainly implicit. The SyDPaCCframework for the Rocqproof assistant takes a similar approach in the sense that users write specifications as possibly inefficient sequential programs, potentially with high computational complexity, which are then transformed into efficient parallel functional programs. These programs are written with algorithmic skeletons that are higher-order functions implemented in parallel on distributed data structures. The output programs are constructed step-by-step by applying transformation theorems. Leveraging Rocqtype classes, the application of transformation theorems is partly automated. However, even when no automatic transformation can be found with the framework, it is still possible to leverage the automatic transformation of specific sequential functions and their compositions into a composition of corresponding algorithmic skeletons. In this case, the SyDPaCCuser has to identify an efficient sequential program, equivalent to the original specification, that is written as a composition of functions for which corresponding algorithmic skeletons are registered. The parallelization is performed automatically by the framework. The current version of the framework is presented through the verified derivation of a parallel program for the maximum segment sum problem. This derivation introduces the verified par_scanr algorithmic skeleton, which is then used by the automatic parallelization phase of SyDPaCC. The extracted program is evaluated on a parallel machine.
Software quality assurance is pivotal in safety-critical domains such as railway systems, where failures could have catastrophic consequences. In this context, the train control and management system, which enables communication and control across multiple subsystems (such as doors and information panels) within a modern train, and its software must undergo rigorous validation. Alstom Rail Sweden AB employs a digital twin infrastructure to simulate and validate train control and management system software. While this setup improves system-level testing, root-cause analysis of test failures remains a manual, time-consuming bottleneck. In this study, we explore the potential of large language models to automate root cause analysis by interpreting test execution logs generated during digital twin-based testing. We benchmark nine state-of-the-art large language models: Aion−1.0, DeepSeek R1, DeepSeek V3 0324, Mistral Small 3.1 24B, GPT o3-mini, Gemini 2.5 Pro Experimental, QwQ 32B, Gemini 2.0 Flash Experimental, and Amazon Nova 2 Lite using zero-shot chain-of-thought prompting to assess their ability to reason about fault patterns in real-world industrial test execution logs. The logs were sourced from Alstom’s digital twin-based testing environment and captured complex operational behaviour typical of embedded, safety-critical systems. Our results showed that long-context LLMs tended to achieve higher accuracy than smaller models. Gemini 2.5 Pro Experimental achieved the best performance with 66.7
Predicting large single-session moves in an equity index is considerably harder than predicting whether the next day will close up or down. Large moves occur infrequently, their likelihood depends heavily on the prevailing market regime, and they are heavily outnumbered by ordinary trading sessions. This paper studies a predictive setup that handles two related tasks together: next-day directional movement and the detection of abnormally large single-day moves. Our experiments draw on daily data for three major Indian indices, NIFTY50, NIFTYBANK, and NIFTYIT, spanning 17 September 2007 to 21 July 2025. We evaluate the setup across these indices and across several label definitions under two validation regimes: a fixed train–test split and a rolling-window protocol meant to capture non-stationarity and changes in market state over time. We report minority-sensitive classification metrics (Precision, Recall, F1) together with Accuracy, and we run standard strategy backtests reporting Total Return and Sharpe Ratio so that economic usefulness can be assessed alongside statistical fit. The results separate into two regimes. Directional prediction is fairly stable across both indices and split protocols, whereas rare-event detection is much more fragile: it responds to the degree of class imbalance and to shifts in market state, and its Accuracy can remain high even as event-level F1 collapses, a weakness the backtests then confirm. We conclude that the genuinely difficult part of deployment is tail-event detection rather than directional forecasting, and that a credible evaluation must rely on event-sensitive metrics and time-aware validation; without them, performance under heavy imbalance is easily overstated.
Federated Learning (FL) enables collaborative model training across distributed IoT devices without sharing raw data, thereby enhancing privacy. However, unreliable or inefficient client participation can hinder convergence, increase energy consumption, and expose the system to security threats. Most existing client selection strategies rely on centralized architectures, which introduce bottlenecks, single points of failure, and poor scalability. This paper presents a decentralized, leader-based client selection framework designed for resource-constrained IoT environments. In our approach, local leaders are dynamically elected within each network to coordinate the collection of node resource profiles. Each leader employs a lightweight Long Short-Term Memory (LSTM) model to predict future resource availability and identify the most reliable clients for participation in FL rounds. Unlike centralized methods, our framework avoids overloading any single node and ensures fault-tolerant, adaptive selection through continuous monitoring and helper-assisted data gathering. The decentralized protocol improves both efficiency and resilience in heterogeneous, real-world IoT settings. Simulation results using the MNIST dataset show that our method achieves faster convergence (up to 27
