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.

Anjiang Wei, Yuheng Wu, Yingjia Wan, Tarun Suresh, Huanmi Tan, Zhanke Zhou, Sanmi Koyejo, Ke Wang, Alex Aiken. Proceedings of the 2025 Conference on Empirical Methods in Natural Language Processing. 2025.

Modern scientific discovery increasingly relies on high-performance computing for complex modeling and simulation. A key challenge in improving parallel program performance is efficiently mapping tasks to processors and data to memory, a process dictated by intricate, low-level system code known as mappers. Developing high-performance mappers demands days of manual tuning, posing a significant barrier for domain scientists without systems expertise. We introduce a framework that automates mapper development with generative optimization, leveraging richer feedback beyond scalar performance metrics. Our approach features the Agent-System Interface, which includes a Domain-Specific Language (DSL) to abstract away the low-level complexity of system code and define a structured search space, as well as AutoGuide, a mechanism that interprets raw execution output into actionable feedback. Unlike traditional reinforcement learning methods such as OpenTuner, which rely solely on scalar feedback, our method finds superior mappers in far fewer iterations. With just 10 iterations, it outperforms OpenTuner even after 1000 iterations, achieving $3.8\times$ faster performance. Our approach finds mappers that surpass expert-written mappers by up to $1.34\times$ speedup across nine benchmarks while reducing tuning time from days to minutes.

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.

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.

In this paper, we take a different angle to evaluate compiler optimizations than all existing works in compiler testing literature. In particular, we consider a specific scenario in software development, that is, when developers manually optimize a program to improve its performance, do compilers actually generate more efficient code with the help of developers' optimizations?

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.

Test-time adversarial attacks have posed serious challenges to the robustness of machine-learning models, and in many settings the adversarial perturbation need not be bounded by small $\ell_p$-norms. Motivated by attacks in program analysis and security tasks, we investigate $\textit{relational adversaries}$, a broad class of attackers who create adversarial examples in a reflexive-transitive closure of a logical relation. We analyze the conditions for robustness against relational adversaries and investigate different levels of robustness-accuracy trade-off due to various patterns in a relation. Inspired by the insights, we propose $\textit{normalize-and-predict}$, a learning framework that leverages input normalization to achieve provable robustness. The framework solves the pain points of adversarial training against relational adversaries and can be combined with adversarial training for the benefits of both approaches. Guided by our theoretical findings, we apply our framework to source code authorship attribution and malware detection. Results of both tasks show our learning framework significantly improves the robustness of models against relational adversaries. In the process, it outperforms adversarial training, the most noteworthy defense mechanism, by a wide margin.

Software APIs exhibit rich diversity and complexity which not only renders them a common source of programming errors but also hinders program analysis tools for checking them. Such tools either expect a precise API specification, which requires program analysis expertise, or presume that correct API usages follow simple idioms that can be automatically mined from code, which suffers from poor accuracy. We propose a new approach that allows regular programmers to find API misuses. Our approach interacts with the user to classify valid and invalid usages of each target API method. It minimizes user burden by employing an active learning algorithm that ranks API usages by their likelihood of being invalid. We implemented our approach in a tool called ARBITRAR for C/C++ programs, and applied it to check the uses of 18 API methods in 21 large real-world programs, including OpenSSL and Linux Kernel. Within just 3 rounds of user interaction on average per API method, ARBITRAR found 40 new bugs, with patches accepted for 18 of them. Moreover, ARBITRAR finds all known bugs reported by a state-of-the-art tool APISAN in a benchmark suite comprising 92 bugs with a false positive rate of only 51.5% compared to APISAN’s 87.9%.

Android apps are GUI-based event-driven software and have become ubiquitous in recent years. Obviously, functional correctness is critical for an app’s success. However, in addition to crash bugs, non-crashing functional bugs (in short as “non-crashing bugs” in this work) like inadvertent function failures, silent user data lost and incorrect display information are prevalent, even in popular, well-tested apps. These non-crashing functional bugs are usually caused by program logic errors and manifest themselves on the graphic user interfaces (GUIs). In practice, such bugs pose significant challenges in effectively detecting them because (1) current practices heavily rely on expensive, small-scale manual validation ( the lack of automation ); and (2) modern fully automated testing has been limited to crash bugs ( the lack of test oracles ). This paper fills this gap by introducing independent view fuzzing , a novel, fully automated approach for detecting non-crashing functional bugs in Android apps. Inspired by metamorphic testing, our key insight is to leverage the commonly-held independent view property of Android apps to manufacture property-preserving mutant tests from a set of seed tests that validate certain app properties. The mutated tests help exercise the tested apps under additional, adverse conditions. Any property violations indicate likely functional bugs for further manual confirmation. We have realized our approach as an automated, end-to-end functional fuzzing tool, Genie. Given an app, (1) Genie automatically detects non-crashing bugs without requiring human-provided tests and oracles (thus fully automated ); and (2) the detected non-crashing bugs are diverse (thus general and not limited to specific functional properties ), which set Genie apart from prior work. We have evaluated Genie on 12 real-world Android apps and successfully uncovered 34 previously unknown non-crashing bugs in their latest releases — all have been confirmed, and 22 have already been fixed. Most of the detected bugs are nontrivial and have escaped developer (and user) testing for at least one year and affected many app releases, thus clearly demonstrating Genie’s effectiveness. According to our analysis, Genie achieves a reasonable true positive rate of 40.9%, while these 34 non-crashing bugs could not be detected by prior fully automated GUI testing tools (as our evaluation confirms). Thus, our work complements and enhances existing manual testing and fully automated testing for crash bugs.

Learning neural program embeddings is key to utilizing deep neural networks in program languages research --- precise and efficient program representations enable the application of deep models to a wide range of program analysis tasks. Existing approaches predominately learn to embed programs from their source code, and, as a result, they do not capture deep, precise program semantics. On the other hand, models learned from runtime information critically depend on the quality of program executions, thus leading to trained models with highly variant quality. This paper tackles these inherent weaknesses of prior approaches by introducing a new deep neural network, Liger, which learns program representations from a mixture of symbolic and concrete execution traces. We have evaluated Liger on two tasks: method name prediction and semantics classification. Results show that Liger is significantly more accurate than the state-of-the-art static model code2seq in predicting method names, and requires on average around 10x fewer executions covering nearly 4x fewer paths than the state-of-the-art dynamic model DYPRO in both tasks. Liger offers a new, interesting design point in the space of neural program embeddings and opens up this new direction for exploration.

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.

This paper introduces the “Search, Align, and Repair” data-driven program repair framework to automate feedback generation for introductory programming exercises. Distinct from existing techniques, our goal is to develop an efficient, fully automated, and problem-agnostic technique for large or MOOC-scale introductory programming courses. We leverage the large amount of available student submissions in such settings and develop new algorithms for identifying similar programs, aligning correct and incorrect programs, and repairing incorrect programs by finding minimal fixes. We have implemented our technique in the Sarfgen system and evaluated it on thousands of real student attempts from the Microsoft-DEV204.1x edX course and the Microsoft CodeHunt platform. Our results show that Sarfgen can, within two seconds on average, generate concise, useful feedback for 89.7% of the incorrect student submissions. It has been integrated with the Microsoft-DEV204.1X edX class and deployed for production use.

Manually providing feedback for programming assignments is a tedious task in traditional classroom education. The challenge increases drastically in Massive open online courses (MOOCs), where the student-teacher ratio can reach thousands to one or even millions to one. Despite the necessity, the current automated feedback approaches suffer from significant weaknesses: inability to scale to larger programs, manual involvement of teacher effort, and lack of precision for pin-pointing errors. We present a technique to tackle these challenges by developing a data-driven automated grader, iGrader, capable of generating instant and precise feedback for programming assignments.