We consider the LTL model-checking problem of concurrent self modifying code, i.e., concurrent code that has the ability to modify its own instructions during execution time. This style of code is frequently utilized by malware developers to make their malicious code hard to detect. To model such programs, we consider Self-Modifying Dynamic Pushdown Networks (SM-DPN). A SM-DPN is a network of Self-Modifying Pushdown processes, where each process has the ability to modify its current set of rules and to spawn new processes during execution time. We consider model checking SM-DPNs against single indexed LTL formulas, i.e., conjunctions of separate LTL formulas on each single process. This problem is non trivial since the number of spawned processes in a given run can be infinite. Our approach is based on computing finite automata representing the set of configurations from which the SM-DPN has a run that satisfies the single-indexed LTL formula. We implemented our techniques in a tool and obtained promising results. In particular, our tool was able to detect concurrent, self-modifying malware.
The rapid development of AI-generated content (AIGC) has heightened the threat of multimodal misinformation, posing significant security concerns. Existing misinformation detection methods have not addressed privacy concerns or have only considered the privacy of single-modal data, overlooking the semantic correlation privacy among multimodal data. In this paper, we propose a cloud-edge-end collaboration-based privacy-preserving multimodal misinformation detection (CPMD) scheme, safeguarding the correlation privacy of multimodal data while efficiently detecting misinformation. To achieve this, we introduce a local differential privacy-based multimodal Fourier dynamic protection (MFDP) scheme, thereby achieving efficient multimodal fusion and semantic correlation protection. We also design a multi-head spatiotemporal correlation attention-based large model pre-training protection (MSLP) method and DP-based Gradient Correlation Protection (DPGC) method, which ensure high-utility gradient correlation protection. Furthermore, we utilize a multimodal misinformation detection transformer (MMDT) to perform high accuracy recognition. Extensive experiments demonstrate that, compared to the HAMMER method, our CPMD method improves the accuracy of multimodal misinformation detection by 5.08%.
Large language models (LLMs) are reshaping software and transforming software paradigms. However, developing LLMs is both costly and frequently susceptible to trustworthiness issues. In this paper, we analyze whether these issues can be effectively mitigated by applying software engineering principles. In particular, we analyze the value of applying the Waterfall Model's phases to the LLM engineering process. We believe this study can provide valuable insights and guide the future development of LLMs toward greater cost-efficiency and trustworthiness.
Traditional pull-up assessments are typically conducted manually, a process that lacks objectivity and is both time-consuming and labor-intensive. To overcome these limitations, it is essential to develop an automated model for evaluating the correctness of pull-up movements. However, due to the absence of publicly available datasets, we constructed a custom pull-up action dataset consisting of videos recorded from both professional athletes and regular college students. In response to the limitations of existing action recognition models, this paper proposes an Adaptive Multi-dimensional Fusion Graph Convolutional Network (AMF-GCN), which comprises two key components: an Adaptive Graph Convolutional Module (AGCN) and a Multi-dimensional Fusion Module (MF). The AGCN module adaptively modifies the graph topology based on sample-specific data, enabling it to capture complex relationships among various joints. The MF module fuses information from multiple feature dimensions, thereby enhancing the model's flexibility and generalization capability. Extensive experimental comparisons demonstrate that our method achieves an accuracy of 97.33%, significantly outperforming several state-of-the-art action recognition models, thus validating its superior performance and effectiveness.
Integrating open-source software (OSS) components introduces significant legal risks due to license non-compliance, including litigation, financial penalties, and reputational damage. These risks escalate in modern dependency networks where projects inherit licenses from hundreds of dependencies, frequently resulting in license incompatibilities. To address these challenges, we present LiCoVer, an LLM-powered framework for automated license compliance verification. Our approach constructs a dependency graph and derives its corresponding license tree. We then utilize Large Language Models (LLMs) to extract critical license terms, while employing established compatibility algorithms to determine license compatibility (both secondary and combinative) across the tree. Additionally, we leverage LLMs' reasoning capabilities to provide AI-guided license recommendations based on developer preferences. By automating license term extraction and compatibility assessment while offering intelligent license selection support, our framework significantly reduces legal risks and streamlines compliant OSS integration.
Accurate time series forecasting demands effective integration of temporal dynamics and contextual semantics. While existing attention mechanisms capture numerical patterns effectively, they often neglect domain-specific temporal knowledge. We propose MixRecLGB, a novel framework that synergizes LightGBM with a language-enhanced mixed attention mechanism. Our key contributions include: 1) A recursive VAE architecture (RecLGB) that compresses long historical sequences into hierarchical memory features through progressive latent space learning; 2) A temporal-semantic fusion mechanism that injects frozen language model embeddings into both static linear attention and dynamic self-attention components, preserving temporal order while incorporating contextual knowledge; 3) A parameter-efficient integration strategy that enhances attention computation through adaptive bias injection and feature fusion, requiring minimal architectural modifications. Evaluated on five real-world datasets, MixRecLGB reduces forecasting errors while maintaining computational efficiency. This work establishes a new paradigm for combining deep temporal modeling with efficient gradient boosting, particularly effective for long-term forecasting scenarios.
Recent advancements in Large Language Models (LLMs) have greatly enhanced natural language understanding and content generation. However, these models primarily operate in disembodied digital environments and lack interaction with the physical world. To address this limitation, Embodied Artificial Intelligence (EAI) has emerged, focusing on agents that can perceive and interact with their surroundings. Despite progress, current embodied agents face challenges in unstructured real-world environments due to insufficient semantic intelligence, which is critical for understanding and reasoning about complex tasks. This paper introduces the Semantic Intelligence-Driven Embodied (SIDE) agent framework, which integrates a hierarchical semantic cognition architecture with a semantic-driven decision-making process. This enables agents to reason about and interact with the physical world in a contextually adaptive manner. The framework is inspired by biological cognitive mechanisms and utilizes bio-inspired principles to design a semantic cognitive architecture that mimics how humans and animals integrate and process sensory information. We present this framework as a step toward developing more intelligent and versatile embodied agents.
The theory of minimal explanations offers a rigorous, model-based solution to the problem of producing explanations for the decisions of AI models. In some high-stakes contexts, there is a need to generate all possible explanations for a particular decision using certified programs, whose output can be trusted. We used the proof assistant Coq to certify a recently proposed algorithm for the enumeration of explanations in the case of monotonic classifiers. Our experimental results on the extracted code showcase the scalability of this approach, underscoring its potential for improving trust and reliability in AI systems.
Program comprehension remains challenging when analyzing complex systems across multiple abstraction levels. Current approaches typically focus on either source code or binary analysis in isolation, and operate at single levels of abstraction. These limitations create gaps between technical analysis and practical understanding needs. To bridge this gap, we present our vision on UFPC, a unified program comprehension framework that bridges multiple abstraction levels while supporting both source code repositories and compiled binaries. Our approach uses a semantic-enhanced code property graph that serves as a compatibility layer. Based on the compatibility layer, the framework recovers high-level system design and infers original business intent from implementation details, while providing both programmatic access through structured APIs and natural language interaction through LLM-based agents. By envisioning UFPC, we aim to facilitate diverse downstream tasks on software engineering and security, including vulnerability detection, malware analysis, software maintenance, and etc.
We investigated the Tendermint protocol, a core Byzantine Fault Tolerance (BFT) consensus engine for the Cosmos Blockchain. When modelling this protocol, we faced significant challenges in the computational performance of verification. To mitigate the state-space explosion issue, we improve the model with optimisation techniques, such as partial-order reduction and role-based symmetry reduction. Through verification, we discovered vulnerabilities in the design of Tendermint, and we proposed fixes that regained both the safety and liveness properties. This paper describes our modelling techniques and optimisations, analyses the vulnerabilities and fixes, and discusses how the optimisations impact verification runtime and results.
As deep neural networks (DNNs) are increasingly deployed in critical domains, ensuring their reliability and security has become a key research focus. While mutation-based fault localization (MBFL) has shown superior effectiveness in DNN testing compared to conventional methods, its practical application faces significant computational challenges due to the enormous number of mutants it generates. To tackle this challenge, we propose DeepMR, a novel learning-based approach for mutation reduction in DNN models that maintains fault localization accuracy while dramatically decreasing computational costs. The core insight behind DeepMR is that strategically targeting key neurons—those critically influencing the decision paths of test cases—with high-impact mutation operators can yield a subset of mutants that substantially improve fault localization efficacy. DeepMR dynamically distinguishes effective mutants by jointly analyzing (1) runtime neuron behaviors during training and inference and (2) mutation operator characteristics, ensuring the selection of maximally informative mutants while discarding redundant ones. To validate the effectiveness of our approach, we trained DeepMR using data from 59 DNN programs and evaluated it on 31 DNN programs. Our experimental results show that when selecting 25
In recent years, Mobile Edge Computing (MEC) and Wireless Power Transfer (WPT) technologies have been widely applied to wireless devices (WDs). However, in remote areas or during disaster events, data and energy transmission cannot be accomplished through conventional ways. To address this challenge, this paper explores a WPT-MEC system using Unmanned Aerial Vehicle (UAV) with 3D flying and obstacle avoidance. Our goal is to maximize the long-term task completion ratio while considering the constraints of UAV coverage, time resources, energy, and task validity duration. We first model this problem into multiple equal-sized time slots, with each time slot involving two main actions. The first action is the UAV selecting its flight direction based on the tasks of the on-site WDs. The second action is after UAV’s flying, the WDs which are in the UAV’s coverage offload their tasks to UAV. For each action decision, we design a Deep Reinforcement Learning (DRL) algorithm. By training two models to accomplish this task, our algorithm significantly improves the long-term task completion ratio, with performance improvements reaching up to 40
Neural Program Repair (NPR) has emerged as a promising approach to automatically fix bugs in software programs. By leveraging large datasets of buggy and patched code, NPR models learn patterns and transformations to generate patches. Nevertheless, one fundamental challenge in NPR is the Out-of-Vocabulary (OOV) problem, which occurs when the model encounters tokens that were not seen during training. Due to the diversity and variability of code, the OOV problem is particularly prevalent in the context of NPR, and it may affect the model's ability to generalize and repair unseen or uncommon code. To comprehensively understand the characteristics of OOV problem and its impacts on NPR, this study conduct an empirical study on three NPR models and two datasets. Our results reveal that the OOV rate decreases with the increasing of the vocabulary of the NPR model, and that the most common types of OOV words in NPR are variable name and parameter name. The results also confirm the negative impact of OOV words on the repair effectiveness of NPR models. Our findings highlight the importance of addressing the OOV problem to enhance the effectiveness and real-world utility of NPR models.
In recent years, the energy-efficient hybrid flow shop scheduling problem (EHFSP) has gained significant attention in both academia and industry. However, most existing studies focus solely on either energy supply or demand strategies, which leads to suboptimal overall system efficiency and energy waste. To address this challenge, this paper proposes a novel multi-objective mixed-integer nonlinear model that integrates time-of-use pricing with machine power-down strategy, achieving a coordinated optimization of production efficiency and energy costs. To solve the proposed model, we develop a Q-learning-driven multi-crossover operator non-dominated sorting genetic algorithm II (QMCO-NSGA-II). By embedding Q-learning into the multi-crossover operator framework, the algorithm adaptively selects crossover operators, effectively balancing solution diversity and convergence. Additionally, an improved Nawaz-Enscore-Ham heuristic is introduced to generate high-quality initial solutions, enhancing both the convergence speed and solution quality. Extensive experiments on standard EHFSP datasets demonstrate that QMCO-NSGA-II significantly outperforms four state-of-the-art multi-objective algorithms in terms of convergence and solution diversity, showcasing its practical applicability to complex industrial scenarios.
Verifying the safety properties of neural network controlled systems (NNCSs) is essential before their deployment in safety-critical scenarios. NNCSs face significant verification challenges due to the complex nonlinear interactions between neural network controllers and dynamic systems. While Taylor models (TMs) excel in capturing nonlinear dynamics of the system and linear abstract domains efficiently verify neural networks, their isolated use faces two limitations: TMs struggle with neural network scalability, while linear abstract domains cannot precisely represent nonlinear system states. To overcome these limitations, we present a verification approach that synergistically integrates TMs with linear abstract domains. Since naive interval-based approximations often destroy variable dependencies between TMs and linear abstract domains, we further propose a parity-characteristic-driven linearization method to construct interval linear abstraction of TMs, preserving variable dependencies by extracting relationships in nonlinear terms and incorporating them into linear terms. Based on the interval linear abstraction of TMs, our approach enables bidirectional conversion between TMs and different linear abstract domains while reducing precision loss during abstraction conversion. We implemented a prototype named TTLA. Experimental results show that TTLA outperforms the tools in terms of both efficiency and tightness of the reachable set overapproximation. In addition, TTLA enables scalable verification, with neural network analysis time under 0.7 s even for large networks.
Financial sentiment analysis is crucial for market insights and investment strategies. While pre-trained language models (PLMs) have demonstrated significant advancements in general domains, they struggle with the unique linguistic characteristics of financial texts. Financial PLMs improve financial feature extraction but are hindered by limited and uniform training data, restricting their ability to capture contextual and semantic nuances. To address these challenges, this work proposes FinPTA a novel framework for financial sentiment analysis. Specifically, FinPTA leverages FiLM (Financial Language Model) for domain-specific feature extraction, capturing intricate semantic features embedded in financial texts. After that, the tTransformer, an enhanced transformer encoding model, is employed to better capture contextual relationships within financial texts. Finally, to further enhance robustness and generalization, we incorporate adversarial training, enabling the model to withstand perturbations and ambiguities inherent in financial texts. Experimental results demonstrate that FinPTA achieves state-of-the-art performance across multiple financial datasets, providing a robust and reliable solution for financial sentiment analysis tasks.
As software systems evolve, test cases must adapt to code changes to remain valid and effective. Traditional test migration approaches, including symbolic execution and diff-based heuristics, often require significant manual effort and struggle to handle complex behavioral changes. Recent advances in large language models (LLMs) offer new opportunities for context-aware and automated test adaptation. However, existing LLM-based approaches are not well-suited for test case migration under evolving code, as they typically lack explicit modeling of code changes and original test context. In this paper, we present TestCaseMig, a framework that integrates LLMs with static analysis to migrate existing test cases in response to code modifications. TestCaseMig constructs change-sensitive, context-rich prompts and employs a multi-round, feedback-driven generation process with validation and coverage analysis to ensure the correctness, completeness, and adaptability of migrated test cases.
The autonomy and contextual complexity of LLM-based age-nts render traditional access control (AC) mechanisms obsolete. Static, rule-based systems designed for predictable environments are fundamentally ill-equipped to manage the dynamic information flows inherent in agentic interactions. This position paper argues for a paradigm shift from binary access control to a more sophisticated model of information governance, positing that the core challenge is not merely about permission, but about governing the flow of information. We introduce Agent Access Control (AAC), a novel framework that reframes AC as a dynamic, context-aware process of information flow governance. AAC operates on two core pillars: (1) multi-dimensional contextual evaluation, which assesses not just identity but also relationships, scenarios, and norms; and (2) adaptive response formulation, which moves beyond simple allow/deny decisions to shape information through redaction, summarization, and paraphrasing. This vision, powered by a dedicated AC reasoning engine, aims to bridge the gap between human-like nuanced judgment and scalable AI safety, proposing a new conceptual lens for future research in trustworthy agent design.
Checking the correctness of complex concurrent programs is inherently challenging due to the large amount of code and complex structures. Three key issues are required to addressed: choosing a proper correctness condition as a goal of checking, proposing an effective approach for checking the correctness condition, and adapting the architectural details of complex concurrent programs. In this paper we propose an efficient methodology to address these issues by considering complex concurrent programs as concurrent objects. To solve the first issue, linearizability, a de facto correctness criterion for concurrent objects, is chosen as the correctness condition for complex concurrent programs. To solve the second issue, we propose an effective approach to reduce the potential exponential explosion in linearizability checking. Sequential executions are referred to as sequential specifications with their correctness guaranteed via a combination of a replay mechanism and the insertion of assertions. The third issue requires to solve architecture-relevant problems that hinder linearizability checking. We propose a notion called "macro operations" to assemble "fragments" of operations. This is quite suitable for dealing with inter-core interrupt mechanisms. To demonstrate the effectiveness of our methodology, we verify a task management and scheduling system, which is a critical component of a multi-core embedded operating system kernel, supporting the preemptive multi-core task scheduling and inter-core interrupts. During this process, we found and fixed numerous errors in the original system design, which were confirmed by the system developer.
With the rapid advancement of artificial intelligence, learning based fault localization has emerged as a critical research area in software testing. Existing methods, including traditional statistical and machine learning based approaches, have significantly improved fault localization by representing program features with deep learning models. However, these methods still encounter challenges such as difficulties in processing complex program structures, dependency on high-quality test suites, and limited generalization across diverse software projects. This paper presents Contast, a graph-based fault localization method that integrates abstract syntax trees (ASTs), path-attention mechanisms, and graph neural networks (GNNs) to address these challenges and improve prediction performance. By incorporating AST path-contexts, node coverage information, and bug reports, Contast effectively captures structural, contextual and behavioral features of programs. The synergy between the path-attention model and GNNs enables precise identification and localization of faulty statements within programs, demonstrating its strength in addressing structural complexity. Empirical evaluations show that Contast outperforms state-of-the-art graph-based and learning-based methods in both localization capability and computational cost. Notably, Contast achieves 91.54 project and even delivers improvements of up to 22.01 project in terms of recall. Moreover, Contast significantly reduces training times across projects, emphasizing its practical advantages of code and graph processing in large-scale applications. These results highlight Contast as an effective and efficient solution for fault localization in modern software testing.
