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.
