Software vulnerabilities pose severe security threats, highlighting the need for effective automated detection. Directed hybrid fuzzing, which combines the rapid exploration of fuzz testing with the precise constraint solving of symbolic execution, has made notable advancements in vulnerability discovery. However, existing directed hybrid fuzzing approaches still face two key challenges: (1) inefficient seed selection, leading to inadequate prioritization of optimal inputs for symbolic execution, and (2) inefficient seed generation, resulting in suboptimal seed generation. To address these issues, we propose TACO-Fuzz, TArget-Centric cOncolic Fuzzing, which introduces a two-phase target-centric seed selection strategy to prioritize under-explored paths and a target-centric seed generation approach based on constructing extended path conditions, thereby improving seed quality. Our evaluation on a selected set of public benchmarks shows that TACO-Fuzz can outperform several representative state-of-the-art directed fuzzing tools, achieving up to an average speedup of nearly 10x in reaching target locations, along with comparable improvements in reproducing real-world vulnerabilities. Moreover, TACO-Fuzz contributed to the discovery of 17 previously unknown vulnerabilities, each assigned a CVE, and demonstrated faster vulnerability discovery and reproduction in most cases.

Real-time systems must simultaneously deliver predictable timing, fault isolation, and memory safety, yet current operating systems expose only low-level primitives that force developers to manually balance concurrency, isolation, and performance. This paper presents LARTS, a language-aided runtime system that elevates these requirements into language abstractions with enforceable semantics. LARTS introduces execution domain, a unified process–thread abstraction that combines thread-level responsiveness with process-level isolation. Memory is managed through deterministic memory contracts, which bind allocation at load time to eliminate runtime failures and unpredictable latencies. Domain interactions are expressed via deterministic communication channels that integrate efficient transfer, type safety, and priority inheritance, ensuring analyzable end-to-end bounds. Moreover, LARTS enforces secure-by-construction semantics, making classes of bugs such as double fetch and use-after-free unrepresentable in the programming model. We formalize the core semantics of LARTS and show how they guarantee determinism and safety by design. A prototype built on RTEMS demonstrates that LARTS preserves competitive real-time performance while substantially reducing programming complexity and eliminating vulnerabilities in realistic case studies. Our results suggest that high-assurance real-time programming can be treated not as an ad-hoc engineering problem, but as a first-class abstraction with verifiable semantics.

Dynamic binary translation serves as a pivotal technique for instruction set simulation, yet encounters critical challenges when handling explicit instruction-level parallelism and operational latency inherent in VLIW architectures. Existing approaches demonstrate limited capability in handling non-arithmetic operations, particularly branch and memory access instructions. The complexity intensifies when translating software-pipelined loops featuring architecture-specific instructions due to two inherent characteristics: 1) instruction reordering, overlapping, and masking within loop bodies, and 2) absence of explicit conditional branches and loop counter manipulation instructions. This work presents three original strategies for VLIW code translation. First, a strategy constrains translation block length to resolve branch instruction challenges. Second, an approach manages store-load dependencies through strategic postponement of store instruction processing. Third, a novel software-pipelined loop translation methodology ensures correct execution semantics by serializing parallel iterations, generating state-specific translation blocks, and synchronizing inner and outer loops translations. We implemented these techniques in VEMU and evaluated it against dsplib and Polybench benchmarks. VEMU successfully translates all benchmark programs. Our first strategy does not degrade performances and the second strategy brings 0.2% time overhead. Comparative analysis reveals a speedup ratio between 3.25× and 7× over the Texas Instruments simulator for the same benchmarks, validating the efficacy of the proposed techniques.

Incremental symbolic execution aims to address the scalability challenges of traditional symbolic execution by concentrating on behavioural differences between program versions introduced during program evolution. Despite progress in the field, existing techniques often struggle to explore these behaviors both efficiently and accurately. In this paper, we introduceFENSE, a novel approach for incremental symbolic execution that improves efficiency by identifying and eliminating redundant paths.FENSEachieves this by summarizing previously explored paths and monitoring variables that may induce divergent incremental behaviors at each branching point. This summarization process enablesFENSEto detect whether a newly explored path subsumes distinct incremental behaviors compared to prior explorations. By effectively pruning redundant paths that exhibit identical incremental behaviors as those previously explored,FENSEachieves a potentially exponential reduction in the number of explored paths. We implemented a prototype ofFENSEand evaluated it on a diverse set of real-world applications. Experimental results demonstrate thatFENSEoutperforms state-of-the-art techniques by significantly reducing both path exploration and execution time. When applied to real-world commits from the GNU Coreutils project,FENSEachieved an average of 76% reduction in explored paths and a 139× speedup overKLEE.

Deep learning-based vulnerability detection has made significant strides, surpassing traditional static and dynamic analysis methods. However, existing approaches, including Graph Neural Networks (GNNs) and Transformer-based models, still struggle to fully capture complex code semantics. In this paper, we proposeCosFormer, a novel Code Semantic-aware Transformer tailored for vulnerability detection.CosFormerintroduces two key components: Code Semantic-aware Embedding, which enhances semantic representation at both the token and line levels, and Spatial Dependency-aware Encoding, which integrates structural dependencies from Control Flow Graphs (CFGs) and Program Dependency Graphs (PDGs) to guide attention toward vulnerability-relevant code. We evaluateCosFormeron four benchmark datasets, including a real-world dataset, and demonstrate its superior performance.CosFormerachieves the highest F1 scores across all tasks, outperforming state-of-the-art GNN-based and Transformer-based models, as well as large language models (LLMs). Notably,CosFormerachieves a Cross F1 of 69.37 and a Mixed F1 of 58.42 in generalization evaluation, surpassing all baselines. These results highlightCosFormer’s effectiveness and robustness in detecting vulnerabilities across diverse and previously unseen codebases.

Symbolic execution is a powerful technique for bug finding by generating test inputs to systematically explore all feasible paths within a given threshold. However, its practical usage is often limited by the path explosion problem. In this paper, we propose compatible branch coverage driven symbolic execution for efficient bug finding. Our new technique owns a novel path-pruning strategy obtained from program dependency analysis to effectively avoid unnecessary explorations. Specifically, based on a Compatible Branch Set , our technique directs symbolic execution to explore feasible branches while soundly pruning redundant paths that have no new contributions to branch coverage. We have implemented our approach atop KLEE and conducted experiments on a set of programs from Siemens Suite, GNU Coreutils, and other real-world programs. Experimental results show that, compared with the state-of-the-art symbolic execution techniques, our approach always uses significantly less time to reproduce bugs while achieving the same or better branch coverage. On average, our approach got over 45% path reduction and 3x speedup on the GNU Coreutils programs

Incremental symbolic execution addresses the scalability problem of symbolic execution by concentrating on incremental behaviors that are introduced by the changes during program evolution. However, the state-of-the-art techniques still face the challenge to efficiently and precisely explore incremental program behaviors. In this paper, we present FENSE, a novel approach for incremental symbolic execution which checks whether the current path may subsume different incremental behavior from previous explorations. This is enabled by summarizing previously explored paths by recording the variables that may induce different incremental behaviors at each branch location. Our approach can identify redundant paths which share the same incremental behavior as previous explorations during test generation. Pruning away such redundant paths can lead to a potentially exponential redunction in the number of explored paths. We implemented a prototype of FENSE and conducted experiments on a set of real-world applications. The experimental results show that our approach is effective in reducing the number of explored paths as well as the execution time, compared with the state-of-the-art techniques.

We present a technique that systematically explores the state spaces of concurrent programs across both the schedule space and the input space. The cornerstone is a new model called Maximal Path Causality (MPC), which captures all combinations of thread schedules and program inputs that reach the same path as one equivalency class, and generates a unique schedule+input combination to explore each path. Moreover, the exploration for different paths can be easily parallelized. Our extensive evaluation on both popular concurrency benchmarks and real-world C/C++ applications shows that MPC significantly improves the performance of existing techniques.

Symbolic execution is emerging as a powerful technique for generating test inputs systematically to achieve exhaustive path coverage of a bounded depth. However, its practical use is often limited by path explosion because the number of paths of a program can be exponential in the number of branch conditions encountered during the execution. To mitigate the path explosion problem, we propose a new redundancy removal method called postconditioned symbolic execution. At each branching location, in addition to determine whether a particular branch is feasible as in traditional symbolic execution, our approach checks whether the branch is subsumed by previous explorations. This is enabled by summarizing previously explored paths by weakest precondition computations. Postconditioned symbolic execution can identify path suffixes shared by multiple runs and eliminate them during test generation when they are redundant. Pruning away such redundant paths can lead to a potentially exponential reduction in the number of explored paths. Since the new approach is computationally expensive, we also propose several heuristics to reduce its cost. We have implemented our method in the symbolic execution engine KLEE [1] and conducted experiments on a large set of programs from the GNU Coreutils suite. Our results confirm that redundancy due to common path suffix is both abundant and widespread in real-world applications.

We propose a new automated debugging method for regression testing based on a synergistic application of both dynamic and semantic analysis. Our method takes a failure- inducing test input, a buggy program, and an earlier correct version of the same program, and computes a minimal set of code changes responsible for the failure, as well as explaining how the code changes lead to the failure. Although this problem has been the subject of intensive research in recent years, existing methods are rarely adopted by developers in practice since they do not produce sufficiently accurate fault explanations for real applications. Our new method is significantly faster and more accurate than existing methods for explaining failed regression tests in real applications, due to its synergistic analysis framework that iteratively applies both dynamic analysis and a constraint solver based semantic analysis to leverage their complementary strengths. We have implemented our new method in a software tool based on the LLVMcompiler and the KLEE symbolic virtual machine. Our experiments on large real Linux applications show that the new method is both efficient and effective in practice.

Symbolic execution is emerging as a powerful technique for generating test inputs systematically to achieve exhaustive path coverage of a bounded depth. However, its practical use is often limited by path explosion because the number of paths of a program can be exponential in the number of branch conditions encountered during the execution. To mitigate the path explosion problem, we propose a new redundancy removal method called postconditioned symbolic execution. At each branching location, in addition to determine whether a particular branch is feasible as in traditional symbolic execution, our approach checks whether the branch is subsumed by previous explorations. This is enabled by summarizing previously explored paths by weakest precondition computations. Postconditioned symbolic execution can identify path suffixes shared by multiple runs and eliminate them during test generation when they are redundant. Pruning away such redundant paths can lead to a potentially \emph{exponential} reduction in the number of explored paths. We have implemented our method in the symbolic execution engine KLEE and conducted experiments on a large set programs from the GNU Coreutils suite. Our results confirm that redundancy due to common path suffix is both abundant and widespread in real- world applications.

During software debugging, a significant amount of effort is required for programmers to identify the root cause of a manifested failure. In this article, we propose a cascade fault localization method to help speed up this labor-intensive process via a combination of weakest precondition computation and constraint solving. Our approach produces a cause tree, where each node is a potential cause of the failure and each edge represents a casual relationship between two causes. There are two main contributions of this article that differentiate our approach from existing methods. First, our method systematically computes all potential causes of a failure and augments each cause with a proper context for ease of comprehension by the user. Second, our method organizes the potential causes in a tree structure to enable on-the-fly pruning based on domain knowledge and feedback from the user. We have implemented our new method in a software tool called CaFL, which builds upon the LLVM compiler and KLEE symbolic virtual machine. We have conducted experiments on a large set of public benchmarks, including real applications from GNU Coreutils and Busybox. Our results show that in most cases the user has to examine only a small fraction of the execution trace before identifying the root cause of the failure.