arXiv subjects

Fatemeh Ghassemi

Publications and source records attributed to Fatemeh Ghassemi.

13 recordsLinked to original sources

arXiv2026

Behavioral Analysis of Timed Actors using Syntactic Slice Equivalence

Tiny twins are compact behavioral models derived from timed actor models for selected observable messages. When a source model evolves, regenerating its tiny twin requires state-space exploration and reduction even if the relevant behavior is unchanged. We present a static analysis for Timed Rebeca that compares backward slices of Rebeca dependence graphs for a given set of observable message names. For the Zeno-free fragment with after annotations and no delay statements, we prove that slice equivalence implies weak timed bisimulation under the selected observations. This preserves observable actions and total elapsed time across internal transitions, allowing the existing tiny twin to be reused. We evaluate the implementation on ten benchmark models paired with revisions that preserve their observable slices. The cost of static comparison depends on the size of the graphs representing source statements and their dependencies, while tiny-twin generation depends on the number of reachable states and transitions. This difference is reflected in the measurements: static comparison takes less than one second using tens of megabytes of memory, while tiny-twin generation can take over an hour and use hundreds of gigabytes.

cs.PL↗

arXiv2026

SieveFL: Hierarchical Runtime-Aware Pruning for Scalable LLM-Based Fault Localization

Automated fault localization requires connecting an observed test failure to the responsible method across thousands of candidates--a task that purely statistical approaches handle with limited precision and that LLMs cannot yet handle at full project scale due to prohibitive token cost and signal dilution. We present SieveFL, a five-stage hierarchical framework that resolves this tension through aggressive pre-LLM filtering. SieveFL converts a failing test into a natural-language failure description, uses dense vector retrieval to narrow the search to a small set of suspicious files, and then eliminates any method not executed during the failing test via JaCoCo runtime traces. Only the surviving candidates are passed to the LLM, which screens each method individually and re-ranks the confirmed suspects in a single comparative pass. We evaluate SieveFL on 395 bugs from Defects4J v1.2.0 using a mid-sized, openly available MoE model deployed on a commodity workstation (32 GB RAM, 8 GB GPU) via Ollama--no frontier APIs or datacenter hardware required. Treating 12 incomplete runs as failures, SieveFL achieves Top-1 accuracy of 41.8% (165/395 bugs) and an MRR of 0.469, outperforming the strongest prior agent-based baseline (AgentFL) by 2.1 pp in Top-1. Runtime pruning removes 79% of candidate methods and reduces input token consumption by 49%, while simultaneously improving ranking quality: Top-1 is preserved exactly and Top-3 through Top-10 improve by up to 2.4 pp. These results demonstrate that, with the right filtering architecture, capable fault localization does not require proprietary frontier models.

cs.SE↗

arXiv2025

A Comprehensive Forecasting-Based Framework for Time Series Anomaly Detection: Benchmarking on the Numenta Anomaly Benchmark (NAB)

Time series anomaly detection is critical for modern digital infrastructures, yet existing methods lack systematic cross-domain evaluation. We present a comprehensive forecasting-based framework unifying classical methods (Holt-Winters, SARIMA) with deep learning architectures (LSTM, Informer) under a common residual-based detection interface. Our modular pipeline integrates preprocessing (normalization, STL decomposition), four forecasting models, four detection methods, and dual evaluation through forecasting metrics (MAE, RMSE, PCC) and detection metrics (Precision, Recall, F1, AUC). We conduct the first complete evaluation on the Numenta Anomaly Benchmark (58 datasets, 7 categories) with 232 model training runs and 464 detection evaluations achieving 100\% success rate. LSTM achieves best performance (F1: 0.688, ranking first or second on 81\% of datasets) with exceptional correlation on complex patterns (PCC: 0.999). Informer provides competitive accuracy (F1: 0.683) with 30\% faster training. Classical methods achieve perfect predictions on simple synthetic data with 60 lower cost but show 2-3 worse F1-scores on real-world datasets. Forecasting quality dominates detection performance: differences between detection methods (F1: 0.621-0.688) are smaller than between forecasting models (F1: 0.344-0.688). Our findings provide evidence-based guidance: use LSTM for complex patterns, Informer for efficiency-critical deployments, and classical methods for simple periodic data with resource constraints. The complete implementation and results establish baselines for future forecasting-based anomaly detection research.

cs.LG↗

arXiv2025

Automated Repair of C Programs Using Large Language Models

This study explores the potential of Large Language Models (LLMs) in automating the repair of C programs. We present a framework that integrates spectrum-based fault localization (SBFL), runtime feedback, and Chain-of-Thought-structured prompting into an autonomous repair loop. Unlike prior approaches, our method explicitly combines statistical program analysis with LLM reasoning. The iterative repair cycle leverages a structured Chain-of-Thought (CoT) prompting approach, where the model reasons over failing tests, suspicious code regions, and prior patch outcomes, before generating new candidate patches. The model iteratively changes the code, evaluates the results, and incorporates reasoning from previous attempts into subsequent modifications, reducing repeated errors and clarifying why some bugs remain unresolved. Our evaluation spans 3,902 bugs from the Codeflaws benchmark, where our approach achieves 44.93% repair accuracy, representing a 3.61% absolute improvement over strong state-of-the-art APR baselines such as GPT-4 with CoT. This outcome highlights a practical pathway toward integrating statistical program analysis with generative AI in automated debugging.

cs.SE↗

arXiv2025

OptiGradTrust: Byzantine-Robust Federated Learning with Multi-Feature Gradient Analysis and Reinforcement Learning-Based Trust Weighting

Federated Learning (FL) enables collaborative model training across distributed medical institutions while preserving patient privacy, but remains vulnerable to Byzantine attacks and statistical heterogeneity. We present OptiGradTrust, a comprehensive defense framework that evaluates gradient updates through a novel six-dimensional fingerprint including VAE reconstruction error, cosine similarity metrics, $L_2$ norm, sign-consistency ratio, and Monte Carlo Shapley value, which drive a hybrid RL-attention module for adaptive trust scoring. To address convergence challenges under data heterogeneity, we develop FedBN-Prox (FedBN-P), combining Federated Batch Normalization with proximal regularization for optimal accuracy-convergence trade-offs. Extensive evaluation across MNIST, CIFAR-10, and Alzheimer's MRI datasets under various Byzantine attack scenarios demonstrates significant improvements over state-of-the-art defenses, achieving up to +1.6 percentage points over FLGuard under non-IID conditions while maintaining robust performance against diverse attack patterns through our adaptive learning approach.

cs.LG↗

arXiv2025

Hybrid Rebeca Revisited

Hybrid Rebeca is a modeling framework for asynchronous event-based cyber-physical systems (CPSs). In this work, we extend Hybrid Rebeca to allow the modeling of non-deterministic time behavior. Besides the syntactical extension, we formalize the semantics of the extended language in terms of Timed Transition Systems, and adapt a reachability analysis algorithm originally designed for hybrid automata to be applicable to Hybrid Rebeca models. We prove the soundness of our approach and illustrate its applicability on a case study. The case study demonstrates that our dedicated algorithm is clearly superior to the alternative approach of transforming Hybrid Rebeca models to hybrid automata as an intermediate model and then applying the original reachability analysis method to this intermediate transformed models.

cs.FL↗

arXiv2022

Specification and Verification of Timing Properties in Interoperable Medical Systems

To support the dynamic composition of various devices/apps into a medical system at point-of-care, a set of communication patterns to describe the communication needs of devices has been proposed. To address timing requirements, each pattern breaks common timing properties into finer ones that can be enforced locally by the components. Common timing requirements for the underlying communication substrate are derived from these local properties. The local properties of devices are assured by the vendors at the development time. Although organizations procure devices that are compatible in terms of their local properties and middleware, they may not operate as desired. The latency of the organization network interacts with the local properties of devices. To validate the interaction among the timing properties of components and the network, we formally specify such systems in Timed Rebeca. We use model checking to verify the derived timing requirements of the communication substrate in terms of the network and device models. We provide a set of templates as a guideline to specify medical systems in terms of the formal model of patterns. A composite medical system using several devices is subject to state-space explosion. We extend the reduction technique of Timed Rebeca based on the static properties of patterns. We prove that our reduction is sound and show the applicability of our approach in reducing the state space by modeling two clinical scenarios made of several instances of patterns.

cs.LO↗

arXiv2019

ConsiDroid: A Concolic-based Tool for Detecting SQL Injection Vulnerability in Android Apps

In this paper, we present a concolic execution technique for detecting SQL injection vulnerabilities in Android apps, with a new tool we called ConsiDroid. We extend the source code of apps with mocking technique, such that the execution of original source code is not affected. The extended source code can be treated as Java applications and may be executed by SPF with concolic execution. We automatically produce a DummyMain class out of static analysis such that the essential functions are called sequentially and, the events leading to vulnerable functions are triggered. We extend SPF with taint analysis in ConsiDroid. For making taint analysis possible, we introduce a new technique of symbolic mock classes in order to ease the propagation of tainted values in the code. An SQL injection vulnerability is detected through receiving a tainted value by a vulnerable function. Besides, ConsiDroid takes advantage of static analysis to adjust SPF in order to inspect only suspicious paths. To illustrate the applicability of ConsiDroid, we have inspected randomly selected 140 apps from F-Droid repository. From these apps, we found three apps vulnerable to SQL injection. To verify their vulnerability, we analyzed the apps manually based on ConsiDroid's reports by using Robolectric.

cs.SE↗

arXiv2019

Hybrid Rebeca: Modeling and Analyzing of Cyber-Physical Systems

In cyber-physical systems like automotive systems, there are components like sensors, actuators, and controllers that communicate asynchronously with each other. The computational model of actor supports modeling distributed asynchronously communicating systems. We propose Hybrid Rebeca language to support modeling of cyber-physical systems. Hybrid Rebeca is an extension of actor-based language Rebeca. In this extension, physical actors are introduced as new computational entities to encapsulate physical behaviors. To support various means of communication among the entities, the network is explicitly modeled as a separate entity from actors. We derive hybrid automata as the basis for analysis of Hybrid Rebeca models. We demonstrate the applicability of our approach through a case study in the domain of automotive systems. We use SpaceEx framework for the analysis of the case study.

eess.SY↗

arXiv2017

An Efficient Loop-free Version of AODVv2

Ad hoc On Demand distance Vector (AODV) routing protocol is one of the most prominent routing protocol used in Mobile Ad-hoc Networks (MANETs). Due to the mobility of nodes, there exists many revisions as scenarios leading to the loop formation were found. We demonstrate the loop freedom property violation of AODVv2-11, AODVv2-13, and AODVv2-16 through counterexamples. We present our proposed version of AODVv2 precisely which not only ensures loop freedom but also improves the performance.

cs.NI↗

arXiv2017

Verification of Asynchronous Systems with an Unspecified Component

Component-based systems evolve as a new component is added or an existing one is replaced by a newer version. Hence, it is appealing to assure the new system still preserves its safety properties. However, instead of inspecting the new system as a whole, which may result in a large state space, it is beneficial to reuse the verification results by inspecting the newly added component in isolation. To this aim, we study the problem of model checking component-based asynchronously communicating systems in the presence of an unspecified component against safety properties. Our solution is based on assume-guarantee reasoning, adopted for asynchronous environments, which generates the weakest assumption. If the newly added component conforms to the assumption, then the whole system still satisfies the property. To make the approach efficient and convergent, we produce an overapproximated interface of the missing component and by its composition with the rest of the system components, we achieve an overapproximated specification of the system, from which we remove those traces of the system that violate the property and generate an assumption for the missing component. We have implemented our approach on two case studies. Furthermore, we compared our results with the state of the art direct approach. Our resulting assumptions are smaller in size and achieved faster.

cs.FL↗

arXiv2017

Reliable Restricted Process Theory

Malfunctions of a mobile ad hoc network (MANET) protocol caused by a conceptual mistake in the protocol design, rather than unreliable communication, can often be detected only by considering communication among the nodes in the network to be reliable. In Restricted Broadcast Process Theory, which was developed for the specification and verification of MANET protocols, the communication operator is lossy. Replacing unreliable with reliable communication invalidates existing results for this process theory. We examine the effects of this adaptation on the semantics of the framework with regard to the non-blocking property of communication in MANETs, the notion of behavioral equivalence relation and its axiomatization. We illustrate the applicability of our framework through a simple routing protocol. To prove its correctness, we introduce a novel proof process, based on a precongruence relation.

cs.LO↗

arXiv2017

Modeling and Efficient Verification of Wireless Ad hoc Networks

Wireless ad hoc networks, in particular mobile ad hoc networks (MANETs), are growing very fast as they make communication easier and more available. However, their protocols tend to be difficult to design due to topology dependent behavior of wireless communication, and their distributed and adaptive operations to topology dynamism. Therefore, it is desirable to have them modeled and verified using formal methods. In this paper, we present an actor-based modeling language with the aim to model MANETs. We address main challenges of modeling wireless ad hoc networks such as local broadcast, underlying topology, and its changes, and discuss how they can be efficiently modeled at the semantic level to make their verification amenable. The new framework abstracts the data link layer services by providing asynchronous (local) broadcast and unicast communication, while message delivery is in order and is guaranteed for connected receivers. We illustrate the applicability of our framework through two routing protocols, namely flooding and AODVv2-11, and show how efficiently their state spaces can be reduced by the proposed techniques. Furthermore, we demonstrate a loop formation scenario in AODV, found by our analysis tool.

cs.NI↗