Static analysis is a foundational technique for detecting software defects, yet it notoriously suffers from high false positive rates. Prior efforts to reduce false positives via model checking, symbolic execution, dynamic analysis, testing, or machine learning either fail to scale or mistakenly eliminate real defects. This paper presents RICAN, a novel approach that leverages dynamic testing to reliably eliminate false alarms in static analysis. The key insight behind RICAN is the concept of input-agnosticity: if the validity of an alarm is independent of program inputs along each execution path, then once all such paths from the program entry to the alarm site have been exercised by tests without triggering the alarmed bug, the alarm can be safely classified as a false positive. To realize this insight, RICAN uses data-dependence analysis to identify input-agnostic alarms among all reported alarms. However, validating even input-agnostic alarms requires exploring all feasible paths, which is generally infeasible. To address this, RICAN computes a necessary set of paths by identifying only those branches and loops that may influence the alarm's validity. Finally, RICAN eliminates false alarms using existing dynamic testing and post-directed fuzzing to cover these critical paths. We evaluate RICAN on six real-world open-source projects. Our experiments show that RICAN can reliably eliminate 1,313 (45.09%) false positives across 2,912 double free, use-after-free, and null pointer dereference alarms, while incurring negligible overhead. Our user studies further demonstrate that RICAN reduces the manual effort required for alarm inspection by over 70% on average and helps programmers find bugs more quickly and accurately, highlighting its practical usefulness in real-world static analysis.

Recovering function signatures is a cornerstone of binary program analysis, yet it remains a challenging task. Existing methods either rely on disassembly-based constraints, which struggle with cross-architecture compatibility and scalability, or adopt learning-based approaches that are resource-intensive and often inaccurate.

Yu Wang, Shiwan Zhao, Zhihu Wang, Ming Fan, Xicheng Zhang, Yubo Zhang, Zhengfan Wang, Heyuan Huang, Ting Liu. Proceedings of the 2025 Conference on Empirical Methods in Natural Language Processing. 2025.

The growing adoption of Go for concurrent programming highlights its strengths in performance and simplicity, yet its special concurrency model-integrating shared memory with channel-based communication-introduces significant challenges for data race detection.Existing dynamic analysis tools suffer from high false negatives due to path-dependent execution, while static approaches often fail to account for features intrinsic to Go's concurrency model, such as channels and context propagation, leading to excessive false positives.To address these limitations, we present GRace, a static analysis framework tailored for Go that systematically models concurrency semantics to improve detection accuracy.GRace first identifies shared memory locations through pointer analysis and syntax-aware rules, then applies lock set analysis to filter protected accesses.By constructing a Go-specific happens-before graph that integrates Go's synchronization mechanisms (e.g., channels, Wait-Groups, Context cancellation), GRace refines event ordering and computes vector clocks to eliminate ordered accesses.Evaluated on real-world projects and benchmark datasets, GRace detected 18 data races in open-source repositories, with 11 confirmed and 8 fixed by developers.

With the rapid development of computer technology, emerging programming languages and compilers are constantly being introduced.However, these new compilers often have defects due to their short development time, insufficient testing, and the challenges they face, which affect their reliability and adoption.Traditional testing methods are limited in addressing the challenges of testing these new compilers.This paper proposes a new method for testing emerging compilers based on test case reuse, utilizing large language models to convert test cases from one programming language to another.Using C++ and Carbon language as examples, historical test cases from C++ are converted to Carbon language versions to expand the test case library for the Carbon compiler.This method involves fine-tuning a large language model to transform C++ historical bugs codes into codes suitable for the Carbon compiler, followed by verification to ensure their effectiveness.By converting and reusing test cases and implementing feature conversions to generate mutations, we improve 6.63% test coverage for Carbon compiler and discover 8 bugs.

The Satisfiability Modulo Theory (SMT) problem over floating-point operations presents a significant challenge. State-of-the-art SMT solvers often run into difficulties when dealing with large, complex floating-point constraints. Recently, a new approach to floating-point constraint solving emerges, utilizing mathematical optimization (MO) methods as an engine of their solving approach. Despite the novelty, these methods can fall short in both effectiveness and efficiency due to issues of the translated functions ( e.g ., discontinuity) and inherent limitations of their underlying MO method ( e.g ., imprecise search process, scalability issues). Driven by these weaknesses of prior solvers, this paper introduces a new MO-based approach that is shown highly potent in solving floating-point constraints. Specifically, on the benchmarks of JFS (a recent solver based on fuzzing), Grater, a realization of our approach, solves as many constraints as Bitwuzla and one more than CVC5 but runs over 10 times faster and over 40 times faster than Bitwuzla and CVC5 in median solving time across all benchmarks. It is worth mentioning that Bitwuzla and CVC5 are the strongest solvers for floating-point constraints according to results of the annual international SMT solver competition (SMT-COMP). Together, they have won all gold medals for QF_FPArith and FPArith divisions, which focus on floating-point constraints solving, over the past three years. To further evaluate Grater, we select over 100 most difficult benchmarks from the FP SMT-LIB, a logic regularly used in SMT-COMP. The difficulty is measured by the complexity of the composition ( e.g ., number of variables, clauses) and the interdependencies within constraints. Grater again solves the same number of constraints as Bitwuzla and CVC5 while running over 10 times faster than both solvers in average solving time, and over 50 times ( resp . 30 times) faster than Bitwuzla ( resp . CVC5) in median solving time. We release the source code of Grater, along with all evaluation data, including detailed comparisons of Grater against each baseline solver ( i.e ., Z3, CVC5, Bitwuzla, JFS, XSat, and CoverMe), at https://github.com/grater-exp/grater-experiment to facilitate reproducibility.

Compilers are among the most foundational software ever developed. A critical component of a compiler is its optimization phase, which enhances the efficiency of the generated code. Given the sheer size and complexity of modern compilers, automated techniques for improving their optimization component have been a major area of research. This paper focuses on a specific category of issues, namely missed optimizations, where compilers fail to apply an optimization that could have made the generated code more efficient. To detect missed optimizations, we propose Synchronized Behavior Checking ( SBC ), a novel approach that cross-validates multiple optimizations by leveraging their coordinated behaviors. The key insight behind SBC is that the outcome of one optimization can validate whether the conditions required for another optimization were met. For a practical implementation of SBC , we cross-validate two optimizations at once based on two kinds of relationships — co-occurring and complementary. In the co-occurring relationship, if an optimization is applied based on a specific semantic constraint ( i.e ., optimization condition) from an input program, another optimization, which depends on the same semantic constraint, should be applied as well. Second, when two optimizations are enabled by complementary semantic constraints, exactly one of the two optimizations should be applied. When an optimization should have been applied (according to either relationship) but was not applied, we regard it as a missed optimization. We conduct an extensive evaluation of SBC on two state-of-the-art industry compilers LLVM and GCC. SBC successfully detects a large number of missed optimizations in both compilers, in particular, they are caused by a wide range of compiler analyses. Based on our evaluation results, we reported 101 issues to LLVM and GCC, out of which 84 have been confirmed, and 39 have been fixed or assigned (for planned fixes). SBC opens up a new, exciting direction for finding missed compiler optimizations.

Layered sparse value-flow analysis (SVFA) is a prominent static analysis for resolving program dependencies. Despite the significant progress, SVFA still suffers from scalability issue. In light of the natural, continuous evolution of software, we introduce SILVA , the first incremental layered SVFA that scales to large, real-world programs efficiently. At the core of SILVA lies a novel incremental pointer analysis and incremental Mod-Ref analysis. Our extensive experiments on large-scale, real-world C/C++ programs demonstrate its effectiveness: SILVA achieves nearly a 7× speedup over SVF , the state-of-the-art layered SVFA, without losing any precision. Moreover, our incremental pointer and Mod-Ref analysis algorithms are 12× and 5× faster than existing methods, respectively. Regarding the impact of the size of the code changes on SILVA ’s effectiveness, we find that SILVA outperforms SVF for changes up to 10K lines—well beyond the typical scope of code commits in real-world software development.

Null pointer dereference raises Null Pointer Exceptions (NPEs). There are two groups of approaches to detect NPEs. Type-based approaches carry out strict type-based null safety checking. They heavily rely on annotations, and thus produce many false positives. Dataflow-based approaches leverage static forward and/or backward dataflow analysis. They mostly have a limited capability in tracking fields and interprocedural analysis, and introduce false positives and false negatives. To address these drawbacks, we propose Wheeljack to detect NPEs for Java. It does not rely on annotations, and hence can work effectively under a lack of annotations. It leverages our novel abstraction of nullness status to enhance field tracking, and our novel invocation analysis (capturing change to return value and side effect of an invocation) to enhance interprocedural analysis. Our evaluation on 28 Java projects has demonstrated that Wheeljack can mostly outperform the four state-of-the-art NPE detectors in recall without sacrificing precision. 5 and 2 new NPEs have been confirmed and fixed by developers after we submit 8 issues.

While deep neural networks provide state-of-the-art solutions to a wide range of programming language tasks, their effectiveness in dealing with foundational program analysis tasks remains under explored. In this paper, we present an empirical study that evaluates four prominent models of code (i.e., CuBERT, CodeBERT, GGNN, and Graph Sandwiches) in two such foundational tasks: (1) alias prediction, in which models predict whether two pointers must alias, may alias or must not alias; and (2) equivalence prediction, in which models predict whether or not two programs are semantically equivalent. At the core of this study is CodeSem, a dataset built upon the source code of real-world flagship software (e.g., Linux Kernel, GCC, MySQL) and manually validated for the two prediction tasks. Results show that all models are accurate in both prediction tasks, especially CuBERT with an accuracy of 89% and 84% in alias prediction and equivalence prediction, respectively. We also conduct a comprehensive, in-depth analysis of the results of all models in both tasks, concluding that deep learning models are generally capable of performing foundational tasks in program analysis even though in specific cases their weaknesses are also evident. Our code and evaluation data are publicly available at https://github.com/CodeSemDataset/CodeSem.

The pervasive brittleness of deep neural networks has attracted significant attention in recent years. A particularly interesting finding is the existence of adversarial examples, imperceptibly perturbed natural inputs that induce erroneous predictions in state-of-the-art neural models. In this paper, we study a different type of adversarial examples specific to code models, called discrete adversarial examples , which are created through program transformations that preserve the semantics of original inputs.In particular, we propose a novel, general method that is highly effective in attacking a broad range of code models. From the defense perspective, our primary contribution is a theoretical foundation for the application of adversarial training — the most successful algorithm for training robust classifiers — to defending code models against discrete adversarial attack. Motivated by the theoretical results, we present a simple realization of adversarial training that substantially improves the robustness of code models against adversarial attacks in practice. We extensively evaluate both our attack and defense methods. Results show that our discrete attack is significantly more effective than state-of-the-art whether or not defense mechanisms are in place to aid models in resisting attacks. In addition, our realization of adversarial training improves the robustness of all evaluated models by the widest margin against state-of-the-art adversarial attacks as well as our own.

This paper introduces a novel method, called WheaCha, for explaining the predictions of code models. Similar to attribution methods, WheaCha seeks to identify input features that are responsible for a particular prediction that models make. On the other hand, it differs from attribution methods in crucial ways. Specifically, WheaCha separates an input program into "wheat" (i.e., defining features that are the reason for which models predict the label that they predict) and the rest "chaff" for any given prediction. We realize WheaCha in a tool, HuoYan, and use it to explain four prominent code models: code2vec, seq-GNN, GGNN, and CodeBERT. Results show that (1) HuoYan is efficient — taking on average under twenty seconds to compute wheat for an input program in an end-to-end fashion (i.e., including model prediction time); (2) the wheat that all models use to make predictions is predominantly comprised of simple syntactic or even lexical properties (i.e., identifier names); (3) neither the latest explainability methods for code models (i.e., SIVAND and CounterFactual Explanations) nor the most noteworthy attribution methods (i.e., Integrated Gradients and SHAP) can precisely capture wheat. Finally, we set out to demonstrate the usefulness of WheaCha, in particular, we assess if WheaCha’s explanations can help end users to identify defective code models (e.g., trained on mislabeled data or learned spurious correlations from biased data). We find that, with WheaCha, users achieve far higher accuracy in identifying faulty models than SIVAND, CounterFactual Explanations, Integrated Gradients and SHAP.

Thanks to the recent breakthroughs in deep learning (DL) methods and ever-increasing computation power, nowadays DL models are being increasingly applied to all kinds of fields. They, along with other software modules, compose complex DL systems such as autonomous driving systems. Unfortunately, fatalities happen to these systems as is reported in real-life situations, e.g., traffic accidents involving autonomous driving vehicles. Further analyses show that this is because DL systems contain defects. To this end, understanding defects in DL systems is critical for preventing such accidents. To help improve the reliability of DL systems, many researchers have devoted efforts to their testing. In this paper, we investigated state-of-the-art methods through in-depth exploration. Firstly, we made a detailed analysis of deep learning system defects. We proposed a defect classification scheme, and summarized the characteristics of defects and their impacts on the system. Secondly, we systematically investigated the detection methods and tools and evaluated their capability in defect detection.

Interrupt-driven programs are widely deployed in safety-critical embedded systems to perform hardware and resource dependent data operation tasks. The frequent use of interrupts in these systems can cause race conditions to occur due to interactions between application tasks and interrupt handlers (or two interrupt handlers). Numerous program analysis and testing techniques have been proposed to detect races in multithreaded programs. Little work, however, has addressed race condition problems related to hardware interrupts. In this paper, we present SDRacer, an automated framework that can detect, validate and repair race conditions in interrupt-driven embedded software. It uses a combination of static analysis and symbolic execution to generate input data for exercising the potential races. It then employs virtual platforms to dynamically validate these races by forcing the interrupts to occur at the potential racing points. Finally, it provides repair candidates to eliminate the detected races. We evaluate SDRacer on nine real-world embedded programs written in C language. The results show that SDRacer can precisely detect and successfully fix race conditions.

Jiaqi Guo, Ziliang Si, Yu Wang, Qian Liu, Ming Fan, Jian-Guang Lou, Zijiang Yang, Ting Liu. Proceedings of the 59th Annual Meeting of the Association for Computational Linguistics and the 11th International Joint Conference on Natural Language Processing (Volume 1: Long Papers). 2021.

Background: Firmware is the enable software of Internet of Things (IoT) devices, and its software vulnerabilities are one of the primary reason of IoT devices being exploited. Due to the limited resources of IoT devices, it is impractical to deploy sophisticated run-time protection techniques. Under an insecure network environment, when a firmware is exploited, it may lead to denial of service, information disclosure, elevation of privilege, or even life-threatening. Therefore, firmware vulnerability detection by fuzzing has become the key to ensure the security of IoT devices, and has also become a hot topic in academic and industrial research. With the rapid growth of the existing IoT devices, the size and complexity of firmware, the variety of firmware types, and the firmware defects, existing IoT firmware fuzzing methods face challenges. Objective: This paper summarizes the typical types of IoT firmware fuzzing methods, analyzes the contribution of these works, and summarizes the shortcomings of existing fuzzing methods. Method: We design several research questions, extract keywords from the research questions, then use the keywords to search for related literature. Result: We divide the existing firmware fuzzing work into real-device-based fuzzing and simulation-based fuzzing according to the firmware execution environment, and simulation-based fuzzing is the mainstream in the future; we found that the main types of vulnerabilities targeted by existing fuzzing methods are memory corruption vulnerabilities; firmware fuzzing faces more difficulties than ordinary software fuzzing. Conclusion: Through the analysis of the advantages and disadvantages of different methods, this review provides guidance for further improving the performance of fuzzing techniques, and proposes several recommendations from the findings of this review.

Learning distributed representations of source code has been a challenging task for machine learning models. Earlier works treated programs as text so that natural language methods can be readily applied. Unfortunately, such approaches do not capitalize on the rich structural information possessed by source code. Of late, Graph Neural Network (GNN) was proposed to learn embeddings of programs from their graph representations. Due to the homogeneous (i.e. do not take advantage of the program-specific graph characteristics) and expensive (i.e. require heavy information exchange among nodes in the graph) message-passing procedure, GNN can suffer from precision issues, especially when dealing with programs rendered into large graphs. In this paper, we present a new graph neural architecture, called Graph Interval Neural Network (GINN), to tackle the weaknesses of the existing GNN. Unlike the standard GNN, GINN generalizes from a curated graph representation obtained through an abstraction method designed to aid models to learn. In particular, GINN focuses exclusively on intervals (generally manifested in looping construct) for mining the feature representation of a program, furthermore, GINN operates on a hierarchy of intervals for scaling the learning to large graphs. We evaluate GINN for two popular downstream applications: variable misuse prediction and method name prediction. Results show in both cases GINN outperforms the state-of-the-art models by a comfortable margin. We have also created a neural bug detector based on GINN to catch null pointer deference bugs in Java code. While learning from the same 9,000 methods extracted from 64 projects, GINN-based bug detector significantly outperforms GNN-based bug detector on 13 unseen test projects. Next, we deploy our trained GINN-based bug detector and Facebook Infer, arguably the state-of-the-art static analysis tool, to scan the codebase of 20 highly starred projects on GitHub. Through our manual inspection, we confirm 38 bugs out of 102 warnings raised by GINN-based bug detector compared to 34 bugs out of 129 warnings for Facebook Infer. We have reported 38 bugs GINN caught to developers, among which 11 have been fixed and 12 have been confirmed (fix pending). GINN has shown to be a general, powerful deep neural network for learning precise, semantic program embeddings.

Dangling pointers have become an important class of software bugs that can lead to use-after-free and double-free vulnerabilities. So far, only a few approaches have been proposed to protect against dangling pointers, while most of them suffer from high overhead. In this paper, we propose a lightweight approach, named DangDone, to eliminate dangling pointers at compile time. Built upon the root cause of a dangling pointer, i.e., a pointer and its aliases are not nullified but the memory area they point to is deallocated, DangDone realizes the protection by inserting an intermediate pointer between the pointers (i.e., a pointer and its aliases) and the memory area they point to. Hence, nullifying the intermediate pointer will nullify the pointer and its aliases, which mitigates the vulnerabilities caused by dangling pointers. Experimental results have demonstrated that DangDone can protect target programs (i.e., the SPEC CPU benchmarks and the programs with known CVEs) with negligible runtime overhead (i.e., around 1% on average).

Interrupt-driven programs are widely deployed in safety-critical embedded systems to perform hardware and resource dependent data operation tasks. The frequent use of interrupts in these systems can cause race conditions to occur due to interactions between application tasks and interrupt handlers. Numerous program analysis and testing techniques have been proposed to detect races in multithreaded programs. Little work, however, has addressed race condition problems related to hardware interrupts. In this paper, we present SDRacer, an automated framework that can detect and validate race conditions in interrupt-driven embedded software. It uses a combination of static analysis and symbolic execution to generate input data for exercising the potential races. It then employs virtual platforms to dynamically validate these races by forcing the interrupts to occur at the potential racing points. We evaluate SDRacer on nine real-world embedded programs written in C language. The results show that SDRacer can precisely detect race conditions.

C programming language never performs automatic bounds checking in order to speed up execution. But bounds checking is absolutely necessary in any program. Because if a variable is out-of-bounds, some serious errors may occur during execution, such as endless loop or buffer overflows. When there are arrays used in a program, the index of an array must be within the boundary of the array. But programmers always miss the array bounds checking or do not perform a correct array bounds checking. In this paper, we perform static analysis based on taint analysis and data flow analysis to detect which arrays do not have correct array bounds checking in the program. And we implement an automatic static tool, Carraybound. And the experimental results show that Carraybound can work effectively and efficiently.

Existing CSP model checkers are incapable of verifying multiple properties concurrently in one run of a model checker, and when trying to alleviate state space explosion problem, most of reduction work are usually done after rather than before the complete state space was produced. Thus, A new CSP model checking tool named ACSPChecker was developed based on answer set programming, which is a declarative logic programming paradigm for solving combinational search problems with the feature of completely free of sequential dependencies, to verifying multiple properties concurrently in one run of a model checker. Additionally, It integrated an abstraction method, which could be used to alleviate the state space explosion before the complete state space was produced. Furthermore, a preprocessing technique of properties was proposed to improve the verification efficiency by reducing the expense spending on replicated verification of the same sub formulas. The feasibility and efficiency of ACSPChecker are illustrated by the experiments with a classic concurrency problem - dining philosophers problem.

Interrupt-driven programs are often embedded in safety-critical systems to perform hardware/resource dependent data operation tasks, such as data acquisition, processing, and transformation. The interrupt programs and tasks may happen in parallel which in a result causes indeterminist concurrent problems at runtime. Data race is one of the most popular problems challenging researchers and practitioners. Various static analysis, software testing approaches have been proposed to detect data races in source code, testing, and even production run. However, static analysis may report too many false positives due to the lack of execution information. Dynamic testing may miss some important races since it could not generate adequate test cases to test all possible execution scenarios. In this paper, we propose a hybrid approach to detect data races in interrupt-driven programs based on static analysis and dynamic simulation. We implemented a prototype tool and conducted a controlled experiment to demonstrate the applicability of our approach.