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.

Large-scale Android apps that provide complex functions are gradually becoming the mainstream in Android app markets. They tend to display many GUI widgets on a single GUI page, which, unfortunately, can cause more redundant test actions—actions with similar functions—to automatic testing approaches. The effectiveness of existing testing approaches is still limited, suggesting the necessity of reducing the test effort on redundant actions. In this article, we first identify three types of GUI structures that can cause redundant actions and then propose a novel approach, called action equivalence evaluation, to find the actions with similar functions by exploiting both GUI structure and functionality. By integrating this approach with existing testing tools, the test efficacy can be improved. We conducted experiments on 17 large-scale Android apps, including three industrial apps Google News , Messenger , and WeChat . The results show that more instructions can be covered, and more crashes can be detected, compared to the state-of-the-art Android testing tools. Twenty-nine real bugs were found in our experiment, and moreover, 760 bugs over 40 versions of WeChat had been detected in the real test environment during a 3-month testing period.

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.

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.

State machines are essential for enhancing protocol analysis to identify vulnerabilities. However, inferring state machines from network protocol implementations is challenging due to complex code syntax and semantics. Traditional dynamic analysis methods often miss critical state transitions due to limited coverage, while static analysis faces path explosion issues. To overcome these challenges, we introduce a novel state machine inference approach utilizing Large Language Models (LLMs), named ProtocolGPT. This method employs retrieval augmented generation technology to enhance a pre-trained model with specific knowledge from protocol implementations. Through effective prompt engineering, we accurately identify and infer state machines. To the best of our knowledge, our approach represents the first state machine inference that leverages the source code of protocol implementations. Our evaluation of six protocol implementations shows that our method achieves a precision of over 90 %, outperforming the baselines by more than 30 %. Furthermore, integrating our approach with protocol fuzzing improves coverage by more than 20 % and uncovers two 0-day vulnerabilities compared to baseline methods.

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.

Graphical User Interface (GUI) testing is one of the primary approaches for testing mobile apps. Test scripts serve as the main carrier of GUI testing, yet they are prone to obsolescence when the GUIs change with the apps' evolution. Existing repair approaches based on GUI layouts or images prove effective when the GUI changes between the base and updated versions are minor, however, they may struggle with substantial changes. In this paper, a novel approach named COSER is introduced as a solution to repairing broken scripts, which is capable of addressing larger GUI changes compared to existing methods. COSER incorporates both external semantic information from the GUI elements and internal semantic information from the source code to provide a unique and comprehensive solution. The efficacy of COSER was demonstrated through experiments conducted on 20 Android apps, resulting in superior performance when compared to the state-of-the-art tools METER and GUIDER. In addition, a tool that implements the COSER approach is available for practical use and future research.

Deep Neural Network (DNN) testing is one of the common practices to guarantee the quality of DNNs. However, DNN testing in general requires a significant amount of test inputs with oracle information (labels), which can be challenging and resource-intensive to obtain. To relieve this problem, we propose DATIS, a distance-aware test input selection approach for DNNs. Specifically, DATIS adopts a two-step approach for selecting test inputs. In the first step, it selects test inputs based on improved uncertainty scores derived from the distances between the test inputs and their nearest neighbor training samples. In the second step, it further eliminates test inputs that may cover the same faults by examining the distances among the selected test inputs. To evaluate DATIS, we conduct extensive experiments on 8 diverse subjects, taking into account different domains of test inputs, varied DNN structures, and diverse types of test inputs. Evaluation results show that DATIS significantly outperforms 15 baseline approaches in both selecting test inputs with high fault-revealing power and guiding the selection of data for DNN enhancement.

Web services have brought great convenience to our daily lives. Meanwhile, they are vulnerable to Denial-of-Service (DoS) attacks. DoS attacks launched via vulnerabilities in the services can cause great harm. The vulnerabilities in protocol implementations are especially important because they are the keystones of web services. One vulnerable protocol implementation can affect all the web services built on top of it. Compared to the vulnerabilities that cause the target service to crash, resource exhaustion vulnerabilities are equally if not more important. This is because such vulnerabilities can deplete the system resources, leading to the unavailability of not only the vulnerable service but also other services running on the same machine. Despite the significance of this type of vulnerability, there has been limited research in this area.

Call graphs facilitate various tasks in software engineering. However, for the dynamic language Python, the complex language features and external library dependencies pose enormous challenges for building the call graphs of real projects. Some program analysis techniques used for call graph construction in other languages are impractical for Python. In this paper, we present STAR, a practical technique for the construction of Python static call graphs. We reformulate call graph construction as an entity identification task. STAR leverages inter-module summary and cross-project dependencies to construct a fine-grained entity knowledge base to identify the possible nodes and edges of the call graph in the code, and then construct the call graph. Our evaluation of three benchmarks shows that (1) STAR improves recall in three benchmarks compared to three baseline tools. Especially, STAR improves the recall of reachable nodes and reachable edges compared with the state-of-the-art tool by 11.3% and 9.8%, respectively; (2) STAR achieves comparable performance as three baseline tools in execution time and memory usage and is more efficient in large projects; (3) STAR can be effectively used for the task of detecting vulnerability propagation with real-world cases. We expect our results will attract more exploration of practical methods and improve the application of Python call graphs.

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.

Datalog is a popular and widely-used declarative logic programming language. Datalog engines apply many cross-rule optimizations; bugs in them can cause incorrect results. To detect such optimization bugs, we propose an automated testing approach called Incremental Rule Evaluation (IRE), which synergistically tackles the test oracle and test case generation problem. The core idea behind the test oracle is to compare the results of an optimized program and a program without cross-rule optimization; any difference indicates a bug in the Datalog engine. Our core insight is that, for an optimized, incrementally-generated Datalog program, we can evaluate all rules individually by constructing a reference program to disable the optimizations that are performed among multiple rules. Incrementally generating test cases not only allows us to apply the test oracle for every new rule generated—we also can ensure that every newly added rule generates a non-empty result with a given probability and eschew recomputing already-known facts. We implemented IRE as a tool named Deopt, and evaluated Deopt on four mature Datalog engines, namely Soufflé, CozoDB, μZ, and DDlog, and discovered a total of 30 bugs. Of these, 13 were logic bugs, while the remaining were crash and error bugs. Deopt can detect all bugs found by queryFuzz, a state-of-the-art approach. Out of the bugs identified by Deopt, queryFuzz might be unable to detect 5. Our incremental test case generation approach is efficient; for example, for test cases containing 60 rules, our incremental approach can produce 1.17× (for DDlog) to 31.02× (for Soufflé) as many valid test cases with non-empty results as the naive random method. We believe that the simplicity and the generality of the approach will lead to its wide adoption in practice.

Function entry identification is a crucial yet challenging task for binary disassemblers that has been the focus of research in the past decades. However, recent researches show that call frame information (CFI) provides accurate and almost complete function entries. With the aid of CFI, disassemblers have significant improvements in function entry detection. CFI is specifically designed for efficient stack unwinding, and every function has corresponding CFI in x64 and aarch64 architectures. Nevertheless, not every function and instruction unwinds the stack at runtime, and this observation has led to the development of techniques such as obfuscation to complicate function detection by disassemblers.

With the rapid expansion of the Internet of Things, a vast number of microcontroller-based (MCU) IoT devices are now susceptible to attacks through the Internet. Vulnerabilities within the firmware are one of the most important attack surfaces. Fuzzing has emerged as one of the most effective techniques for identifying such vulnerabilities. However, when applied to IoT firmware, several challenges arise, including: 1) the inability of firmware to execute properly in the absence of peripherals; 2) the lack of support for exploring input spaces of multiple peripherals; 3) difficulties in instrumenting and gathering feedback; and 4) the absence of a fault detection mechanism. To address these challenges, we have developed and implemented an innovative peripheral-independent hybrid fuzzing tool called FirmHybirdFuzzer. This tool enables testing of MCU firmware without reliance on specific peripheral hardware. First, a unified virtual peripheral was integrated to model the behaviors of various peripherals, thus enabling the physical devices-agnostic firmware execution. Then, a hybrid event generation approach was used to generate inputs for different peripheral accesses. Furthermore, two-level coverage feedback was collected to optimize the testcase generation. Finally, a plugin-based fault detection mechanism was implemented to identify typical memory corruption vulnerabilities. A large-scale experimental evaluation has been performed to show FirmHybirdFuzzer’s effectiveness and efficiency.

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.

Managing cross-project dependencies is tricky in modern software development. A primary way to manage dependencies is using dependency configuration files, which brings convenience to the entire software ecosystem, including developers, maintainers, and users. However, developers may introduce dependency smells if dependency configuration files are not well written and maintained. Dependency smells are recurring violations of dependency management in dependency configuration files and can potentially lead to severe consequences. This paper provides an in-depth look at three dependency smells, namely,Missing Dependency,Bloated Dependency, andVersion Constraint Inconsistencyin Python projects. First, we implement a tool calledPythonCross-projectDependency- PyCD to accurately extract dependency information from configuration files. The evaluation result on 212 Python projects shows that PyCD outperforms state-of-the-art tools. Then, we make an empirical study for three dependency smells in 132 Python projects to investigate the pervasiveness, causes, and evolution. The results show that: 1) dependency smells are prevalent in Python projects and exist inconsistently in different projects; 2) dependency smells are introduced into Python projects for different reasons, mainly due to the problems of synchronous update and collaborative development; and 3) dependency smells can be removed with different patterns according to different dependency smells. Furthermore, we report and get responses for 40 harmful dependency smell instances, 34 of which have been responded that these dependency smells do exist in the projects, and 10 instances are fixed or under process. The feedback from developers indicates that dependency smells can have a negative impact on project maintenance. Our study highlights that these dependency smells deserve the attention of developers.

This paper proposes a joint acoustic echo cancellation (AEC) and speech enhancement method with adaptive filter and deep neural network (DNN) model. A partitioned block adaptive filter is adopted for linear AEC followed by a convolutional neural network and transformer based model to suppress the residual echo, noise, and reverberation. The DNN model has three modules: encoder, dual-path transformer (DPT) and decoder. The encoder is adopted to explore the potential relationships of far-end and near-end signals with the attention mechanism of transformer. The DPT module is further used to explore context information in both time and frequency dimension. The attention mask is used in transformer to realize real-time process. The complex spectra mask is finally estimated by the decoder to recover the target speech. Our proposed DNN model is trained on the ICASSP 2022 AEC Challenge datasets and placed fourth in the challenge with satisfactory performance on subjective and word acceptance rate evaluation.

With the growth of Issue Tracking Systems, issue reports have become an important data to aid software maintenance and evaluation. Issue classification is one of the most important methods for such purpose, which aims to automatically distinguish issues related to bugs from other issues via machine learning algorithm. However, existing issue classification approaches are still inadequate due to either the incorrect usages of the textual fields of the issues or the ineffective feature representation methods. In this paper, we propose a novel issue classification approach named DeepLabel for achieving advanced issue classification. DeepLabel predicts the issue types by the ensemble of field-specific models that are applied on different textual fields, so as to make the maximum use of the information contained in the textual fields. In addition, DeepLabel adopts Word2Vec combined with attention-based Bi-directional Long Short-Term Memory (ABLSTM) as the feature extractor for the field-specific models in order to effectively extract the semantic information from the textual fields. We conduct an empirical study to evaluate the effectiveness of DeepLabel based on a widely used issue dataset. The results demonstrate that DeepLabel can significantly outperform the state-of-the-art approaches, in which DeepLabel correctly identifies more bug issues (160.1 vs. 140.1) and more non-bug issues (345.7 vs. 325.4) on average compared to the best one existing approach.

Spectrum-based fault localization(SBFL) has become one of the most widely studied localization techniques by its effectiveness and lightweightness. However, existing simple SBFL techniques are still not accurate enough for they are not able to distinguish specific locations in the same basic block. To address this problem, techniques that combine SBFL and MBFL(Mutation-based fault localization) have been proposed with the cost of introducing huge overhead from mutants. This paper proposes a graph neural network (GNN) based two-phase localization approach that localizes statements in blocks accurately and efficiently. The graph neural network introduced from our approach extracts the information from both the control flow graph and data flow graph, which includes the dependencies that distinguish the specific locations and further increase the localization accuracy. Our localization process is divided into two phases: Phase-I computes the suspiciousness score of each method and generates a ranking list, and phase-II further highlights the potential faulty locations inside a method by a fine-grained GNN with graphs in the method. We conduct experiments on 357 real bugs of 5 projects in the Defects4j benchmark. The results show that with a small overhead in our approach, the number of our successfully localized faults within the top-1, top-3, and top-5 positions is obviously higher than other SBFL techniques.

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.

With the rapid development of Deep Learning, deep predictive models have been widely applied to improve Software Engineering tasks, such as defect prediction and issue classification, and have achieved remarkable success. They are mostly trained in a supervised manner, which heavily relies on high-quality datasets. Unfortunately, due to the nature and source of software engineering data, the real-world datasets often suffer from the issues of sample mislabelling and class imbalance, thus undermining the effectiveness of deep predictive models in practice. This problem has become a major obstacle for deep learning-based Software Engineering.

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.

Hardware tracing modules such as Intel Processor Trace perform continuous control-flow tracing of an end-to-end program execution with an ultra-low overhead. PT has been used in a variety of contexts to support applications such as testing, debugging, and performance diagnosis. However, these hardware modules have so far been used only to trace native programs, which are directly compiled down to machine code. As high-level languages (HLL) such as Java and Go become increasingly popular, there is a pressing need to extend these benefits to the HLL community. This paper presents JPortal, a JVM-based profiling tool that bridges the gap between HLL applications and low-level hardware traces by using a set of algorithms to precisely recover an HLL program’s control flow from PT traces. An evaluation of JPortal with the DaCapo benchmark shows that JPortal achieves an overall 80% accuracy for end-to-end control flow profiling with only a 4-16% runtime overhead.

Sophisticated static analysis techniques often have complicated implementations, much of which provides logic for tuning and scaling rather than basic analysis functionalities. This tight coupling of basic algorithms with special treatments for scalability makes an analysis implementation hard to (1) make correct, (2) understand/work with, and (3) reuse for other clients. This paper presents Chianina, a graph system we developed for fully context- and flow-sensitive analysis of large C programs. Chianina overcomes these challenges by allowing the developer to provide only the basic algorithm of an analysis and pushing the tuning/scaling work to the underlying system. Key to the success of Chianina is (1) an evolving graph formulation of flow sensitivity and (2) the leverage of out-of-core, disk support to deal with memory blowup resulting from context sensitivity. We implemented three context- and flow-sensitive analyses on top of Chianina and scaled them to large C programs like Linux (17M LoC) on a single commodity PC.

Static program analysis has been widely applied along the whole process of the program development for bug detection, code optimization, testing, etc. Although researchers have made significant work in static program analysis, it is still challenging to perform sophisticated interprocedural analysis on large-scale modern software. The underlying reason is that interprocedural analysis for large-scale modern software is highly computation- and memory-intensive, leading to poor efficiency and scalability. In this article, we introduce an efficient distributed and scalable solution for sophisticated static analysis. Specifically, we propose a data-parallel algorithm and a join-process-filter computation model for the CFL-reachability-based interprocedural analysis. Based on that, an efficient distributed static analysis engine called BigSpa is developed, which is composed of an offline batch static program analysis system and an online incremental static program analysis system. The BigSpa system has high generality and can support all kinds of static analysis tasks that can be expressed as CFL reachability problems. The performance of BigSpa is evaluated on real-world large-scale software datasets. Our experiments show that the offline batch system can exceed an order of magnitude compared with the most advanced analysis tools available on performance, and for incremental analysis with small batch updates on the same data sets, the online analysis system can achieve near real-time response, which is very fast and flexible.

Ordinary users can build their smart home automation system easily nowadays, but such user-customized systems could be error-prone. Using formal verification to prove the correctness of such systems is necessary. However, to conduct formal proof, formal specifications such as Linear Temporal Logic (LTL) formulas have to be provided, but ordinary users cannot author LTL formulas but only natural language.To address this problem, this paper presents a novel approach that can automatically generate formal LTL specifications from natural language requirements based on domain knowledge and our proposed ambiguity refining techniques. Experimental results show that our approach can achieve a high correctness rate of 95.4% in converting natural language sentences into LTL formulas from 481 requirements of real examples.

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.

There is more than a decade-long history of using static analysis to find bugs in systems such as Linux. Most of the existing static analyses developed for these systems are simple checkers that find bugs based on pattern matching. Despite the presence of many sophisticated interprocedural analyses, few of them have been employed to improve checkers for systems code due to their complex implementations and poor scalability. In this article, we revisit the scalability problem of interprocedural static analysis from a “Big Data” perspective. That is, we turn sophisticated code analysis into Big Data analytics and leverage novel data processing techniques to solve this traditional programming language problem. We propose Graspan , a disk-based parallel graph system that uses an edge-pair centric computation model to compute dynamic transitive closures on very large program graphs. We develop two backends for Graspan, namely, Graspan-C running on CPUs and Graspan-G on GPUs, and present their designs in the article. Graspan-C can analyze large-scale systems code on any commodity PC, while, if GPUs are available, Graspan-G can be readily used to achieve orders of magnitude speedup by harnessing a GPU’s massive parallelism. We have implemented fully context-sensitive pointer/alias and dataflow analyses on Graspan. An evaluation of these analyses on large codebases written in multiple languages such as Linux and Apache Hadoop demonstrates that their Graspan implementations are language-independent, scale to millions of lines of code, and are much simpler than their original implementations. Moreover, we show that these analyses can be used to uncover many real-world bugs in large-scale systems code.

Many real-world bugs in large-scale systems are related to object state that is supposed to obey a specified finite state machine (FSM). They are triggered when unexpected events occur on objects in certain states, making these objects transition in a way that violates their specifications. Detecting such FSM-related bugs with static analysis is challenging, especially in distributed systems that have large codebases.

Numerical code is often applied in the safety-critical, but resource-limited areas. Hence, it is crucial for it to be correct and efficient, both of which are difficult to ensure. On one hand, accumulated rounding errors in numerical programs can cause system failures. On the other hand, arbitrary/infinite-precision arithmetic, although accurate, is infeasible in practice and especially in resource-limited scenarios because it performs thousands of times slower than floating-point arithmetic. Thus, it has been a significant challenge to obtain high-precision, easy-to-maintain, and efficient numerical code. This paper introduces a novel global optimization framework to tackle this challenge. Using our framework, a developer simply writes the infinite-precision numerical program directly following the problem's mathematical requirement specification. The resulting code is correct and easy-to-maintain, but inefficient. Our framework then optimizes the program in a global fashion (i.e., considering the whole program, rather than individual expressions or statements as in prior work), the key technical difficulty this work solves. To this end, it analyzes the program's numerical value flows across different statements through a symbolic trace extraction algorithm, and generates optimized traces via stochastic algebraic transformations guided by effective rule selection. We first evaluate our technique on numerical benchmarks from the literature; results show that our global optimization achieves significantly higher worst-case accuracy than the state-of-the-art numerical optimization tool. Second, we show that our framework is also effective on benchmarks having complicated program structures, which are challenging for numerical optimization. Finally, we apply our framework on real-world code to successfully detect numerical bugs that have been confirmed by developers.

Static program analysis is widely used in various application areas to solve many practical problems. Although researchers have made significant achievements in static analysis, it is still too challenging to perform sophisticated interprocedural analysis on large-scale modern software. The underlying reason is that interprocedural analysis for large-scale modern software is highly computation- and memory-intensive, leading to poor scalability. We aim to tackle the scalability problem by proposing a novel big data solution for sophisticated static analysis. Specifically, we propose a data-parallel algorithm and a join-process-filter computation model for the CFL-reachability based interprocedural analysis and develop an efficient distributed static analysis engine in the cloud, called BigSpa. Our experiments validated that BigSpa running on a cluster scales greatly to perform precise interprocedural analyses on millions of lines of code, and runs an order of magnitude or more faster than the existing state-of-the-art analysis tools.

It is challenging to have a general solution to precisely detect arbitrary vulnerabilities. Thus security research has focused on detecting specific types of vulnerabilities. Missing checks for untrusted inputs used in security-sensitive operations are one of the major causes of various serious vulnerabilities. Efficiently detecting missing checks is essential for identifying insufficient attack protections and prognosing potential vulnerabilities. This paper proposes a systematic static approach to detect missing checks for manipulable data used in security-sensitive operations in C/C++ programs. We first locate customized security-sensitive operations with lightweight static analysis; then judge assailability of sensitive data used in security-sensitive operations via static taint analysis; finally, assess the existence and risk degree of missing checks using static analysis. We have implemented the approach into an automated and cross-platform tool, named Vanguard, on top of Clang/LLVM 3.6.0. Experimental results on open-source projects have shown its effectiveness and efficiency. Furthermore, Vanguard has led us to uncover five known vulnerabilities and two unknown bugs.

In regression GUI testing for Android apps, test scripts often fail due to changes to, rather than faults in, those apps. To avoid such false positives while still retaining the value of the old test scripts as much as possible, programmers need an automatic way to maintain the tests after the corresponding GUI has evolved. In this paper, we propose the CHATEM approach to automate GUI test script maintenance for Android apps. Taking as input the models for the GUIs of the base and updated version app and the original test scripts, CHATEM automatically extracts the changes between the two GUIs and generates maintenance actions for each change, which are then combined to form the maintenance actions for affected test scripts. In an experimental evaluation on 16 Android apps, CHATEM was able to automatically maintain the test scripts so that overall more than 95% of the remaining behaviors tested before are still tested, and almost 80% of the reusable test actions are retained in the result tests.

The importance of regression testing in assuring the integrity of a program after changes is well recognized. One major obstacle in practicing regression testing is in maintaining tests that become obsolete due to evolved program behavior or specification. For mobile apps, the problem of maintaining obsolete GUI test scripts for regression testing is even more pressing. Mobile apps rely heavily on the correct functioning of their GUIs to compete on the market and provide good user experiences. But on the one hand, GUI tests break easily when changes happen to the GUI, On the other hand, mobile app developers often need to fight for a tight feedback loop and are left with limited time for test maintenance. In this paper, we propose a novel approach, called ATOM, to automatically maintain GUI test scripts of mobile apps for regression testing. ATOM uses an event sequence model to abstract possible event sequences on a GUI and a delta ESM to abstract the changes made to the GUI. Given both models as input, ATOM automatically updates the test scripts written for a base version app to reflect the changes. In an experiment with 22 versions from 11 production Android apps, ATOM updated all the test scripts affected by the version change, the updated scripts achieve over 80% of the coverage by the original scripts on the base version app, all except one set of updated scripts preserve over 60% of the actions in the original test scripts.

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.

Buffer overflow is one of the most common types of software security vulnerabilities. Although researchers have proposed various static and dynamic techniques for buffer overflow detection, buffer overflow attacks against both legacy and newly-deployed software systems are still quite prevalent. Compared with dynamic detection techniques, static techniques are more systematic and scalable. However, there are few studies on the effectiveness of state-of-the-art static buffer overflow detection techniques. In this paper, we perform an in-depth quantitative and qualitative study on static buffer overflow detection. More specifically, we obtain both the buggy and fixed versions of 100 buffer overflow bugs from 63 real-world projects totalling 28 MLoC (Millions of Lines of Code) based on the reports in Common Vulnerabilities and Exposures (CVE). Then, quantitatively, we apply Fortify, Checkmarx, and Splint to all the buggy versions to investigate their false negatives, and also apply them to all the fixed versions to investigate their false positives. We also qualitatively investigate the causes for the false-negatives and false-positives of studied techniques to guide the design and implementation of more advanced buffer overflow detection techniques. Finally, we also categorized the patterns of manual buffer overflow repair actions to guide automated repair techniques for buffer overflow. The experiment data is available at http://bo-study.github.io/Buffer-Overflow-Cases/.

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.

Buffer overflow is one of the most common types of software vulnerabilities. Various static analysis and dynamic testing techniques have been proposed to detect buffer overflow vulnerabilities. With automatic tool support, static buffer overflow detection technique has been widely used in academia and industry. However, it tends to report too many false positives fundamentally due to the lack of software execution information. Currently, static warnings can only be validated by manual inspection, which significantly limits the practicality of the static analysis. In this paper, we present BovInspector, a tool framework for automatic static buffer overflow warnings inspection and validated bugs repair. Given the program source code and static buffer overflow vulnerability warnings, BovInspector first performs warning reachability analysis. Then, BovInspector executes the source code symbolically under the guidance of reachable warnings. Each reachable warning is validated and classified by checking whether all the path conditions and the buffer overflow constraints can be satisfied simultaneously. For each validated true warning, BovInspector fix it with three predefined strategies. BovInspector is complementary to prior static buffer overflow discovery schemes. Experimental results on real open source programs show that BovInspector can automatically inspect on average of 74.9% of total warnings, and false warnings account for about 25% to 100% (on average of 59.9%) of the total inspected warnings. In addition, the automatically generated patches fix all target vulnerabilities. Further information regarding the implementation and experimental results of BovInspector is available at http://bovinspectortool.github.io/project/. And a short video for demonstrating the capabilities of BovInspector is now available at https://youtu.be/IMdcksROJDg.

STT-MRAM (Spin-Transfer Torque Magnetic RAM) has recently emerged as one of the most promising memory technologies for constructing large capacity last level cache (LLC) of low power mobile processors. With fast technology scaling, STT-MRAM read operations will become destructive such that post-read restores are inevitable to ensure data reliability. However, frequent restores introduce large energy overheads. In this paper, we propose Selective Restore (SR), an energy efficient scheme to mitigate the restore overheads. Given a L2 cacheline disturbed from a read operation, SR postpones its restore till the cacheline being evicted from the upper level cache L1. Based on the status of the line at the eviction time, SR selectively restores the disturbed cells to achieve energy efficiency. Our experimental results show that SR improves system performance by 5% and reduces dynamic energy consumption by 62%.

Recent studies have shown that Phase Change Memory faces significant write disturbance (WD) when scaling in deep submicron regime, i.e., resetting a cell may disturb the values of its adjacent cells if these cells are in amorphous state. A preventive approach to mitigate WD errors is to allocate sufficient inter-cell thermal band. However, this approach greatly reduces chip capacity due to low cell density. A cost effective approach VnC (verify-and-correct), relies on Verification after each write and Correction if errors do happen. Simple VnC improves chip capacity but introduces large performance degradation.

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.

Software test adequacy criteria are used to determine whether the test on a software system is sufficient. Code coverage shows how thoroughly a program is tested according to corresponding testing adequacy criteria. There are many coverage criteria used in practice to measure the test adequacy at different granularity of the target program. Length-n subpath criterion is a systematic flexible coverage criterion at a fine granularity. In this paper, we present a prototype test coverage tool named nCov for measuring length-n subpath coverage based on control flow graph. For a C program and corresponding test suite, our tool can measure the length-n subpath coverage for various n, say 1 to 8. It can also be used to select test cases for satisfying length-n subpath coverage with specific n. In addition, to improve the scalability of the tool, we propose a loop compression algorithm to record the program trace. We have conducted a controlled experiment to demonstrate the feasibility and efficiency of our tool.

NAND flash has been widely adopted as storage devices in real-time embedded systems. However, garbage collection is needed to reclaim space and introduces a lot of time overhead. As the worst system latency is determined by the worst-case execution time of garbage collection in NAND flash, it is important to optimize garbage collection so as to give a deterministic worst system latency. On the other hand, since the garbage collection does not happen very often, optimizing garbage collection should not bring too much overhead to the average system latency. This paper presents for the first time a worst-case and average-case joint optimization scheme for garbage collection in NAND flash. With our scheme, garbage collection can be postponed to the latest stage so improves the average system latency. By combining partial garbage collection and over-provisioning, our scheme can guarantee that one free block is enough to hold all pages from both write requests and valid-page copies. The experiments have been conducted on a real embedded platform and the results show that our technique can improve both worstcase and average-case system latency compared with the previous works.

Due to many attractive and unique properties, NAND flash memory has been widely adopted in mission-critical hard real-time systems and some soft real-time systems. However, the nondeterministic garbage collection operation in NAND flash memory makes it difficult to predict the system response time of each data request. This article presents Lazy-RTGC , a real-time lazy garbage collection mechanism for NAND flash memory storage systems. Lazy-RTGC adopts two design optimization techniques: on-demand page-level address mappings, and partial garbage collection. On-demand page-level address mappings can achieve high performance of address translation and can effectively manage the flash space with the minimum RAM cost. On the other hand, partial garbage collection can provide the guaranteed system response time. By adopting these techniques, Lazy-RTGC jointly optimizes both the average and the worst system response time, and provides a lower bound of reclaimed free space. Lazy-RTGC is implemented in FlashSim and compared with representative real-time NAND flash memory management schemes. Experimental results show that our technique can significantly improve both the average and worst system performance with very low extra flash-space requirements.

The world's increased dependence on software-enabled systems has raised major concerns about software reliability and security. New cost-effective tools for software quality assurance are needed. This paper presents an automated test generation technique, called Model-based Integration and System Test Automation (MISTA), for integrated functional and security testing of software systems. Given a Model-Implementation Description (MID) specification, MISTA generates test code that can be executed immediately with the implementation under test. The MID specification uses a high-level Petri net to capture both control- and data-related requirements for functional testing, access control testing, or penetration testing with threat models. After generating test cases from the test model according to a given criterion, MISTA converts the test cases into executable test code by mapping model-level elements into implementation-level constructs. MISTA has implemented test generators for various test coverage criteria of test models, code generators for various programming and scripting languages, and test execution environments such as Java, C, C++, C#, HTML-Selenium IDE, and Robot Framework. MISTA has been applied to the functional and security testing of various real-world software systems. Our experiments have demonstrated that MISTA can be highly effective in fault detection.

Address mapping is one of the major functions in managing NAND flash. With the capacity increase of NAND flash, it becomes vitally important to reduce the RAM print of the address mapping table while not introducing big performance overhead. Demand-based address mapping is an effective approach to solve this problem, in which the address mapping table is stored in NAND flash (called translation pages), and mapping items are cached on-demand in RAM. Therefore, it is critical to manage translation pages in demand-based address mapping. This paper solves two most important problems in translation page management. First, to reduce frequent translation page updates caused by data requests, we propose a page-level caching mechanism to exploit the fundamental property of NAND flash where the basic read/write unit is one page. Second, to reduce the garbage collection overhead from translation pages, we propose a multiple write pointers strategy to group data pages corresponding to the same translation page into one data block, by which, when the data block is reclaimed via the garbage collection, we only need to update one translation page. We evaluate our scheme using a set of benchmarks from both real-world and synthetic traces. Experimental results show that our techniques can achieve significant reduction in the extra translation operations and improve the system response time.

It is encouraged to develop practical approaches to ensure that the software artifacts are created as expected or defect-free as early as possible. In the industry, software analysis and testing techniques are widely used solutions for codes and executables, respectively. However, software design artifacts can only be verified by manual peer review in design phase. In this paper, we propose an approach to automatically simulate the expected software behavior depicted in UML activity diagrams. First, UML activity diagrams are parsed and initialized semantically with a concrete execution. Second, the model is symbolically executed, to collect paths, input variables, and their path conditions. Then, the path conditions are passed to a constraint solver to generate a set of concrete value of possible input variables. Final, the generated concrete input variables are semantically executed on the model to identify the defects as well as to collect the execution path. The model simulation approach reuses the design models, automates the simulation process by using model-based concolic execution, and has the advantage of visibility and observability on model simulation. In addition, we found that the solvable paths represent behavioral scenarios. While simulating the model, input values corresponding to execution paths in the model are generated automatically. They can also be used as test suites to find the inconsistency between the design and implementation. We have also developed a prototype tool to support the above process, and have conducted a trivial case study to demonstrate the applicability of our approach.

File Edit Options Buffers Tools TeX Help Memory leaks have significant impact on software availability, performance, and security. Static analysis has been widely used to find memory leaks in C/C++ programs. Although a static analysis is able to find all potential leaks in a program, it often reports a great number of false warnings. Manually validating these warnings is a daunting task, which significantly limits the practicality of the analysis. In this paper, we develop a novel dynamic technique that automatically validates and categorizes such warnings to unleash the power of static memory leak detectors. Our technique analyzes each warning that contains information regarding the leaking allocation site and the leaking path, generates test cases to cover the leaking path, and tracks objects created by the leaking allocation site. Eventually, warnings are classified into four categories: MUST-LEAK, LIKELY-NOT-LEAK, BLOAT, and MAY-LEAK. Warnings in MUST-LEAK are guaranteed by our analysis to be true leaks. Warnings in LIKELY-NOT-LEAK are highly likely to be false warnings. Although we cannot provide any formal guarantee that they are not leaks, we have high confidence that this is the case. Warnings in BLOAT are also not likely to be leaks but they should be fixed to improve performance. Using our approach, the developer's manual validation effort needs to be focused only on warnings in the category MAY-LEAK, which is often much smaller than the original set.

Symbolic execution is a promising testing and analysis methodology. It systematically explores a program's execution space and can generate test cases with high coverage. One significant practical challenge for symbolic execution is how to effectively explore the enormous number of program paths in real-world programs. Various heuristics have been proposed for guiding symbolic execution, but they are generally inefficient and ad-hoc. In this paper, we introduce a novel, unified strategy to guide symbolic execution to less explored parts of a program. Our key idea is to exploit a specific type of path spectra, namely the length-n subpath program spectra, to systematically approximate full path information for guiding path exploration. In particular, we use frequency distributions of explored length-n subpaths to prioritize "less traveled" parts of the program to improve test coverage and error detection. We have implemented our general strategy in KLEE, a state-of-the-art symbolic execution engine. Evaluation results on the GNU Coreutils programs show that (1) varying the length n captures program-specific information and exhibits different degrees of effectiveness, and (2) our general approach outperforms traditional strategies in both coverage and error detection.

Dealing with crosscutting concerns has been a critical problem in software development processes. To facilitate handling crosscutting concerns at design phases, we proposed an aspect-oriented modeling and integration approach with UML activity diagrams. The primary concerns are depicted with UML activity diagrams as primary models, whereas crosscutting concerns are described with aspectual extended activity diagrams as aspect models. Aspect models can be integrated into primary models automatically. The AOM approach can reduce the complexity of design models. However, potential faults that violate desired properties of the software system might still be introduced during the modeling or integration processes. The verification technique is well-known for its ability to assure the correctness of models and uncover design problems before implementation. We propose a framework to verify aspect-oriented UML activity diagrams based on Petri net verification techniques. For verification purpose, we transform the integrated activity diagrams into Petri nets and prove the consistency of the transformation. Then, crosscutting concerns in system requirements are refined to properties in the form of CTL formulas. Finally, the Petri nets are verified against the formalized properties to report whether the aspect-oriented design models satisfies the requirements. Furthermore, we implement a tool named Jasmine-AOV to support the verification process. Case studies are conducted to evaluate the effectiveness of the proposed approach.

Correct real-time behavior is an important aspect for time sensitive software, but it is difficult to get right. Time faults can be introduced not just during software development but also maintenance. So software maintainers without time information tend to have more chances to introduce unintended time behaviors. In this paper, we propose time change impact analysis to help maintainers estimate the potential influence of time changes on programs before the software evolves. Our main insight is that by being reminded and warned that a small-time change at some places in the source code will largely affect the whole task execution time, maintainers can be more cautious when updating such places. Because these places have a leverage effect that multiplies the task execution time in a subtle way, we call them time-leverage points. We give an approach to detect the time-leverage points based on a dynamic testing method, which instruments the program at a point for introducing a small delay and observes its impact on the task execution time. We implement a prototype tool and empirically evaluate the approach.

It is well-known that as software system evolves, the source code tends to deviate from its design model so that maintaining their consistence is challenging. Our objective is to detect code changes that influence designed program behaviour which are referred as design level changes and update the behavioural model timely and automatically to maintain consistence. We propose an approach that filters out low-level source code changes that do not influence program behaviour, abstracts code changes into updating operations for behavioral model, and automates the integration and update of activity diagrams to maintain consistence. We've recognised that it is not uncommon for developers to introduce quick and dirty implementation that unnecessarily increases program complexity or introduces suboptimal behaviour changes. So while merging code changes into behaviour model, our approach also calculates cyclometric complexity variation before and after the process so that developers can be alerted of significant and/or detrimental changes. Our tool allows the user to approve the change in code before merging and updating the model.

Scenario-based specifications (SBSs), such as UML interaction models, offer an intuitive and visual way of describing design requirements, and are playing an increasingly important role in the design of software systems. This paper presents an approach to timing analysis of SBSs expressed by UML interaction models. The approach considers more general and expressive timing constraints in UML sequence diagrams (SDs), and gives a solution to the reachability analysis, constraint conformance analysis and bounded delay analysis problems, which reduces these problems into linear programs. With the synchronous interpretation of the SD compositions, the timing analysis algorithms in the approach form a decision procedure for a class of SBSs where any loop in any path is time-independent of the other parts in the path. These algorithms are also a semi-decision procedure for general SBSs with both the synchronous and asynchronous composition semantics. The approach also supports bounded timing analysis of SBSs, which investigates all the paths in the bound limit one by one, and performs the timing analysis for each finite path by linear programming. A tool prototype has been developed to support this approach. Copyright © 2010 John Wiley & Sons, Ltd. (This paper presents a linear programming-based approach to timing analysis of scenario-based specifications (SBSs) expressed by UML interaction models. With more general and expressive timing constraints in UML sequence diagrams, the algorithms in the approach solve the problems of the reachability, constraint conformance and bounded delay analysis of SBSs. These algorithms form a decision procedure for the loop-unlimited SBSs where any loop in any path is time-independent of the other parts in the path, and a semi-decision procedure for general SBSs.)

SUMMARY Aspect‐oriented programming yields new types of programming faults due to the introduction of new constructs for dealing with crosscutting concerns. To reveal aspect faults, this paper presents a framework for testing whether or not aspect‐oriented programs conform to their state models. It supports two families of strategies (i.e. structure‐oriented and property‐oriented) for automated generation of aspect tests from aspect‐oriented state models. A structure‐oriented testing strategy derives tests and test code from an aspect‐oriented state model to meet a given structural coverage criterion, such as state coverage, transition coverage, or round trip. A property‐oriented testing strategy generates test code from the counterexamples of model checking. Two such strategies are checking an aspect‐oriented state model against trap properties and checking mutants of aspect models against system properties. Mutation analysis of aspect‐oriented programs is used to evaluate the effectiveness of these testing strategies. The experiments demonstrate that testing aspect‐oriented programs against their state models can detect many aspect faults. The comparative evaluations also reveal that the structure‐oriented and property‐oriented testing strategies complement each other—some aspect faults were detected by the structure‐oriented strategies, but not by the property‐oriented strategies and vice versa. Copyright © 2010 John Wiley & Sons, Ltd.

Existing reachability analysis techniques are easy to fail when applied to large compositional linear hybrid systems, since their memory usages rise up quickly with the increase of systems' size. To address this problem, we propose a tool BACH 2 that adopts a path-oriented method for bounded reachability analysis of compositional linear hybrid systems. For each component, a path is selected and all selected paths compose a path set for reachability analysis. Each path is independently encoded to a set of constraints while synchronization controls are encoded as a set of constraints too. By merging all the constraints into one set, the path-oriented reachability problem of a path set can be transformed to the feasibility problem of this resulting linear constraint set, which can be solved by linear programming efficiently. Based on this path-oriented method, BACH 2 adopts a shared label sequence guided depth first search (SLS-DFS) method to perform bounded reachability analysis of compositional linear hybrid system, where all potential path sets within the bound limit are identified and verified one by one. By this means, since only the structure of a system and the recently visited one path in each component need to be stored in memory, memory consumption of BACH 2 is very small at runtime. As a result, BACH 2 enables the verification of extremely large systems, as is demonstrated in our experiments.

Monitoring and fault tolerance are important approaches to give high confidence that long-running online software systems run correctly. But these approaches will certainly cause high overhead cost, i.e. the loss of efficiency. Multi-core platforms can make such cost acceptable because of the advantage of the parallel performance. For allowing ordinary software developers without any knowledge of multi-core platforms to handle such programming tasks more efficiently, we propose an approach to enable multi-core based monitoring and fault tolerance in C++/Java.

Since Wireless Sensor Networks (WSNs) are increasingly used in many industrial and civilian application areas, the correctness of their low level protocol such as the Flooding Time Synchronization Protocol (FTSP) is critical. However ensuring such correctness is difficult because of the complexity of the runtime environment. Model checking is an effective method for this problem, since it is a formal verification approach which has an advantage in exploring all behaviors of the system and discovering subtle errors. In this paper, we present a novel timed automaton model for FTSP. The main insight of our method is that by using timed automata, we can introduce the transmission delay and node failures that exist in real WSNs into our model and check whether FTSP is robust to node failures under a more realistic environment. We generate the timed automata models of FTSP and verify them by the model checking tool UPPAAL. Our evaluation result depicts an error of FTSP when the algorithm runs in the scenario that two root nodes fail continuously.

Program understanding plays an important role in the maintenance and reuse of open source code. Rapid evolving and bad documentation makes the understanding and reusing difficult. Design patterns are widely employed in the open source code. In this paper, we propose a design pattern directed clustering approach to help understand the structure of open source code. According to the approach, we have implemented a prototype tool. We also conducted an experiment on an open source system to evaluate it.

Test case generation based on design specifications is an important part of testing processes. In this paper, Unified Modeling Language activity diagrams are used as design specifications. By setting up several test adequacy criteria with respect to activity diagrams, an automatic approach is presented to generate test cases for Java programs. Instead of directly deriving test cases from activity diagrams, this approach selects test cases from a set of randomly generated ones according to a given test adequacy criterion. In the approach, we first instrument a Java program under testing according to its activity diagram model, and randomly generate abundant test cases for the program. Then, by running the instrumented program we obtain the corresponding program execution traces. Finally, by matching these traces with the behavior of the activity diagram, a reduced set of test cases are selected according to the given test adequacy criterion. This approach can also be used to check the consistency between the program execution traces and the behavior of activity diagrams.

Hybrid automata are well studied formal models for hybrid systems with both discrete and continuous state changes. However, the analysis of hybrid automata is quite difficult. Even for the simple class of linear hybrid automata, the reachability problem is undecidable. In the author's previous work, for linear hybrid automata we proposed a linear programming based approach to check one path at a time while the length of the path and the size of the automaton being checked can be large enough to handle problems of practical interest. Based on this approach, in this paper we present a prototype tool BACH to perform bounded reachability checking of linear hybrid automata. The experiment data shows that BACH has good performance and scalability, and supports our belief that BACH could become a powerful assistant to design engineers for the reachability analysis of linear hybrid automata.

Data race occurs when multiple threads simultaneously access shared data without appropriate synchronization, and at least one is write. System with a data race is nondeterministic and may generate different outputs even with the same input, according to different interleaving of data access. We present a model-based approach for detecting data races in concurrent Java programs. We extend UML Activity diagrams with data operation tags, to model program behavior. Program under test (PUT) is instrumented according to the model. It is then executed with random test cases generated based on path analysis of the model. Execution traces are reverse engineered and used for post-mortem verification. First, data races are identified by searching the time overlaps of entering and exiting critical sections of different threads. Second, implementation could be inconsistent with the design. The problem may tangle with race condition and makes it hard to detect races. We compare the event sequences with the behavior model for consistency checking. Identified inconsistencies help debuggers locate the defects in the PUT. A prototype tool named tocAj implements the proposed approach and was successfully applied to several cases studies.

The growing scale and complexity of the enterprise computing systems under distributed and heterogeneous environments present new challenges to system development, integration, and maintenance. In this paper, we present a model driven Web service development framework to combat these challenges. The framework capitalizes on the UML profile for Enterprise Distributed Object Computing (EDOC), MDA and Web services. Within the framework, first, the platform independent models (PIMs) are created using the EDOC profile. Second, the PIMs are broken down into sub PIMs according to functional decomposition, each of which can provide service independently and will be implemented in a Web service. Then, these sub PIMs are transformed into the corresponding Web service interface models for service publication and invoking. Finally, supported by model transform techniques, the sub PIMs are implemented into Web services on specific platforms. Automatic model transformation is the key to this framework, therefore, the transformation from EDOC models to Web service interface models within this framework is deeply discussed, and the detailed transformation rules are proposed. A case study is also provided to demonstrate the effectiveness of these rules and the merits of this framework

Test case generation is the most important part of the testing efforts, the automation of specification based test case generation needs formal or semi-formal specifications. As a semi-formal modelling language, UML is widely used to describe analysis and design specifications by both academia and industry, thus UML models become the sources of test generation naturally. Test cases are usually generated from the requirement or the code while the design is seldom concerned, this paper proposes an approach to generate test cases directly from UML activity diagram using Gray-box method, where the design is reused to avoid the cost of test model creation. In this approach, test scenarios are directly derived from the activity diagram modelling an operation. Then all the information for test case generation, i.e. input/output sequence and parameters, the constraint conditions and expected object method sequence, is extracted from each test scenario. At last, the possible values of all the input/output parameters could be generated by applying category-partition method, and test suite could be systematically generated to find the inconsistency between the implementation and the design. A prototype tool named UMLTGF has been developed to support the above process.