Formal verification is a vital method for ensuring software quality, which relies on precise system specifications, especially for safety-critical systems. However, manually crafting formal specifications is error-prone and inefficient, significantly limiting the widespread application of verification techniques. Existing studies have explored Large Language Models (LLMs) to enhance the efficiency of automatic formal specifications generation, but few of them considered non-canonical patterns in natural language requirements, such as partially missing atomic propositions, quantified enumeration, and implicit negation in conditionals. In real-world scenarios, such patterns frequently occur in requirement documents. Moreover, the stochastic nature of LLMs prevents guaranteed correctness in their output. In this paper, we propose a novel approach for automatically generating Linear Temporal Logic (LTL) formulas from non-canonical natural language requirements. First, we develop an interactive reasoning mechanism based on LLMs prompt engineering, enabling users to iteratively refine atomic propositions and logical structures through human-AI collaboration. Second, to address the scarcity of datasets close to real-world for evaluation, we summarize several logically implicit patterns from industrial requirement documents, and propose a method for generating Natural Language (NL)-LTL pairs containing these patterns using the LLMs. Subsequently, we implement a tool that automates LTL formula generation and facilitates human–LLM interaction. Finally, we validate our approach through experiments on translation accuracy using two state-of-the-art LLMs (ChatGPT-4o and DeepSeek-R1), demonstrating the effectiveness of our method.
In the era of large language model (LLM) applications, the widespread deployment of intelligent systems in privacy-critical domains (e.g., mental health, finance) poses significant challenges for data privacy and the limited availability of labeled data. To address these issues, FL-DPLoRA integrates federated learning (FL), transfer learning (TL), and differential privacy (DP) into a unified training paradigm. Specifically, it leverages a public dataset to pretrain a base model and then employs a low-rank adaptation (LoRA) mechanism for local fine-tuning at each client, with Gaussian noise injection during gradient aggregation to enforce rigorous differential privacy guarantees during updates. Our framework significantly reduces communication overhead by transmitting only a small set of adapted parameters while preserving data confidentiality and minimizing communication costs. We provide formal privacy guarantees and demonstrate the effectiveness of FL-DPLoRA through comprehensive experiments in mental health detection tasks. The results show that FL-DPLoRA achieves competitive performance with minimal degradation under strict privacy budgets and reduces communication costs by more than 99.7% compared to conventional methods. This validates FL-DPLoRA as a broadly applicable solution for safely deploying LLMs in sensitive, distributed environments.
Controller synthesis is a formal method approach for automatically generating Labeled Transition System (LTS) controllers that satisfy specified properties. The efficiency of the synthesis process, however, is critically dependent on exploration policies. These policies often rely on fixed rules or strategies learned through reinforcement learning (RL) that consider only a limited set of current features. To address this limitation, this paper introduces GCRL, an approach that enhances RL-based methods by integrating Graph Neural Networks (GNNs). GCRL encodes the history of LTS exploration into a graph structure, allowing it to capture a broader, non-current-based context. In a comparative experiment against state-of-the-art methods, GCRL exhibited superior learning efficiency and generalization across four out of five benchmark domains, except one particular domain characterized by high symmetry and strictly local interactions.
Software defect prediction plays a vital role in software development. During the process of software updates and iterations, it helps developers anticipate potential defects in advance, thereby reducing unnecessary consumption of human, material, and time resources, while optimizing the allocation efficiency of Software Quality Assurance (SQA) resources. Given the widespread use of generative artificial intelligence in code development, effective software defect prediction has become increasingly important. Most previous studies primarily constructed defect prediction models using traditional metric-based features. However, in recent years, research focusing on semantic feature-based defect prediction has gained increasing attention, with researchers leveraging deep learning to automatically extract deep semantic information from source code. Nevertheless, existing approaches often rely on a single type of source code representation, overlooking the advantages and potential contributions of diverse features. To address this issue, this paper proposes a software defect prediction method based on multi-feature fusion, which incorporates multiple types of code representations to capture semantic information from different perspectives. The proposed model, DP-TACT, utilizes a multi-scale Convolutional Neural Network (Multiscale CNN) and Bidirectional Long Short-Term Memory (BiLSTM) network to process Abstract Syntax Tree (AST) and Full-token features. It also employs a Multi-head SelfAttention mechanism to capture critical information. Additionally, a Graph Convolutional Network (GCN) is used to process Control Flow Graph (CFG) features. Finally, traditional features are integrated to validate the effectiveness of the feature fusion strategy. The model is evaluated on the PROMISE dataset, and experimental results demonstrate that the proposed approach outperforms baseline models across multiple metrics.
Existing backdoor attack methods predominantly rely on single static code features as triggers, rendering them easily detectable and achieving limited efficacy. To address this critical vulnerability, we propose a novel hybrid trigger mechanism that synergistically integrates static code structures, dynamic execution characteristics, and function signature patterns, coupled with an adaptive backdoor injection algorithm. Experimental evaluations demonstrate that our approach maintains model functionality while achieving exceptional attack performance. Specifically, the static-function signature hybrid configuration attains an average attack success rate of 99.0 % on CodeBert models, representing a 13-percentagepoint improvement over dynamic-only baselines. Furthermore, the static-function signature hybrid mechanism consistently outperforms conventional dynamic triggers across parameter configurations in GraphCodeBert models, achieving Attack Success Rate gains of 12-12.7 percentage points. Crucially, the static-dynamic hybrid configuration exhibits robust defense evasion capabilities when confronted with advanced detection systems such as Spectral Signatures, attaining a 94 % evasion success rate while achieving a 40 % relative reduction in detection likelihood compared to static-only baselines. Our study reveals critical security risks in code intelligence systems and provides essential insights for designing next-generation defense frameworks that are resilient to adaptive adversarial threats.
As the application of Deep Reinforcement Learning (DRL) systems gradually expands, improving their reliability becomes an important issue. Currently, improving the reliability of DRL systems primarily relies on testing techniques aimed at generating test cases to uncover as many bugs as possible. However, these techniques cannot guarantee the resolution of various bugs that may arise during the execution phase. Therefore, it is necessary to employ fault-tolerant techniques during the design phase as a means to enhance the reliability of DRL systems. This study focuses on developing a fault-tolerant framework for continuous DRL systems, based on the principles of N-Version Programming (NVP). Specifically, it investigates the critical design elements of DRL systems and proposes three types of independent factors, including DNN architecture, hyperparameter and training algorithm, to construct single version models. Subsequently, different mechanisms are explored to combine these models into the framework. Our empirical study conducted on three classical DRL tasks demonstrates that our proposed framework can achieve impressive fault tolerance and validates the feasibility of our proposed independent factors. To the best of our knowledge, this study first explores the fault-tolerant techniques in DRL systems, laying the groundwork for subsequent research on fault-tolerant frameworks in this field.
With its ability to alleviate the test oracle problem, Metamorphic Testing (MT) has been widely used to test Deep Neuron Networks (DNN). To improve failure detection ability of MT, recently, researchers have proposed uncertainty based methods to select Metamorphic test case Pairs (MPs) that are more likely to violate metamorphic relations. However, in these methods, the DNN under test needs to be frequently invoked to obtain the output probabilities of test cases for uncertainty calculation, potentially limiting their adoptions in resource-constrained test scenarios where the number of DNN calls should be minimized. To further boost the costeffectiveness of MT, in this paper, we propose MPSS, a black-box method that relies on a surrogate model to select failure-revealing MPs. In particular, MPSS aims to train and iteratively optimize a support vector machine to approximate the DNN classification boundaries in the latent space. Then, by analyzing the relative positions of both source and followup test cases of each MP to such boundaries, MPSS can effectively estimate whether the execution of this MP will lead to a metamorphic relation violation without actually calling the DNN model. Experimental results show that MPSS can increase the cost-effectiveness of MP selection by maximizing detected failures while minimizing DNN calling times under given test budgets in various situations.
Identifying interaction scenarios between a system and its actors from the high-level requirements and forming use case basic flows is crucial in requirement refinement. Traditional manual methods often yield incomplete or inaccurate flows due to engineers' limited domain expertise, while rule-based methods-relying on predefined parsing rules-suffer from linguistic ambiguities and domain-dependent limitations. Although large language model (LLM) approaches leverage rich domain knowledge and robust natural language processing, they are constrained by input length, generation instability, and the risk of out-of-system outputs, frequently resulting in context-unaware or irrelevant flows. To overcome these challenges, this paper proposes BFGen to generate context-compliant basic flows strictly adhering to domain constraints and requirement boundaries. BFGen employs LLMs to accurately extract domain-specific terms and interactions, and integrates a Relational Graph Attention Network with attention preservation factors to model logical dependencies and domain constraints effectively. Empirical evaluations on 13 public and 7 industrial datasets show that BFGen outperforms leading baselines by approximate to 14% in Precision, approximate to 7-25% in Recall, approximate to 11-30% in F1 Score, and approximate to 10-19% in AUC. Furthermore, our evaluations confirm the effectiveness of both the LLM module and the attention preservation factors, and assess the impact of requirement completeness on the performance of BFGen.
Organizations migrating monolithic applications to microservice architectures often face significant challenges in both decomposition and refactoring phases. While the decomposition step has received considerable automation research, refactoring remains predominantly manual, creating bottlenecks in migration efforts and preventing runtime-based and a more realistic evaluation of decomposition techniques. We propose a fully automated refactoring methodology that complements existing decomposition approaches. Our technique implements an ID-based and DTO-based hybrid design for inter-service communication and leverages Large Language Models (LLMs) for decision making, code analysis and code generation. Taking a monolith's source code and decomposition plan as input, our approach identifies “API classes” that cross service boundaries, selects their appropriate target design among the ID and DTO based methods and then automatically generates the necessary communication components—API contracts, server-side endpoints, and client-side proxies. This approach balances the preservation of the monolith's workflow consistency through the ID-based design and minimizing the overhead and complexity of the cross-service interactions through the DTO-based design. A qualitative evaluation using three benchmark applications demonstrates our approach's feasibility and advantages over related work.
The wide range of applications of deep neural networks in image recognition, medical diagnosis, and safetycritical areas makes it essential to test them adequately. However, traditional software testing methodologies proves challenging due to the inherent complex topology and blackbox characteristics of DNNs. Existing testing techniques (e.g., coverage-guided testing, fuzzy testing, etc.) generally lack guidance mechanisms for generating samples and similar fault characteristics. To address the lack of guidance and constraints on the generated samples, a conditional metric, the Gini impurity, is introduced to generate test inputs with high fault detection rates. In addition, many randomly generated similar and redundant test case samples ignore the problem of generating image diversity, and to solve this problem, the geometric diversity (GD) score is introduced to generate image test cases with more different fault feature types. In this paper, we propose DeepMCC, a multi-conditional constraintbased test case generation method based on the Conditional Generative Adversarial Networks (CGANs) framework, which innovatively introduces geometric diversity (GD) scores and Gini impurity. To validate the effectiveness of our method, we conduct experiments on four publicly available image datasets with five widely used DNN models, and the results show that (1) our method is more effective in terms of fault detection rate compared to black-box test methods, which generally improves the fault detection rate by 1% to 2%; (2) with the preset constraints on the geometric diversity scores, we can precisely control the generated test cases with higher diversity; (3) using the images generated by this method for retraining can effectively improve the accuracy of the model, which improves the accuracy by 0.1% to 0.4% on the original test set compared to other methods.
Accuracy and rigor are vital indicators of the specification document, especially for the ARINC653 aviation industry standard. A high-quality standard or specification should clearly depict the system behaviors yet leave no fatal vulnerability. Formal verification could definitely help achieve this goal, but it requires intensive professional domain knowledge and overwhelming manpower. Recently, fast-growing natural language processing (NLP) techniques do well in harvesting knowledge extraction for the downstream tasks. However, since knowledge about an entity is scattered over heterogeneous contents (plain text, pseudocode, XML, etc.) for almost all such standard documents, a single content or not all contents cannot account for the entire knowledge. To this end, we propose a novel and practical approach to construct the Ontology of ARINC653 and extract the logical guards. Technically, we combine the NLP techniques with domainspecific naming and lexical rules for entity recognition in Ontology and then apply information extraction and relation formalization for relation extraction (in terms of guards). We evaluate the quality of our Ontology against that induced by the domain professor. We further apply this approach to the historical ARINC653 standards and evaluate the performance. Results show that our approach indeed helps construct knowledge integration and aid for specification understanding.
Contrastive learning has shown impressive progress for the self-supervision based 3D point clouds feature learning. Based on the distance control in the feature space of positive and negative samples, it can obtain effective point cloud feature representations in a self-supervised manner. However, most existing contrast based point cloud learning methods only consider the feature similarity relationship between samples, (e.g., point cloud, voxel or image), which lack of explicit exploration on point cloud structure. Considering that structure is an important property of point clouds, for better feature learning, we propose a effective cross-modal contrast based method with image jigsaw (CrossCon-Jig) to better learn point cloud representations with both semantic and structural information. Specifically, our method includes intra-modal contrast of point cloud, cross-modal contrast between point cloud and rendered image, and point cloud guided image jigsaw. The intra-modal contrast and the contrast of cross-modal focus on the exploring of invariant and consistent feature representations, and image jigsaw guides the model to explore spatial structure information of point clouds. Extensive experimental tests on 3D object classification and 3D object part segmentation tasks have achieved excellent performance, demonstrating the effectiveness of the proposed method.
In the field of autonomous driving, safe and efficient decision-making through deep reinforcement learning remains a significant challenge. Existing methods often struggle to adapt to the dynamic and complex conditions of urban environments, while the lack of interpretability in reinforcement learning algorithms raises safety concerns. To address these issues, this paper proposes a reinforcement learning method guided by reward machine. Firstly, a reward machine tailored for autonomous driving scenarios is constructed to better guide the agent's behavior selection. Then, a time sensitivity factor is proposed to adjust the generation of counterfactual experiences, optimizing the effectiveness of policy learning. Furthermore, to improve the safety of autonomous driving decisions, formal verification of the decision-making process is conducted via the UPPAAL model checker, enabling the identification and handling of potential hazardous states. Finally, the effectiveness and safety of this method are validated through a case study of an autonomous driving system, demonstrating that the proposed reward machine-guided reinforcement learning algorithm performs well in complex road scenarios.
The rapid growth of the decentralized finance (DeFi) ecosystem has given rise to flash loan, a type of uncollateralized loan service that enables users to easily borrow substantial amounts of funds. However, this has prompted attackers to conduct malicious arbitrage within DeFi protocols, known as notorious flash loan attacks, resulting in significant asset losses. Existing works primarily focus on investigating price oracle manipulation, a common tactic in flash loan attacks, but lack a comprehensive understanding regarding the entire process of flash loan attacks and the diverse range of attack methods. In this paper, we empirically study 155 real-world flash loan attack incidents, representing the largest-scale study to date. We first categorize these incidents into five types based on their root causes and compile statistics on their distribution, then elucidate the vulnerable code and finance mechanisms exploited in each category. Subsequently, we identify the symptoms of codebased vulnerabilities and summarize the abstract attack models for the entire process. Finally, we evaluate the effectiveness of state-of-the-art off-chain tools in detecting code-based vulnerabilities within their scope of capabilities. We find that Slither performs the best in detecting 22 % of temporal reentrancy vulnerabilities, and DeFiTainter has a 52% false negative rate in detecting price oracle manipulation, mainly attributed to three limitations.
With the development of Pre-trained Language Models (PLMs), a wide variety of Chinese NLP tasks benefit from the BERT structure. Unfortunately, Chinese BERT-based PLMs are vulnerable to adversarial attacks and expose robustness issues. It inspired numerous defense works devoted to improving the model robustness. However, existing pre-training methods incur substantial time costs, while fine-tuning methods need more evidence to demonstrate how well the target model has been defended. This work aims to bridge this gap. We propose RoFuBERT, a robust fine-tuning framework using fuzz testing for Chinese BERT-based PLMs. We extract Chinese pinyin, glyph, and synonym features of downstream NLP tasks during fine-tuning. We integrate them into fuzz testing and evaluate the testing completeness of the model under adversarial attacks. Finally, we retrain the model for robust fine-tuning. Our evaluation shows that RoFuBERT improves adversarial robustness efficiently. Compared with the two baselines, RoFuBERT takes only 0.13 times more time. The reduction of adversarial attack success rate is improved by 41.26 %, and the modification rate of the adversarial samples is improved by 16.19 %, on average.
Finding the attack surface of the systems and applications is an important phase in secure software development lifecycle. Attack surface usually analyzed with the help of the experts or static and dynamic analysis tools. Most of the analysis tools and methods can be applied only to the single programs and do not cover the systems that consist of several heterogenous components. In this paper we present new hybrid introspection method for analyzing the software which includes interpreted code and just-in-time (JIT) compilers besides the machine code. We show how to inspect such applications when they are executed in the virtual machine. Targeting the virtual machine analysis allows one to recover the attack surface for the complex systems that include web servers, databases, and other backend components. We also present a case study with the analysis of Java application and show how to find bugs in the core dependencies, that reside on the attack surface.
Existing research in mobile app compatibility analysis faces two critical limitations: the absence of large-scale real-world datasets and the lack of systematic taxonomies for tool evaluation. To address these gaps, this study proposes a novel two-dimensional classification framework that categorizes compatibility issues through two analytical dimensions: causes (including API-induced issues such as deprecated methods, system-induced issues like permission changes, and hardware-induced issues such as sensor variations) and consequences (encompassing crashes, functional failure, UI inconsistencies, and performance degradation). Based on this classification framework, we developed CompatBench, the first manually curated dataset containing 78 real-world cases collected from GitHub submissions spanning 2017 to 2024. The dataset comprises 45 researcher-reproduced issues and 33 user-reported issues. Key findings reveal significant discrepancies between laboratory reproduction scenarios and real-world cases. API-related causes dominate reproduction cases at 91.1 %, but account for only 42.4 % of user-reported issues. Regarding manifestation visibility, 35.6 % of reproduction cases lack clear symptoms, whereas 96.9 % of real cases exhibit observable failures such as crashes or UI inconsistencies. Repair dynamics analysis shows 88.8 % of reproducible issues resolved within 50 days, contrasting with a 55.7 % fix rate for real issues. These results highlight critical methodological gaps in current research paradigms, particularly in causal inference based on observable consequences and consequence prediction based on potential causes. The study establishes three core contributions for validating compatibility management tools: a standardized taxonomy for issue classification, an openaccess dataset with real-world cases, and empirical evidence demonstrating discrepancies between laboratory and field observations. The findings emphasize the necessity of incorporating real-world datasets to improve evaluation validity in compatibility research.
In recent years, automated program repair has garnered considerable attention owing to its potential to mitigate software maintenance costs. There remain challenges for automated program repair techniques to be widely applied in practice, where too many overfitting patches are one of the issues. Automated patch correctness assessment emerges as a crucial means to enhance the viability of recommended patches in automated program repair technology. The current automated patch correctness assessment methods exhibit suboptimal performance when evaluating multiline patches compared to their effectiveness in assessing single-line patches. This disparity arises because multiline patches involve intricate contextual semantic relationships and significant program structure modifications, such as branching and looping. Those complexities render it more challenging for neural networks to capture the latent features essential for assessing correctness. To address the above problem, this paper proposes an automated patch correctness assessment method, named Peft, which fine-tunes a large language model using “golden data” that is generated based on semantic and program structural features, resulting in a patch evaluation model. Experiments were conducted on three datasets with varying proportions of multiline complex patches. The patches were sourced from real-world applications or generated by 23 APR techniques for fixing Defects4J v1.2. The results demonstrated that Peft consistently outperformed existing methods across all datasets. Notably, when evaluating datasets composed entirely of multiline complex patches, Peft significantly outperformed the open-source baseline technique Cache (accuracy: 79.2% vs. 66.1%, F1-score: 81.9% vs. 69.5%).
Deep neural networks can exhibit defects that lead to erroneous decisions in safety-critical scenarios, potentially causing severe consequences. While various repair techniques exist, methods based on retraining are often costly and imprecise and existing searchbased approaches can suffer from inefficient fault localization and patch generation. This paper introduces an end-to-end multi-objective, search-based framework for repairing DNNs that couples spectrumguided fault localization with an enhanced particle-swarm patch generator, and it directly modifies neural weights to address these challenges. Our approach features a novel, two-stage fault localization technique that first uses spectrum-based analysis to identify suspicious neurons and then applies multi-objective optimization to pinpoint the most critical weights for repair. For patch generation, we employ an enhanced Multi-Objective Particle Swarm Optimization algorithm designed for faster convergence and more effective exploration of the solution space. We evaluated our framework on multiple DNN architectures using four public datasets (Fashion-MNIST, CIFAR-10, LFW, and GTSRB). The proposed fault localization method led to an 18% increase in repair rate on the Fashion-MNIST dataset compared to state-of-the-art techniques. Furthermore, our end-to-end framework successfully reduced the most frequent misclassification type in a pretrained model by 31.3 % and proved effective for the adaptive repair of fully-trained models without causing catastrophic performance degradation. The results demonstrate that our approach offers a more precise and less disruptive alternative to retraining, providing a practical and cost-efficient method for the targeted repair of DNNs.
Efficient bug triage is a critical aspect of large-scale software development, yet it remains a labor-intensive and error-prone task. This paper presents a novel approach to automated bug report classification by leveraging BERT, a state-of-the-art transformer-based LLM, to categorize bug reports into well-defined software defect types. We introduce a structured and scalable classification taxonomy designed to reflect the complexities of real-world bug reports. The proposed method incorporates fine-tuning of BERT on domain-specific datasets and evaluates performance across multiple bug categories using accuracy, precision, recall, and F1-score metrics. Empirical results demonstrate that our approach outperforms traditional machine learning methods, achieving an overall accuracy of 72% and delivering particularly strong performance in critical categories such as security and performance bugs. Using both the bug title and description as input produced the best results, underscoring the importance of contextual detail in effective bug triage. This work contributes to the field of software defect classification by providing a replicable and adaptable methodology for automated bug triage, with practical implications for enhancing software maintenance and quality in large-scale development projects.
