Abstract In numeric-intensive computations, it is well known that the execution of floating-point programs is imprecise as floating-point arithmetic incurs round-off errors. Although round-off errors are small for a single floating-point operation, the aggregation of such errors may be dramatic and cause catastrophic program failures. Therefore, to ensure the correctness of floating-point programs, round-off error needs to be carefully taken into account. In this work, we consider polynomial invariant generation for floating-point programs, aiming at generating tight invariants under the perturbation of round-off errors. Our contribution is a novel framework for applying polynomial constraint solving to address the invariant generation problem, which is also the first polynomial constraint solving based approach that handles floating-point errors to our best knowledge. In our framework, we propose a novel combination of round-off error analysis and polynomial constraint solving, aiming to circumvent the cost of handling a large number of error variables in the floating-point model. Experimental results over a variety of challenging benchmarks show that our framework outperforms SOTA approaches in both time efficiency and the precision of generated invariants.

Software vulnerability detection is crucial for ensuring the security of software systems, representing a significant and challenging task. Recently, some studies have integrated large language models and graph neural networks to extract code features from different modalities (code sequences and graphs) for vulnerability detection. Unfortunately, current solutions struggle to fully leverage the complementary knowledge between modalities, thereby undermining their effectiveness in practical applications. In this paper, we proposeClara, a novel cross-modal learning approach that integrates multi-modal information from both global and local perspectives for effective detection. Specifically, for local fusion, we design an information interaction module guided by prompts, which employs learnable prompts to enhance feature extraction through the interaction of information between modalities. For global fusion, we devise a Cross-attention Adaptive Fusion module that adaptively adjusts the fusion weights of embeddings from different modalities using attention mechanisms. Experimental results on two benchmark datasets demonstrate thatClaraachieves improvements of 21.37% and 11.86% in F1 score over state-of-the-art vulnerability detection methods, respectively.

The software development process is characterized by an iterative cycle of continuous functionality implementation and debugging, essential for the enhancement of software quality and adaptability to changing requirements. This process incorporates two isolatedly studied tasks: Code Search (CS), which retrieves reference code from a code corpus to aid in code implementation, and Fault Localization (FL), which identifies code entities responsible for bugs within the software project to boost software debugging. The basic observation of this study is that these two tasks exhibit similarities since they both address search problems. Notably, CS techniques have demonstrated greater effectiveness than FL ones, possibly because of the precise semantic details of the required code offered by natural language queries, which are not readily accessible to FL methods. Drawing inspiration from this, we hypothesize that a fault localizer could achieve greater proficiency if semantic information about the buggy methods were made available. Based on this idea, we propose \(\texttt{CosFL}\) , an FL approach that decomposes the FL task into two steps: query generation , which describes the functionality of the problematic code in natural language, and fault retrieval , which uses CS to find program elements semantically related to the query, allowing for finishing the FL task from a CS perspective. Specifically, to depict the buggy functionalities and generate high-quality queries, \(\texttt{CosFL}\) extensively harnesses the code analysis, semantic comprehension, text generation, and decision-making capabilities of LLMs. Moreover, to enhance the accuracy of CS, \(\texttt{CosFL}\) captures varying levels of context information and employs a multi-granularity CS strategy, which facilitates a more precise identification of buggy methods from a holistic view. The evaluation on 835 real bugs from 23 Java projects shows that \(\texttt{CosFL}\) successfully localizes 324 bugs within Top-1, which significantly outperforms the state-of-the-art approaches by 26.6%–57.3%. The ablation study and sensitivity analysis further validate the importance of different components and the robustness of \(\texttt{CosFL}\) across different backend models.

The integration of Large Language Models (LLMs) into software development has revolutionized the field, particularly through the use of Retrieval-Augmented Code Generation (RACG) systems that enhance code generation with information from external knowledge bases. However, the security implications of RACG systems, particularly the risks posed by vulnerable code examples in the knowledge base, remain largely unexplored. This risk is particularly concerning given that public code repositories, which often serve as the sources for knowledge base collection in RACG systems, are usually accessible to anyone in the community. Malicious attackers can exploit this accessibility to inject vulnerable code into the knowledge base, making it toxic. Once these poisoned samples are retrieved and incorporated into the generated code, they can propagate security vulnerabilities into the final product. This paper presents the first comprehensive study on the security risks associated with RACG systems, focusing on how vulnerable code in the knowledge base compromises the security of generated code. We investigate the LLM-generated code security across different settings through extensive experiments using four major LLMs, two retrievers, and two poisoning scenarios. Our findings highlight the significant threat of knowledge base poisoning, where even a single poisoned code example can compromise up to 48% of generated code. Our findings provide crucial insights into vulnerability introduction in RACG systems and offer practical mitigation recommendations, thereby helping improve the security of LLM-generated code in future works.

As software evolves, test code must be co-maintained to ensure quality, but it often becomes obsolete, leading to failures that mislead developers and increase maintenance overhead. While recent Large Language Model (LLM)-based approaches show promise for repairing obsolete tests, their effectiveness is constrained by a critical challenge: providing comprehensive, repository-level context without overwhelming the models’ input limits. Fixed retrieval strategies often fail to capture the diverse dependencies required for complex repairs. In this paper, we present Trace, a retrieve-agent-based repository-level test repair method. The Trace selectively retrieves crucial context by analyzing (1) class-level structures to understand internal changes, (2) caller methods to capture real-world usage patterns, and (3) related files along the call graph to trace transitive dependencies. This multi-faceted context provides the LLM with a precise and concise understanding of the necessary code environment. We evaluated Trace on a dataset of real-world Java test updates, where it demonstrated superior performance compared to existing state-of-the-art baselines. Our results confirm that a structured, adaptive retrieval process is key to unlocking the full potential of LLMs for automated test maintenance.

Retrieval-Augmented Code Generation (RACG) leverages external knowledge to enhance Large Language Models (LLMs) in code synthesis, improving the functional correctness of the generated code. However, existing RACG systems largely overlook security, leading to substantial risks. Especially, the poisoning of malicious code into knowledge bases can mislead LLMs, resulting in the generation of insecure outputs, which poses a critical threat in modern software development. To address this, we propose a security-hardening framework for RACG systems, CodeGuarder, that shifts the paradigm from retrieving only functional code examples to incorporating both functional code and security knowledge. Our framework constructs a security knowledge base by analyzing real-world vulnerabilities from the ReposVul dataset. For each code generation query, a retriever decomposes the query into fine-grained sub-tasks and fetches relevant security knowledge. To prioritize critical security guidance, we introduce a re-ranking and filtering mechanism by leveraging the LLMs' susceptibility to different vulnerability types. This filtered security knowledge is seamlessly integrated into the generation prompt. Our evaluation shows CodeGuarder significantly improves code security rates across various LLMs, achieving average improvements of 20.12% in standard RACG, and 31.53% and 21.91% under two distinct poisoning scenarios without compromising functional correctness. Furthermore, CodeGuarder demonstrates strong generalization, enhancing security even when the targeted language's security knowledge is lacking. This work presents CodeGuarder as a pivotal advancement towards building secure and trustworthy RACG systems.

Floating-point exceptions are hard to avoid and can cause disastrous consequences. However, testing methods for floating-point exceptions in GPU programs are currently quite limited due to their closed-source nature. Existing tools, even the state-of-the-art Xscope, still exhibit low search efficiency and poor input coverage. In this paper, we combine interval-wise random sampling and Markov Chain Monte Carlo (MCMC) sampling in a synergistic way to efficiently detect exception-inducing inputs in GPU programs. To improve the search efficiency, based on the bit patterns of exceptional floating-point values, we propose a floating-point format-aware input space partitioning method for random sampling and define a unified fitness function for MCMC sampling. We implement our approach in a tool DFEG and demonstrate it on 76 functions from the CUDA Math Library, HPC programs, and FPBench. DFEG outperforms Xscope in terms of both effectiveness and efficiency. DFEG finds$949 \times$more exceptions than Xscope and detects new exceptions in 9 functions where Xscope fails. Moreover, compared to Xscope, DFEG achieves an average$34 \times$speedup.

Fault localization (FL) is a critical but time-consuming part of software debugging. With the improvement of the Large Language Models (LLMs) in their code capabilities, the increasing demand for automated software development has encouraged more research on building LLM-based Fault Localization (LLMFL) systems. However, existing LLMFL techniques are typically restricted to predicting bug locations by analyzing static code, while overlooking crucial dynamic program state of the software. This lack of context makes LLMs prone to generating "hallucinations", incorrectly identifying bug-free code as suspicious. To address this, this paper introduces PingFL, the LLMFL system that incorporates program dynamic information for more accurate automatic fault localization. PingFL comprises a Fault Localization (FL) agent and a Print Debugging (PD) agent. The FL agent is tasked with understanding the root cause through a set of callable tools. When the FL agent nominates a location as suspicious, it would entrust the PD agent to verify the suspected issue through multiple rounds of print debugging. In particular, these two agents communicate efficiently by conveying the textual thought generated by the LLM. The evaluation on 812 real-world bugs from the Defects4J benchmark shows that PingFL can localize 450 bugs within Top-1, which significantly outperforms other LLM-based approaches by 41% to 122%. A deeper dive into PingFL’s performance reveals that it exhibits specific FL strategies and tool usage patterns even without explicit instructions. Finally, PingFL proves to be cost-effective, spending an average of $0.23 and 104.62 seconds per bug, with the print debugging mechanism accounting for only $0.07 and 48.14 seconds.

With the advancement of neural networks, neural network controlled systems (NNCSs) are increasingly deployed in safety-critical scenarios, making the safety verification of NNCSs imperative. Traditional verification methods based on overapproximated reachability analysis introduce precision loss during the verification process, which may lead to “Unknown” results. Moreover, standalone forward reachability analysis often fails to incorporate target safety properties into its verification process, while backward reachability analysis does not account for input constraints. To address these challenges, this paper proposes an iterative refinement approach by combining forward and backward reachability analysis. For a given safety property, our method guides state space partitioning and pruning on-the-fly by making use of the target safety constraints when verification results remain “Unknown”. By partitioning the state space into smaller subspaces, the precision loss due to overapproximation is significantly mitigated. Additionally, integrating forward and backward reachability analysis further counteracts these overapproximation effects through pruning, ultimately yielding more accurate verification outcomes. We demonstrate that our approach successfully verifies the system's safety properties with a 100% success rate across four benchmarks, whereas other verification tools for NNCSs such as Reach-LP-GSG, BReach-LP, and DRIP-Hpoly either return “Unknown” results or require up to$29 \%, 60 \%$, and 232% more time.

Despite its effectiveness in ensuring software quality, code review remains a labor-intensive and time-consuming task. In order to alleviate this burden on developers, researchers have proposed the automation of code review activities, particularly focusing on automating code revisions. This automation can benefit both code authors, as they are relieved from the manual task of code revision, and code reviewers, as they are spared from addressing minor code flaws through manual comments. While current code revision approaches have shown promising results, they typically operate within a single phase, in which the code requiring revision is treated as the input of a deep learning model, and the revised code is directly generated through a sequence-to-sequence transformation. Consequently, these approaches tackle both the challenges of localization (i.e., where to revise) and revision (i.e., how to revise) simultaneously. Attempting to handle the entire complex process with a single model goes against the principle of “Divide-and-Conquer,” which encourages breaking down complex problems into smaller sub-problems and addressing them individually. In fact, we have observed that existing code revision approaches often yield inaccurate results in both the localization and revision phases. In this article, we present a two-phase code revision approach that aims to overcome the aforementioned limitations by adhering to the “Divide-and-Conquer” principle. Our approach comprises two key components: a localizer, responsible for identifying the specific parts of the input code that require revisions, and a reviser, tasked with generating the revised code based on the localization result. Extensive experiments conducted on two widely used datasets demonstrate the substantial superiority of our approach over existing code revision approaches. For instance, when revising code based on the code reviewer’s comments, our approach achieves a success rate of over 20% in implementing the ground-truth code revisions. In comparison, the widely used pre-trained model CodeT5 achieves a success rate of less than 16% on the same test set, which contains 16K+ cases.

As software grows in complexity to accommodate diverse features and platforms, software bloating has emerged as a significant challenge, adversely affecting performance and security. However, existing approaches inadequately address the dual objectives of debloating: maintaining functionality by preserving essential features and enhancing security by reducing security issues. Specifically, current software debloating techniques often rely on input-based analysis, using user inputs as proxies for the specifications of desired features. However, these approaches frequently overfit provided inputs, leading to functionality loss and potential security vulnerabilities. To address these limitations, we proposeLEADER, a program debloating framework enhanced by Large Language Models (LLMs), which leverages their semantic understanding, generative capabilities, and decision-making strengths.LEADERmainly consists of two modules: (1) a documentation-guided test augmentation module designed to preserve functionality, which leverages LLMs to comprehend program documentation and generates sufficient tests to cover the desired features comprehensively, and (2) a multi-advisor-aided program debloating module that employs a neuro-symbolic pipeline to ensure that the security of the software can be perceived during debloating. This module combines debloating and security advisors for analysis and employs an LLM as a decision-maker to eliminate undesired code securely. Extensive evaluations on widely used benchmarks demonstrate the efficacy ofLEADER. It achieves a 95.5% test case pass rate and reduces program size by 42.5%. Notably, it reduces the introduction of vulnerabilities during debloating by 79.1% and decreases pre-existing vulnerabilities by 16.5% more than CovA. These results demonstrate thatLEADERsurpasses the state-of-the-art tool CovA in functionality and security. These results underscore the potential ofLEADERto set a new standard in program debloating by effectively balancing functionality and security.

Software vulnerability detection is crucial for high-quality software development. Recently, some studies utilizing Graph Neural Networks (GNNs) to learn the graph representation of code in vulnerability detection tasks have achieved remarkable success. However, existing graph-based approaches mainly face two limitations that prevent them from generalizing well to large code graphs: (1) the interference of noise information in the code graph; (2) the difficulty in capturing long-distance dependencies within the graph. To mitigate these problems, we propose a novel vulnerability detection method,ANGEL, whose novelty mainly embodies the hierarchical graph refinement and context-aware graph representation learning. The former hierarchically filters redundant information in the code graph, thereby reducing the size of the graph, while the latter collaboratively employs the Graph Transformer and GNN to learn code graph representations from both the global and local perspectives, thus capturing long-distance dependencies. Extensive experiments demonstrate promising results on three widely used benchmark datasets: our method significantly outperforms several other baselines in terms of the accuracy and F1 score. Particularly, in large code graphs,ANGELachieves an improvement in accuracy of 34.27%-161.93% compared to the state-of-the-art method, AMPLE. Such results demonstrate the effectiveness ofANGELin vulnerability detection tasks.

Neural network verification, particularly verification of robustness properties, has received much research attention. However, many existing verification methods overlook the influence of floating-point rounding errors in the deployed neural networks, resulting in unsound verification outcomes. In this paper, we propose a sound robustness verification approach aiming at overcoming this limitation. Our method utilizes real-number intervals to approximate floating-point arithmetic and abstracts floating-point neural networks into equivalent networks using real-number interval arithmetic semantics, thereby effectively taking into account for floating-point rounding errors. We sub-sequently employ exact MILP formulations to verify robustness over these abstracted networks. We introduce FMIPVerify, a dedicated verification tool tailored to ensure the soundness of floating-point neural network verification. Experimental results demonstrate that FMIPVerify significantly improves the robustness verification ability in floating-point ReLU neural networks compared to established complete methods like MIPVerify.

Vulnerabilities exert great burden on developers in terms of debugging and maintenance. Automated Vulnerability Repair(AVR) is considered as a promising approach to alleviate the burden of developers. Template-based automated program repair techniques have shown their effectiveness in fixing general bugs. However, due to the diverse root causes of vulnerabilities, it is challenging to construct sufficient repair templates to cover various vulnerabilities. In this paper, we introduce a Template-guided Retrieval-Augmented Patch generation approach, named T-RAP. Inspired by retrieval-augmented techniques that effectively utilize historical data, our approach leverages repair templates to extract similar vulnerability repair patches from the codebase. These patches then guide the process of generating vulnerability patches. To extract similar patches, we also propose a matching algorithm specifically designed for the retrieval-augmented vulnerability repair. This involves identifying similarities between numerous templates and vulnerabilities during the template-guided stage. Experimental results demonstrate that T-RAP outperforms all the studied AVR approaches, repairing 56.8% more vulnerabilities than VulRepair and 30.24% more than VulMaster. It can also accurately repair more types of real-world vulnerabilities than VulMaster. Additionally, we evaluated the effectiveness of our patch retriever. The results indicate that our template-guided retriever, which is based on our matching algorithm, outperforms the retrieval algorithm proposed in the recent retrieval-augmented patch generation approach RAP-Gen.

Software vulnerabilities inevitably arise during software development and may leave behind huge security risks. In order to detect and mitigate vulnerabilities before they can be exploited, various fine-grained deep learning (DL)-based vulnerablity detection (VD) approaches have been proposed to locate vulnerable statements, among which the Transformer-based methods have shown promising performances. However, existing Transformer-based statement-level approaches still suffer from a crucial limitation: they ignore the intrinsic data/control dependency relations between the statements. In this work, we propose a novel Transformer-based model MatsVD, which aims to address the above challenge from two aspects: Firstly, inspired by the hierarchical structure of code (i.e., tokens, statements, and functions), MatsVD comprises three different Transformer-based layers (i.e., statement embedding layer, statement representation layer, and function representation layer) to gradually aggregate the basic code tokens into meaningful statement/function representations; Secondly, to further exploit the data/control dependencies between statements, we replace the original attention mechanism of the Transformer with a novel dependency-based attention by masking irrelevant attention scores according to the program dependency graph. We comprehensively evaluate MatsVD on the widely used C/C++ vulnerability dataset Big-Vul. The results show that MatsVD significantly outperforms 6 other statement-level methods on both binary classification and ranking metrics. In particular, MatsVD obtains an F1 score of 86% and a Top-1 Accuracy of 93% on statement-le, which improves by respectively 22.97% and 7.76% compared to the state-of-the-art method VELVET.

Automated program repair aims to automate bug correction and alleviate the burden of manual debugging, which plays a crucial role in software development and maintenance. Recent studies reveal that learning-based approaches have outperformed conventional APR techniques (e.g., search-based APR). Existing learning-based APR techniques mainly center on treating program repair either as a translation task or a cloze task. The former primarily emphasizes statement-level repair, while the latter concentrates on token-level repair, as per our observations. In practice, however, patches may manifest at various repair granularity, including statement, expression, or token levels. Consequently, merely generating patches from a single granularity would be ineffective to tackle real-world defects. Motivated by this observation, we propose Mulpor, a multi-granularity patch generation approach designed to address the diverse nature of real-world bugs. Mulpor comprises three components: statement-level, expression-level, and token-level generator, each is pre-trained to generate correct patches at its respective granularity. The approach involves generating candidate patches from various granularities, followed by a re-ranking process based on a heuristic to prioritize patches. Experimental results on the Defects4J dataset demonstrate that Mulpor correctly repair 92 bugs on Defects4J-v1.2, which achieves 27.0% (20 bugs) and 12.2% (10 bugs) improvement over the previous state-of-the-art NMT-style Rap-Gen and Cloze-style GAMMA. We also studied the generalizability of Mulpor in repairing vulnerabilities, revealing a notable 51% increase in the number of correctly-fixed patches compared with state-of-the-art vulnerability repair approaches. This paper underscores the importance of considering multiple granularities in program repair techniques for a comprehensive strategy to address the diverse nature of real-world software defects. Mulpor, as proposed herein, exhibits promising results in achieving effective and diverse bug fixes across various program repair scenarios.

Deep neural network (DNN) has been increasingly deployed as a key component in safety-critical systems. However, the credibility of DNN components is uncertain due to the absence of formal specifications for their data preconditions, which are essential for ensuring trustworthy postconditions.In this paper, we propose a guess-and-check-based framework PreBoxes to automatically synthesize Boxes sufficient preconditions for DNN concerning rich safety and robustness postconditions.The framework operates in two phases: the guess phase generates potentially complex candidate preconditions through heuristic methods, while the check phase verifies these candidates with formal guarantees.The entire framework supports automatic and adaptive iterative running to obtain weaker preconditions as well.Such resulting preconditions can be leveraged to shield DNN for safety and enhance the interpretability of DNN in application.PreBoxes has been evaluated on over 20 models with 23 trustworthy properties of 4 benchmarks and compared with 3 existing typical schemes.The results show that not only does PreBoxes generally infer weaker non-trivial sufficient preconditions for DNN than others, but also it expands competitive capabilities to handle both complex properties and Non-ReLU complex structured networks.

Floating-point arithmetic is notorious for its rounding errors, which can propagate and accumulate, leading to unacceptable results. Detecting inputs that can trigger significant floating-point errors is crucial for enhancing the reliability of numerical programs. Existing methods for generating error-triggering inputs often rely on costly shadow executions that involve high-precision computations or suffer from false positives. This paper introduces chain conditions to capture the propagation and accumulation of floating-point errors, using them to guide the search for error-triggering inputs. We have implemented a tool named FPCC and evaluated it on 88 functions from the GNU Scientific Library, as well as 21 functions with multiple inputs from previous research. The experimental results demonstrate the effectiveness and efficiency of our approach: (1) FPCC achieves 100% accuracy in detecting significant errors for the reported rank-1 inputs, while 72.69% rank-1 inputs from the state-of-the-art tool ATOMU can trigger significant errors. Overall, 99.64% (1049/1053) of the inputs reported by FPCC can trigger significant errors, whereas only 19.45% (141/723) of the inputs reported by ATOMU can trigger significant errors; (2) FPCC exhibits a 2.17x speedup over ATOMU in detecting significant errors; (3) FPCC also excels in supporting functions with multiple inputs, outperforming the state-of-the-art technique. To facilitate further research in the community, we have made FPCC available on GitHub at https://github.com/DataReportRe/FPCC .

Automated program repair is to reduce the manual work for bug fixing by human developers. In recent 15 years, the research community of program repair has created many novel techniques. However, these techniques share several assumptions that cannot always be satisfied in daily software development. This badly hurts the application of program repair in practice. For example, many repair techniques assume that test cases are well written before patch generation; many techniques assume that specific language features can be ignored (or already-processed). In this paper, we propose a framework of C program repair, which mainly addresses two challenges: test-independent repair and preprocessor directive processing. Our solution to test-independent repair is to automatically construct patch conditions for C programs via parsing the syntax structures; our solution to preprocessor directive processing is to generate code symbols to replace preprocessor directives. We plan to implement these potential solutions with program analysis techniques. The goal of this paper is to present practical solutions for developers to automate C program repair.

It is difficult to write a numerical program that does not incur floating-point exceptions in practice. To detect floatingpoint exceptions, most existing methods use static analysis, which may induce false alarms (due to over-approximation), or suffer from scalability issues (since solving floating-point constraints is expensive). Fuzzing is a widely used technique to finding bugs, but existing fuzzing techniques have not yet considered the specific format of floating-point and are lack of guidance for detecting floating-point exceptions. In this paper, we propose a floating-point format aware coverage-based grey-box fuzzing to detect floating-point exceptions for numerical programs. More specifically, we propose a novel mutation strategy for floating-point format aiming at producing valid floating-point test inputs. Moreover, we present a new guidance aiming to search for test inputs that are closer to exposing exceptions. We implement our approach as a tool, named NumFUZZ, based on AFL. We have conducted experiments to evaluate NUMFUZZ on GNU Scientific Library (GSL) and Sun’s C math library respectively. The preliminary experimental results suggest that our approach has promising ability in detecting floating-point exceptions and achieving high floating-point branch coverage in real-world numerical programs.

Abstract Worst-case resource usage provides a useful guidance in the design, configuration and deployment of software, especially when it runs under a context with limited amount of resources. Static resource-bound analysis can provide sound upper bounds of worst-case resource usage but may provide too conservative, even unbounded, results. In this paper, we present a resource-usage-aware fuzzing approach to estimate worst-case resource usage. The key idea is to guide the fuzzing process using resource-usage amount together with resource-usage relevant coverage. Moreover, we leverage semantic patch to make use of static analysis information (including control-flow, function-call, etc.) to instrument the original program, for the sake of aiding the subsequent fuzzing. We have conducted experiments to estimate worst-case resource usage of various resources in real-world programs, including heap memory, stack depths, sockets, user-defined resources, etc. The preliminary experimental results show the promising ability of our approach in estimating worst-case resource usage in real-world programs, compared with two state-of-the-art fuzzing tools (AFL and MemLock).

Automated program repair (APR) holds the promise of aiding manual debugging activities. Over a decade of evolution, a broad range of APR techniques have been proposed and evaluated on a set of real-world bug datasets. However, while more and more bugs have been correctly fixed, we observe that the growth of newly fixed bugs by APR techniques has hit a bottleneck in recent years. In this work, we explore the possibility of addressing complicated bugs by proposing TransplantFix, a novel APR technique that leverages graph differencing-based transplantation from the donor method. The key novelty of TransplantFix lies in three aspects: 1) we propose to use a graph-based differencing algorithm to distill semantic fix actions from the donor method; 2) we devise an inheritance-hierarchy-aware code search approach to identify donor methods with similar functionality; 3) we present a namespace transfer approach to effectively adapt donor code.

Safety and robustness properties are highly required for neural networks deployed in safety-critical applications. Current complete verification techniques of these properties suffer from the lack of efficiency and effectiveness. In this article, we present an efficient complete approach to verify safety and robustness properties of neural networks through incrementally determinizing activation states of neurons. The key idea is to generate constraints via layerwised splitting that make activation states of hidden neurons become deterministic efficiently. These constraints are then utilized for refining inputs systematically so that abstract analysis over the refined input can be more precise. Our approach decomposes a verification problem into a set of subproblems via layerwised input space splitting. The property is then checked on each subproblem, where the activation states of at least one hidden neurons will be determinized. Further checking is accelerated by constraint-guided input refinement. We have implemented a parallel tool called LayerSAR to verify safety and robustness properties of ReLU neural networks in a sound and complete way, and evaluated it extensively on several benchmark sets. Experimental results show that our approach is promising, compared with complete tools, such as Planet, Neurify, Marabou, ERAN, Venus, Venus2, and nnenum in verifying safety and robustness properties on the benchmarks.

Analyzing worst-case resource usage of a program is a difficult but important problem. Existing static bound analysis techniques mainly focus on deriving the upper-bound number of visits to a given control location or iterations of a loop. However, there still exist gaps between such bounds and resource usage bounds. In this paper, we present a static analysis approach to derive resource usage bounds for imperative programs. We leverage techniques of program transformation, numerical value analysis, pointer analysis and program slicing, to model and analyze resource usage in a program. We have conducted experiments to derive usage bounds of various resources in C programs, including heap memory, file descriptors, sockets, user-defined resources, etc. The result suggests that our approach can infer usage bounds of resources in practical imperative programs.

Linear programming is a key technique for analysis and verification of numerical properties in programs, neural networks, etc. In particular, in program analysis based on abstract interpretation, many numerical abstract domains (such as Template Constraint Matrix, constraint-only polyhedra, etc.) are designed on top of linear programming. However, most state-of-the-art linear programming solvers use floating-point arithmetic in their implementations, leading to an approximate result that may be unsound. On the other hand, the solvers implemented using exact arithmetic are too costly. To this end, this paper focuses on advancing rigorous linear programming techniques based on floating-point arithmetic for building sound and efficient program analysis. Particularly, as a supplement to existing techniques, we present a novel rigorous linear programming technique based on Fourier-Mozkin elimination. On this basis, we implement a tool, namely, RlpSolver, combining our technique with existing techniques to lift effectiveness of rigorous linear programming in the scene of analysis and verification. Experimental results show that our technique is complementary to existing techniques, and their combination (RlpSolver) can achieve a better trade-off between cost and precision via heuristic rules.

In this work-in-progress innovative practice paper, we argue the application-ability training in Discrete Mathematics (DM) should be enhanced for students majoring in computing science. Our motivation is based on the analysis of the differences in learning outcomes between DM and other branches of Math courses, the special role of DM in computer science (CS) courses and the gaps between DM and other CS courses. Motivated by the above analysis, we rethink of CS undergraduate education program as a DM-centric program. Furthermore, we make an experimental implementation of the DM-centric program and enhance application-ability training by designing and adopting many large-scale projects from various related topics, such as database, satisfiability, deductive proof and so on. Each project is decomposed into several sub-projects, which are integrated with a project-based learning environment. The large-scale projects derived from related CS courses enable students to get in touch with various computing topics related to DM applications at an early stage in the learning process. The learning environment with the ability of automatic assessment enables students to complete the projects in a step-by-step manner. The preliminary feedback from 219 students after taking the redesigned DM course shows the promising effects on students' following learning.

It is widely desired to precisely predict bounds of resource usages statically in a program, particularly when the program runs in resource-limited contexts. The resource bound problem becomes more challenging for C programs due to the allowed flexible manipulations on dynamically allocated resources in C. In this paper, we present a static analysis approach to deriving the bounds of dynamically allocated resources for C programs. The key idea is to combine numerical value analysis with pointer analysis under the unified framework of abstract interpretation. First, to track resource usage, we intro-duce auxiliary numerical variables to model the resource usage due to resource-manipulating functions such as allocation and deallocation. Second, to handle resource-manipulating functions involving pointers as parameters or return values, we propose a pointer analysis approach designed specifically for resource bound analysis, and combine it with numerical value analysis, to handle pointer arithmetics, dynamic allocation and deallocation, etc. Then, we infer the value bound of auxiliary resource-usage modeling variables to predict resource bounds at each program location. We have implemented our approach in a tool called DARB and conducted experiments on a set of benchmarks extracted from real-world programs. The results show that DARB can deal with C programs with complex resource manipulations.

The classic linear (technically, affine) equality abstract domain, which can infer linear equality relations among variables of a program automatically, is one of the earliest and fundamental abstract domains. As a lightweight relational abstract domain, it has been widely used in program analysis. However, it cannot express non-convex properties that appear naturally due to the inherent disjunctive behaviors in a program. In this paper, we introduce a new abstract domain, namely the abstract domain of linear absolute value equalities, which generalizes the linear equality abstract domain with absolute value terms of variables. More clearly, we leverage the absolute value function to design the new abstract domain for discovering linear equality relations among values and absolute values of program variables. The new abstract domain can be used to infer piecewise linear behaviors (e.g., due to conditional branches, absolute value function calls, max/min function calls, etc.) in a program. Experimental results of our prototype are encouraging: In practice, the new abstract domain can find interesting piece-wise linear invariants that are non-convex and out of the expressiveness of the linear equality domain.

Abstract Deep neural networks (DNNs) have been shown lack of robustness, as they are vulnerable to small perturbations on the inputs. This has led to safety concerns on applying DNNs to safety-critical domains. Several verification approaches based on constraint solving have been developed to automatically prove or disprove safety properties for DNNs. However, these approaches suffer from the scalability problem, i.e., only small DNNs can be handled. To deal with this, abstraction based approaches have been proposed, but are unfortunately facing the precision problem, i.e., the obtained bounds are often loose. In this paper, we focus on a variety of local robustness properties and a ( δ , ε ) -global robustness property of DNNs, and investigate novel strategies to combine the constraint solving and abstraction-based approaches to work with these properties: We propose a method to verify local robustness, which improves a recent proposal of analyzing DNNs through the classic abstract interpretation technique, by a novel symbolic propagation technique. Specifically, the values of neurons are represented symbolically and propagated from the input layer to the output layer, on top of the underlying abstract domains. It achieves significantly higher precision and thus can prove more properties. We propose a Lipschitz constant based verification framework. By utilising Lipschitz constants solved by semidefinite programming, we can prove global robustness of DNNs. We show how the Lipschitz constant can be tightened if it is restricted to small regions. A tightened Lipschitz constantcan be helpful in proving local robustness properties. Furthermore, a global Lipschitz constant can be used to accelerate batch local robustness verification, and thus support the verification of global robustness. We show how the proposed abstract interpretation and Lipschitz constant based approaches can benefit from each other to obtain more precise results. Moreover, they can be also exploited and combined to improve constraints based approach. We implement our methods in the tool PRODeep, and conduct detailed experimental results on several benchmarks

Software merging is an important activity during software development. Merge conflicts may arise and degrade the software quality. Empirical studies on software merging are helpful to understand developers' needs and the challenges of detecting and resolving conflicts. Existing studies collect merges by identifying commits that have more than one parent commit. Different from these explicit merges, rebasing branches is used to merge other changes but rewrites the evolutionary history. Hence, existing studies fail to identify implicit merges performed by rebasing branches. Consequently, the results of these studies may fail to provide comprehensive insights on software merging. In our study, we leverage the recently updated APIs of GitHub to study rebase activities in the pull requests. Our study shows that rebasing is widely used in pull requests. And our results indicate that, to resolve textual conflicts, developers adopt similar strategies shown in existing studies on explicit merges. However, in 34.2% of non-conflict rebase scenarios, developers add new changes during the rebase process. And this indicates that there are some new challenges of validating rebases. Our results provide useful insights for improving the state-of-the-art techniques on resolving conflicts and validating rebases.

Detecting bugs in deep learning software at the architecture level provides additional benefits that detecting bugs at the model level does not provide. This paper makes the first attempt to conduct static analysis for detecting numerical bugs at the architecture level. We propose a static analysis approach for detecting numerical bugs in neural architectures based on abstract interpretation. Our approach mainly comprises two kinds of abstraction techniques, i.e., one for tensors and one for numerical values. Moreover, to scale up while maintaining adequate detection precision, we propose two abstraction techniques: tensor partitioning and (elementwise) affine relation analysis to abstract tensors and numerical values, respectively. We realize the combination scheme of tensor partitioning and affine relation analysis (together with interval analysis) as DEBAR, and evaluate it on two datasets: neural architectures with known bugs (collected from existing studies) and real-world neural architectures. The evaluation results show that DEBAR outperforms other tensor and numerical abstraction techniques on accuracy without losing scalability. DEBAR successfully detects all known numerical bugs with no false positives within 1.7–2.3 seconds per architecture. On the real-world architectures, DEBAR reports 529 warnings within 2.6–135.4 seconds per architecture, where 299 warnings are true positives.

Numerical computation is often involved in software of embedded control systems, cyber-physical systems, artificial neural network systems, big data processing systems, etc. Automatically discovering numerical loop invariants is fundamental for checking the safety of such software. Abstract interpretation provides a framework to automatically discover sound invariants but which may be not precise enough due to over-approximations. One major source of precision loss is due to the limited linear expressiveness of most widely used numerical abstract domains and the widening operation. This becomes more serious when analyzing all variables simultaneously as a whole for programs that involve nonlinear behaviors. Based on the observation that the dependency among variables in a loop can be hierarchical, in this article, we propose a hierarchical static analysis to analyze a loop by utilizing relaxed abstract transformers. The main idea is to first partition all variables involved in a loop into different hierarchical layers, then compute invariants over the variables layer by layer in a bottom-up manner. During the iterative process, the computed invariants over lower layer variables are then used to relax transfer functions when analyzing the higher layer variables. One benefit of our method lies in that it can generate linear invariants to soundly enclose nonlinear behaviors in a loop. Finally, we present encouraging experimental results on benchmark programs involving nonlinear behaviors.

Background: Over the years, Automated Program Repair (APR) has attracted much attention from both academia and industry since it can reduce the costs in fixing bugs. However, how to assess the patch correctness remains to be an open challenge. Two widely adopted ways to approach this challenge, including manually checking and validating using automated generated tests, are biased (i.e., suffering from subjectivity and low precision respectively). Aim: To address this concern, we propose to conduct an empirical study towards understanding the correct patches that are generated by existing state-of-the-art APR techniques, aiming at providing guidelines for future assessment of patches. Method: To this end, we first present a Literature Review (LR) on the reported correct patches generated by recent techniques on the Defects 4J benchmark and collect 177 correct patches after a process of sanity check. We investigate how these machine-generated correct patches achieve semantic equivalence, but syntactic difference compared with developer-provided ones, how these patches distribute in different projects and APR techniques, and how the characteristics of a bug affect the patches generated for it. Results: Our main findings include: 1) we do not need to fix bugs exactly like how developers do since we observe that 25.4% (45/177) of the correct patches generated by APR techniques are syntactically different from developer-provided ones; 2) the distribution of machine-generated correct patches diverges for the aspects of Defects 4J projects and APR techniques; and 3) APR techniques tend to generate patches that are different from those by developers for bugs with large patch sizes. Conclusion: Our study not only verifies the conclusions from previous studies but also highlights implications for future study towards assessing patch correctness.

Floating point computation is by nature inexact, and numerical libraries that intensively involve floating-point computations may encounter high floating-point errors. Due to the wide use of numerical libraries, it is highly desired to reduce high floating-point errors in them. Using higher precision will degrade performance and may also introduce extra errors for certain precision-specific operations in numerical libraries. Using mathematical rewriting that mostly focuses on rearranging floating-point expressions or taking Taylor expansions may not fit for reducing high floating-point errors evoked by ill-conditioned problems that are in the nature of the mathematical feature of many numerical programs in numerical libraries. In this paper, we propose a novel approach for efficient automated repair of high floating-point errors in numerical libraries. Our main idea is to make use of the mathematical feature of a numerical program for detecting and reducing high floating-point errors. The key components include a detecting method based on two algorithms for detecting high floating-point errors and a repair method for deriving an approximation of a mathematical function to generate patch to satisfy a given repair criterion. We implement our approach by constructing a new tool called AutoRNP. Our experiments are conducted on 20 numerical programs in GNU Scientific Library (GSL). Experimental results show that our approach can efficiently repair (with 100% accuracy over all randomly sampled points) high floating-point errors for 19 of the 20 numerical programs.

Real-world bugs and the bug-fix activities are essential in many fields such as bug prediction and automatic program repair. Identifying bug-fix commits from version histories has received much recent attention. Linking commits to bug reports and analyzing the commits individually are common practice. However, considering the one-to-many relationship between the bug report and the bug-fix commits, analyzing commits individually will miss the relevance between commits, since several commits might fix the same bug together. In addition, some supplementary bug-fix commits which supplement or correct the identified bug-fix commit may be neglected. For empirical studies on bug-fix commits, it is important to study all the relevant commits as a whole, otherwise we will fail to understand the complete real bug-fix activities. In this paper, we investigate the relevance between bug-fix commits that are linked to the same bug-fix pull request, and utilize machine learning techniques to determine supplementary bug-fix commits for an identified bug-fix commit. Experimental results show that there indeed exist supplementary bug-fix commits (i.e., 19.8% on average) that are neglected when analyzing commits individually. The performance of our tool SupBCFinder is much better than that of using a sliding window of one hour and that of analyzing the local change. Moreover, inspired by our learning-based approach and extracted features, we propose one effective heuristic as an alternative for the cases when there are not enough pull requests for training.

User-space programs rely on memory allocation primitives when they need to construct dynamic structures such as lists or trees. However, low-level OS kernel services and embedded device drivers typically avoid resorting to an external memory allocator in such cases, and store structure elements in contiguous arrays instead. This programming pattern leads to very complex code, based on data-structures that can be viewed and accessed either as arrays or as chained dynamic structures. The code correctness then depends on intricate invariants mixing both aspects. We propose a static analysis that is able to verify such programs. It relies on the combination of abstractions of the allocator array and of the dynamic structures built inside it. This approach allows to integrate program reasoning steps inherent in the array and in the chained structure into a single abstract interpretation. We report on the successful verification of several embedded OS kernel services and drivers.

Floating-point rounding errors are pervasive when using numerical code to implement the real arithmetic algorithm. In particular, high floating-point inaccuracies may cause serious problems once being triggered. Hence, a testing method that can find concrete test cases to trigger high floating-point inaccuracies, is quite helpful to aid debugging and reduce high inaccuracies. Recently, two testing approaches have been proposed to find inputs triggering high floating-point inaccuracies in numerical programs: Locality-Sensitive Genetic Algorithm (LSGA) and Binary Guided Random Testing (BGRT). However, experiments show that LSGA may result in a high rate of false alarm while BART may easily fall into a local maximum when the search space is large. In this paper, we propose a novel testing approach to trigger high floating-point inaccuracies in numerical code. The main idea is utilizing heuristic rules drawn from error analysis to guide the process of global search of test cases. Comparative experiments with the random and BGRT methods are conducted on benchmarks including real-world scientific programs. Experimental results show that our approach can efficiently find inputs that trigger higher floating-point inaccuracies in 11 of 12 real-world programs (especially for programs whose input space are large) and have better stability.

Rounding errors are introduced pervasively when using floating-point arithmetic to approximate real arithmetic. The accumulation or catastrophic cancellation of rounding errors in numerical programs may produce high inaccuracy results, which can cause serious software failures once being triggered. High inaccuracies are known hard to debug and fix manually for developers. Hence, the automated techniques are desired for solving the high inaccuracy problem. In this paper, we propose a novel framework for automated repair of high-inaccuracy bugs in numerical programs. The framework includes the phases of detecting high-inaccuracy bugs, localizing the buggy code, generating and validating the patches, and synthesizing the repaired program at last. Based on this framework, we develop a prototype tool for repairing high inaccuracies in numerical programs. Our preliminary experimental results are encouraging.

Recently, much attention has been paid on program repair by reusing existing code from other software. However, the technique of reusing code needs to search fix ingredients which refer to the existing code that can be reused to form a fix, and the searching space tends to be huge. Finding out those code fragments that contain proper fix ingredients efficiently will largely improve repair efficiency. Based on the assumption that similar code fragments may contain fix ingredients, this paper proposes reusability metrics of similar code fragments for program repair. By combining the similarity and differentiality at the level of program syntax trees, reusablility metrics is able to help picking out the most suitable reusable candidate. In order to apply reusability metrics to automated program repair, we have implemented SCRepair, which can utilize the guidance of reusability metrics to automatically fix bugs. Experimental results indicate that SCRepair can improve repair efficiency by making use of the reusability metrics of similar code.

Embedded software often involves intensive numerical computations and suffers from a number of runtime errors. The technique of numerical static analysis is of practical importance for checking the correctness of embedded software. However, most of the existing approaches of numerical static analysis consider sequential programs, while interrupts are a commonly used facility that introduces concurrency in embedded systems. Therefore, a numerical static analysis approach is highly desired for embedded software with interrupts. In this article, we propose a static analysis approach specifically for interrupt-driven programs based on sequentialization techniques. We present a method to sequentialize interrupt-driven programs into nondeterministic sequential programs according to the semantics of interrupts. The key benefit of using sequentialization is the ability to leverage the power of state-of-the-art analysis and verification techniques for sequential programs to analyze interrupt-driven programs, for example, the power of numerical abstract interpretation to analyze numerical properties of the sequentialized programs. Furthermore, to improve the analysis precision and scalability, we design specific abstract domains to analyze sequentialized interrupt-driven programs by considering their specific features. Finally, we present encouraging experimental results obtained by our prototype implementation.

Despite the availability of garbage collectors, programmers must manually manage non-memory finite system resources such as file descriptors. Resource leaks can gradually consume all available resources and cause programs to raise resource exhaustion exceptions. However, programmers commonly provide no effective recovery approach for resource exhaustion exceptions, which often causes programs to halt without completing their tasks. In this paper, we propose to automatically recover programs from resource exhaustion exceptions caused by resource leaks. We transform programs to catch resource exhaustion exceptions, collect leaked resources, and then retry the failure code. A resource collector is designed to identify leaked resources and safely release them. We implement our approach for Java programs. Experimental results show that our approach can successfully handle resource exhaustion exceptions caused by reported resource leaks and allow programs to complete their tasks with an average execution time increase of 2.52% and negligible bytecode size increase.

Heap-manipulating programs allow flexible manipulations over dynamically allocated, shared, and mutable heap cells via pointers that point to not only linked data structures but also their pointer fields. Therefore, memory leak detection for these programs requires precise field-sensitive pointer alias information, which make the problem more challenging. In this paper, we present a field and context sensitive algorithm for detecting memory leaks in heap-manipulating programs. First, we propose a modular heap abstraction based on member-access distances and alias bit-vector domain as the escape model of each procedure, Then, based on procedural summaries characterized by this modular heap abstraction, an efficient context-sensitive memory leak detection is proposed in an on-demand way. Experimental evaluation about a set of large C benchmark programs shows that the proposed approach is scalable with satisfied precision as expected.