We address the problem of verifying safety properties for iterative numerical programs. This problem amounts in, given a program and its specification (a pair of pre and post conditions), to find a strong enough inductive invariant allowing to establish correctness. The verification problem being undecidable in general, our aim is to provide a powerful invariant synthesis method allowing to handle automatically a large number of programs in practice. We propose such a method based on a data-driven approach that is enhanced with symbolic bounded reachability analysis. Our method builds on prior work we published in CAV'22 [6] where we defined an invariant learning procedure based on a new technique for generating relevant decision-tree attributes extracted from convex separators of samples (sets of program states seen as vectors of integers). In this work, we show that by coupling the previous method with a symbolic bounded model checker it is possible to improve significantly performances both in terms of running time and in the number of solved cases. The model checker can help in two ways: it might prove faster that a program is unsafe (by hitting error states), or more interestingly, it can provide interpolants (showing unreachability of error states) which can be used as attributes to speed-up the convergence of the learning procedure. We have implemented our new algorithm and shown that it is quite competitive with state-of-the-art tools such as Spacer, CVC4/5, solving globally more cases than these tools on the SyGuS and SV-COMP benchmarks.
Deterministic Suffix-reading Automata (DSA) were introduced recently as a concise model for regular languages. DSAs can succinctly capture formal specifications that are based on sequences of input actions (and not just single actions). For a concurrent system, specifications may further depend on combinations of input sequences seen across multiple components (ports). For such systems, DSAs consider all possible interleavings, resulting in large and unreadable automata. In this work, we enrich DSAs to include a ∥ operator in its transitions. The resulting multi-port DSAs (mDSAs) can succinctly represent concurrent suffix-based specifications. Subsequently, we extend mDSAs to produce outputs on transitions, and show that state reachability becomes PSPACE-complete in the presence of outputs. Finally, we apply our results to the formal analysis of Expressive Decision Tables (EDT) – an industry notation for specifying requirements of reactive systems.
We study the impact of restricting the class of separator problems on the look-compute-move mobile robot model hierarchy. In particular, we show that reachability specifications are sufficient to separate the semi-synchronous and the asynchronous model variants when robots agree on the unit-distance, but the two model variants are equivalent when considering terminating problems and no coordinate system agreement.
Federated learning (FL) is a distributed machine learning (ML) scheme that enables collaborative model training without compromising data privacy. In the TinyML community, communication is often prioritized over computation due to the limited bandwidth of the client devices. This paper aims to explore the rationale behind this perception by focusing on small models with approximately 1M parameters and investigating the effects of quantization and sparsification techniques for computation and communication purposes. We introduce mathematical models essential for estimating the time and energy consumption of computation and communication in an FL setup. Our research explores various configurations that impact FL efficiency, including model quantization and sparsification, processor frequency, batch sizes, and ML architecture. Notably, we demonstrate that for small models, communication energy can be negligible compared to computational energy. Consequently, contrary to existing literature, we propose that sparsification for communication may not be necessary as it introduces additional computational effort and energy consumption to achieve a target accuracy without significant gains in communication energy. This research enhances our understanding of the trade-offs between communication and computation in FL, particularly for small models like in TinyML. By emphasizing the importance of computational energy, our findings provide valuable insights for the design and optimization of FL systems.
In this paper, we consider the pattern formation problem of mobile agents in n× m dynamic grids, requiring k agents in the grid to stay at x designated (target) nodes to form some shape (pattern). We assume that at most one link is missing at each round. In this case, some agent’s movement may be always blocked and the agent cannot reach any target node. In addition, if the number k of agents is smaller than the number x of target nodes, several target nodes cannot be occupied. For this reason, focusing on the relationship between the values of k and x, we consider variants of the pattern formation problem in dynamic grids and examine how differences in these requirements and the number of agents influence the design and performance of algorithms. First, we consider the case of k ≤ x . In this case, we consider the approximate pattern formation problem, requiring at least k-1 ( x . In this case, we consider the exact pattern formation problem, requiring each of the x target nodes to be occupied. For this problem, we propose an algorithm to achieve exact pattern formation in O(kn+km+mn) rounds. In particular, when k - x is sufficiently large, we show that exact pattern formation can be achieved in (n+m) rounds.
To address the growing challenges of plant diseases and their impact on global food security, this study presents an innovative AI-driven workflow for disease detection and management. Leveraging the Plant Village dataset, our approach combines image classification, information retrieval, and response generation to provide actionable insights for farmers. The proposed system employs a hybrid VGG16/VGG19 model, achieving 96.12
Precise short-term blood glucose forecasting is critical for managing type 1 diabetes (T1D), enabling timely interventions to prevent complications. Complex deep learning models often rely on intricate architectures, increasing computational demands. We propose an ensemble model integrating XGBoost and LSTM, evaluated on the OhioT1DM dataset. Our preprocessing pipeline employs Kalman Filter smoothing, oversampling of high-glucose events, and feature engineering to extract lagged, rolling, and interaction features. The ensemble achieves an RMSE of 19.89 mg/dL, an MAE of 10.37 mg/dL, and 99.20
This paper reports the experimental results related to Lineage Event storage via smart-contracts deployed on private and public Blockchains. In our experiments we measure three key metrics: the cost to deploy the storage Smart Contract on the Blockchain. This metric captures the initial expenditure, typically in gas units, required to deploy the Smart Contract that facilitates Lineage Event storage, then the time and gas costs needed to store a Lineage Event. We investigated both single and multi-clients scenarios. We considered the following public Blockchains (largely used by industry): Hedera, Fantom, Harmony Shard0, Polygon Amoy, Ethereum Sepolia, Optimism Sepolia, Klaytn Baobab and Arbitrum Sepolia. Furthermore, we investigate the performances of Hyperledger Besu with different consensus algorithms as private Blockchains. Additionally, we explore an alternative case study involving hash-based batch Lineage Event storage using the QBFT consensus algorithm on a private Blockchain, and analyze the impact of client scaling on transaction times.
IoT applications are typically developed on serverless platforms and deployed for use with an underlying cloud service provider. Such applications typically use JSON files to represent sensor data and communicate with the IoT core using protocols like MQTT, MQTTSN, AMQP, HTTP, etc. The main functionality of an IoT application is implemented on the serverless platform including synchronous and asynchronous computations on the sensor data, notification services, accessing databases, data streaming, etc. We provide a framework to verify the requirements of these IoT applications specified as assertions. Our framework extends the notion of asynchronous call graphs of serverless applications to IoT applications by including notations for communication protocols, their QoS features, and message-passing properties, modeling both synchronous and asynchronous computations and services that support notifications, sensor actuation, etc. We then use this framework to verify assertions corresponding to correctness properties of the IoT applications.
Deepfake videos have been getting increasingly prevalent in recent years due to the presence of mobile apps and tools that can create highly realistic deepfake images/videos without any technical expertise. With the evolution of this domain of technology in the future, the quality and quantity of deepfake videos are expected to increase while making deepfake media a likely tool for disseminating misinformation. Due to these concerns, the deepfake video identification techniques are becoming essential. In this paper, we present a novel hybrid deeplearning model that combines two different models for deepfake identification. Our network employs Vgg-16 as a feature extractor and a Vision Transformer as the feature classifier. We train the Vision Transformer, as well as the feature extractors end to end manner, on the CelebDF and Faceforensics benchmarks. Notwithstanding a comparatively straightforward architecture, our network performs better than previous methods when evaluated on Faceforensics and CelebDF benchmark. Additionally, we introduce a novel random erasing image augmentation technique for training our network. We demonstrate that the proposed image augmentation technique improves the network's identification performance and reduces overfitting. Finally, we demonstrate that our network is able to learn from a substantially smaller amount of data.
In this paper, we study the problem of Byzantine fault-tolerant distributed set intersection and the importance of redundancy in solving this problem. Specifically, consider a distributed system with n agents, each of which has a local set. There are up to f agents that are Byzantine faulty. The goal is to find the intersection of the sets of the non-faulty agents. We are the first to consider the Byzantine set intersection problem with redundancy, and our problem formulation differs from prior works on related problems in different ways. We derive the Byzantine set intersection problem from the Byzantine optimization problem. We present the definition of 2f-set-redundancy for Byzantine set intersection, derived from 2f-redundancy in Byzantine optimization – a necessary condition for Byzantine optimization to be solvable in server-based systems [11]. We study Byzantine set intersection in decentralized (server-less) systems, presenting the necessary and sufficient condition on the communication graph for the Byzantine set intersection problem to be solvable with 2f-set-redundancy. Finally, we present solvability results for Byzantine optimization in decentralized systems, derived from our findings on Byzantine set intersection. Aside from the theoretical results, we also present two practical algorithms for Byzantine set intersection and optimization.
Coreference resolution aims to identify and link mentions that refer to a same entity in a text. However, Arabic coreference resolution remains under-explored due to data scarcity and linguistic complexity. Previous work has primarily relied on pre-trained language models, multilingual transformers, and cross-lingual transfer learning. Yet, these approaches often overlook syntactic and semantic structures, which are essential for capturing richer contextual representations. In this work, we focus on considering syntactic and semantic information to improve mentions linking for the Arabic language. We propose a heterogeneous graph-based model that jointly leverages these features to enhance Arabic coreference resolution. The suggested model encodes syntactic structure via dependency trees, using the Arabic parser, Camel-Parser 2.0. This model refines contextual representations by incorporating semantic role labeling (SRL), leading to a deeper semantic understanding. We conduct an analysis of our approach, comparing its performance with BERTbased methods and sequence-to-sequence models. Experiments on Arabic CoNLL-2012 shared task show that the suggested model outperforms BERT-based approaches in terms of F1 score and achieves competitive results against state-of-the-art sequence-to-sequence models.
Recent advancements in large language models (LLMs) have enabled the rise of LLM agents. These agents can act autonomously, make decisions, and perform tasks with minimal human input. However, one of the most pressing challenges is enabling these agents to interact with open-book data stored in real-world database environments to respond to user queries. In real-world settings, within a given organization data is not stored in a single, uniform system but is spread across multiple databases with different formats and structures. To interact with this open-book data, LLM agents must adapt to different schemas, process complex queries, and integrate information from multiple sources into a coherent response. Existing agentic frameworks are too generic and struggle to meet these demands. To address this, we propose a networked agent framework. In our approach, we consider a set of distributed specialized LLM agents, each dedicated to a specific database. These agents are orchestrated by a central router agent LLM. The router agent decomposes queries using chain-of-thought reasoning, delegates retrieval tasks to relevant agents, and integrates their structured responses into a coherent final answer. To validate our approach, we implemented a prototype across several widely used databases. Our experimental results demonstrate the effectiveness of our approach in accurately responding to complex queries in real-world data environments. These findings suggest that a networked LLM agent approach is a promising path forward for enabling interaction with complex data ecosystems.
We consider the parametric reachability problem (PRP) for families of networks described by vertex-replacement (VR) graph grammars, where network nodes run replicas of finite-state processes that communicate via binary handshaking. We show that the PRP problem for VR grammars can be effectively reduced to the PRP problem for hyperedge-replacement (HR) grammars at the cost of introducing extra edges for routing messages. This transformation is motivated by the existence of several parametric verification techniques for families of networks specified by HR grammars, or similar inductive formalisms. Our reduction enables applying the verification techniques for HR systems to systems with dense architectures, such as user-specified cliques and multi-partite graphs.
We present SmartShards: a new sharding algorithm for improving Byzantine tolerance and churn resistance in blockchains. Our algorithm places a peer in multiple shards to create an overlap. This simplifies cross-shard communication and shard membership management. We describe SmartShards, prove it correct and evaluate its performance. We propose several SmartShards extensions: defense against a slowly adaptive adversary, combining transactions into blocks, fortification against the join/leave attack.
Twin nodes in a static network capture the idea of being substitutes for each other for maintaining paths of the same length anywhere in the network. In dynamic networks, we model twin nodes over a time-bounded interval, noted ( ,d) -twins, as follows. A periodic undirected time-varying graph 𝒢=(G_t)_t∈ℕ of period p is an infinite sequence of static graphs where G_t=G_t+p for every t∈ℕ . For and d two integers, two distinct nodes u and v in 𝒢 are ( ,d) -twins if, starting at some instant, their outside neighbourhoods N(u)∖{u,v} and N(v)∖{u,v} have non-empty intersection and differ by at most d elements for consecutive instants. In particular when d=0 , u and v can act during the instants as substitutes for each other in order to maintain journeys of the same length in time-varying graph 𝒢 . It is known how to compute ( ,0) -twins in polynomial time by a centralized algorithm. In this paper we propose the first distributed deterministic algorithm enabling each node to enumerate its ( ,d) -twins in at most 2p rounds. We prove that the size of the messages used in our algorithm is at most O(δ _𝒢log n+log p) , where n is the total number of nodes and δ _𝒢 is the maximum degree of the graphs G_t ’s. Additionally, we prove that using randomized techniques borrowed from distributed hash function sampling the message size can be reduced w.h.p. down to O(log n+log p) .
We introduce a new approach in distributed learning, building on Hinton’s Forward-Forward (FF) algorithm to speed up the training of neural networks in distributed environments without losing accuracy. Unlike traditional methods that rely on forward and backward passes, the FF algorithm employs a dual forward pass strategy, eliminating the dependency among layers required during the backpropagation period, which prevents efficient parallelization of the training process. Although the original FF algorithm focused on its ability to match the performance of the backpropagation algorithm, this work aims to reduce the training time with pipeline parallelism. We propose three novel pipelined FF algorithms that speed up training 3.75 times on the MNIST dataset while maintaining accuracy when training a four-layer network with four compute nodes. These results show that FF is highly parallelizable and its potential in large-scale distributed/federated systems to enable faster training for larger and more complex models.
Large-scale, fault-tolerant, distributed systems are the backbone for many critical software services. Since they must execute correctly in a possibly adversarial environment with arbitrary communication delays and failures, the underlying algorithms are intricate. In particular, achieving consistency and data retention relies on intricate consensus (state machine replication) protocols. Ensuring the reliability of implementations of such protocols remains a significant challenge because of the enormous number of exceptional conditions that may arise in production. We propose a methodology and a tool called Netrix for testing such implementations that aims to exploit programmer’s knowledge to improve coverage, enables robust bug reproduction, and can be used in regression testing across different versions of an implementation. As evaluation, we apply our tool to a popular proof of stake blockchain protocol, Tendermint, which relies on a Byzantine consensus algorithm, a benign consensus algorithm, Raft, and BFT-Smart. We were able to identify deviations of the implementation from the protocol specification and validate corrections on an updated implementation. Additionally, we were able to confirm the presence of known bugs in previous versions.
We present a new symbolic static data race detection algorithm, which is defined as a code-to-code translation that injects code to monitor any accesses to shared memory locations. We implemented this algorithm in the LaDR tool as an extension of an existing lazy sequentialization schema which works well when used in tandem with bounded model checkers. We evaluated LaDR on the benchmarks from the data race demonstration category of SV-COMP 2024, and on safestack, a lock-free data structure that contains a rare ABA-related bug. LaDR finds more data races than all other tools participating in SV-COMP 2024, and is the only tool that can find a data race in safestack.
We study a dynamic assignment problem in a communication network where a set of mobile nodes called clients have to upload data packets to a set of static nodes called stations. Clients are restricted by a maximum delay between packet uploads, and stations by a maximum capacity at any given round of communication. The goal is to assign clients to stations in each round aiming to minimize various energy-related costs. The Station Assignment problem has been well studied from a centralized scheduling perspective. In this work we consider the application of Multi-Agent Reinforcement Learning (MARL) so that each client can self-assign to a station independently using only local information. MARL is challenging because the decisions of clients are affected by the concurrent decisions of other clients. In this work, as a step towards a better understanding of the feasibility of MARL for distributed assignment problems, we study Distributed Station Assignment experimentally applying Independent Proximal Policy Optimization (IPPO) for various scenarios.
