Low-rank tensor recovery methods within the tensor singular value decomposition (t-SVD) framework have demonstrated considerable success by leveraging the inherent low-dimensional structures of multi-dimensional data. However, previous approaches in this framework often rely on linear transforms or, in some cases, nonlinear transforms constructed with fully connected networks (FCNs). These methods typically promote a global low-rank structure, which may not fully exploit the nature of multiple subspaces in real-world data. In this work, we propose a nonlinear transform to capture long-range dependencies and diverse patterns across multiple subspaces of the data within the t-SVD framework. This approach provides a richer and more nuanced representation compared to the localized processing typically seen in FCN-based transforms. In the transform domain, we construct a low-rank self-representation layer that fully exploits the multi-subspace structure inherent in tensor data. Instead of merely enforcing overall low-rankness, our method minimizes the nuclear norm of a self-representation tensor, allowing for a more precise and joint characterization of multiple subspaces. This results in a more accurate representation of the data's intrinsic low-dimensional structures, leading to superior recovery performance. This new framework, termed the DEep Low-rank Tensor representAtion (DELTA), is evaluated across several typical multi-dimensional data recovery applications, including tensor completion, robust tensor completion, and spectral snapshot imaging. Experiments on various real-world multi-dimensional data illustrate the superior performance of our DELTA.

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

Android apps rely on application programming interfaces (APIs) to access various functionalities of Android devices. These APIs however are regularly updated to incorporatenew features while the old APIs get deprecated. Even though the importance of updating deprecated API usages with the recommended replacement APIs has been widely recognized, it is non-trivial to update the deprecated API usages. Therefore, the usages of deprecated APIs linger in Android apps and cause compatibility issues in practice. This paper introduces GUPPY, an automated approach that utilizes large language models (LLMs) to update Android deprecated API usages. By employing carefully crafted Chain-of-Thoughts prompts, GUPPY leverages GPT-4, one of the most powerful LLMs, to update deprecated-API usages, ensuring compatibility in both the old and new API levels. Additionally, GUPPY uses GPT-4 to generate tests, identify incorrect updates, and refine the API usage through an iterative process until the tests pass or a specified limit is reached. Our evaluation, conducted on 360 benchmark API usages from 20 deprecated APIs and an additional 156 deprecated API usages from the latest API levels 33 and 34, demonstrates GUPPY’s advantages over the state-of-the-art techniques.

Deep learning has been widely applied to various aspects of computer vision, but the emergence of adversarial attacks raises concerns about its reliability. Adversarial training (AT) is one of the most effective defense methods, which incorporates adversarial examples into the training data. However, AT is typically employed in a discriminative learning manner, i.e., learning the mapping (conditional probability) from samples to labels, it essentially reinforces this mapping without considering the underlying data distribution. It is notable that adversarial examples often deviate from the distribution of normal (clean) samples. Therefore, building upon existing adversarial defense schemes, we propose to further exploit the distribution of normal samples, partly from the generative learning perspective, resulting in a novel robustness enhancement paradigm. We train a simple autoencoder (AE) autoregressively on normal samples to learn their prior distribution, effectively serving as an image manifold. This AE is then used as a manifold projection operator to incorporate the distribution information of normal samples. Specifically, we organically integrate the pretrained AE into the training process of both AT and adversarial distillation (AD), a method aiming at improving the robustness of small models with low capacity. Since the AE captures the distribution of normal samples, it can adaptively pull adversarial examples closer to the normal sample manifold, weakening the attack strength of adversarial samples and easing the learning of mappings from adversarial samples to correct labels. From the Pearson correlation coefficient (PCC) between the statistics on normal and adversarial examples, it’s validated that the AE indeed pulls adversarial samples closer to normal samples. Extensive experiments illustrate that our proposed adversarial defense paradigm significantly improves the robustness compared with previous state-of-the-art AT and AD methods.

Information theft attacks pose a significant risk to Large Language Model (LLM) tool-learning systems. Adversaries can inject malicious commands through compromised tools, manipulating LLMs to send sensitive information to these tools, which leads to potential privacy breaches. However, existing attack approaches are black-box oriented and rely on static commands that cannot adapt flexibly to the changes in user queries and the invocation chain of tools. It makes malicious commands more likely to be detected by LLM and leads to attack failure. In this paper, we propose AutoCMD, a dynamic attack comment generation approach for information theft attacks in LLM tool-learning systems. Inspired by the concept of mimicking the familiar, AutoCMD is capable of inferring the information utilized by upstream tools in the toolchain through learning on open-source systems and reinforcement with target system examples, thereby generating more targeted commands for information theft. The evaluation results show that AutoCMD outperforms the baselines with +13.2% ASR_{Theft}, and can be generalized to new tool-learning systems to expose their information leakage risks. We also design four defense methods to effectively protect tool-learning systems from the attack.

The combination of computer vision and artificial intelligence is fundamentally transforming a broad spectrum of industries by enabling machines to interpret and act upon visual data with high levels of accuracy. As the biggest and by far the most popular open-source computer vision library, OpenCV library provides an extensive suite of programming functions supporting real-time computer vision. Bugs in the OpenCV library can affect the downstream computer vision applications, and it is critical to ensure the reliability of the OpenCV library. This paper introduces VistaFuzz, a novel technique for harnessing large language models (LLMs) for document-guided fuzzing of the OpenCV library. Vistafuzz utilizes LLMs to parse API documentation and obtain standardized API information. Based on this standardized information, Vista Fuzz extracts constraints on individual input parameters and dependencies between these. Using these constraints and dependencies, VistaFuzz then generates new input values to systematically test each target API. We evaluate the effectiveness of Vistafuzz in testing 330 APIs in the OpenCV library, and the results show that Vistafuzz detected 17 new bugs, where 10 bugs have been confirmed, and 5 of these have been fixed.

Deep learning powers critical applications such as autonomous driving, healthcare, and finance, where the correctness of underlying libraries is essential. Bugs in widely used deep learning APIs can propagate to downstream systems, causing serious consequences. While existing fuzzing techniques detect bugs through intra-framework testing across hardware backends (CPU vs. GPU), they may miss bugs that manifest identically across backends and thus escape detection under these strategies. To address this problem, we propose XAMT, a cross-framework fuzzing method that tests deep learning libraries by matching and comparing functionally equivalent APIs across different frameworks. XAMT matches APIs using similarity-based rules based on names, descriptions, and parameter structures. It then aligns inputs and applies variance-guided differential testing to detect bugs. We evaluated XAMT on five popular frameworks, including PyTorch, TensorFlow, Keras, Chainer, and JAX. XAMT matched 839 APIs and identified 238 matched API groups, and detected 17 bugs, 12 of which have been confirmed. Our results show that XAMT uncovers bugs undetectable by intraframework testing, especially those that manifest consistently across backends. XAMT offers a complementary approach to existing methods and offers a new perspective on the testing of deep learning libraries.

Abstract Android dominates the mobile operating system market, yet ensuring the quality and reliability of Android applications remains a persistent challenge. The diversity of devices, screen sizes, and OS versions complicates testing, leading to fragmented adoption of best practices. Despite advancements in automated testing, there is Limited empirical evidence on how developers test Android applications and the extent to which existing tools and frameworks are utilized effectively. In this paper, we aim to investigate the current state of Android app testing, identifying key challenges, Limitations, and best practices. Specifically, we assess the adoption of automated testing, test coverage levels, and the impact of testing practices on software quality. We conduct an experimental study on 2965 open-source Android apps, examining the quantity and coverage of the tests used for open-source Android app development. We further conduct a survey to gather more insights in testing practices from Android app developers and testers. The results reveal a limited adoption of testing among Android app developers, a restricted range of testing tools and frameworks being used, and low code and API coverage in testing. This investigation shows that current Android app testing practices are lacking the use of automated testing tools and embarks on a need for more awareness and adoption of state-of-the-art testing tools and techniques.

Symbolic execution is a popular program analysis technique. It systematically explores all feasible paths of a program but its scalability is largely limited by the path explosion problem, which causes the number of paths proliferates at runtime. A key idea in existing methods to mitigate this problem is to guide the selection of states for path exploration, which primarily relies on the features to represent program states. In this paper, we propose concrete constraint guided symbolic execution, which aims to cover more concrete branches and ultimately improve the overall code coverage during symbolic execution. Our key insight is based on the fact that symbolic execution strives to cover all symbolic branches while concrete branches are neglected, and directing symbolic execution toward uncovered concrete branches has a great potential to improve the overall code coverage. The experimental results demonstrate that our approach can improve the ability of KLEE to both increase code coverage and find more security violations on 10 open-source C programs.

In an era where Android dominates the mobile operating system market, it is important to ensure high quality Android app delivery. In this paper, we delve into the essential need for effective Android app testing in a market characterized by diversity and widespread usage and empirically investigate testing practices for Android apps. We conduct an experimental study on 2965 open-source Android apps, examining the quantity and coverage of the tests used for open-source Android app development. We further conduct a survey to gather more insights in testing practices from Android app developers and testers. The results reveal a limited adoption of testing among Android app development, a restricted range of testing tools and frameworks being used, and low code and API coverage in testing. This investigation shows that current Android app testing practices are lacking the use of automated testing tools and embarks on a need for more awareness and adoption of state-of-the-art testing tools and techniques.

Security patches are essential for enhancing the stability and robustness of projects in the open-source software community. While vulnerabilities are officially expected to be patched before being disclosed, patching vulnerabilities is complicated and remains a struggle for many organizations. To patch vulnerabilities, security practitioners typically track vulnerable issue reports (IRs), and analyze their relevant insecure code to generate potential patches. However, the relevant insecure code may not be explicitly specified and practitioners cannot track the insecure code in the repositories, thus limiting their ability to generate patches. In such cases, providing examples of insecure code and the corresponding patches would benefit the security developers to better locate and resolve the actual insecure code. In this paper, we propose PatUntrack, an automated approach to generating patch examples from IRs without tracked insecure code. PatUntrack utilizes auto-prompting to optimize the Large Language Model (LLM) to make it applicable for analyzing the vulnerabilities described in IRs and generating appropriate patch examples. Specifically, it first generates the completed description of the Vulnerability-Triggering Path (VTP) from vulnerable IRs. Then, it corrects potential hallucinations in the VTP description with external golden knowledge. Finally, it generates Top-K pairs of Insecure Code and Patch Example based on the corrected VTP description. To evaluate the performance of PatUntrack, we conducted experiments on 5,465 vulnerable IRs. The experimental results show that PatUntrack can obtain the highest performance and improve the traditional LLM baselines by +17.7% (MatchFix) and +14.6% (Fix@10) on average in patch example generation. Furthermore, PatUntrack was applied to generate patch examples for 76 newly disclosed vulnerable IRs. 27 out of 37 replies from the authors of these IRs confirmed the usefulness of the patch examples generated by PatUntrack, indicating that they can benefit from these examples for patching the vulnerabilities.

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

Moving Target Defenses (MTD) are proactive security countermeasures that change the attack surface in a system in ways that make it harder for attackers to succeed. These techniques have been shown to be effective, and their application in software-defined networking (SDN) against simple automated attacks is growing in popularity. However, with the increased knowledge of and ease of access to Artificial Intelligence (AI) techniques, AI is starting to be used to enhance cyber attacks, which are becoming increasingly complex. Hence, the evaluation of MTDs against simple automated attacks is no longer enough to demonstrate their effectiveness in increasing system security.

Secure coding practices (SCPs) have been proposed to guide software developers to write code securely to prevent potential security vulnerabilities. Yet, they are typically one-sentence principles without detailed specifications, e.g., “Properly free allocated memory upon the completion of functions and at all exit points.”, which makes them difficult to follow in practice, especially for software developers who are not yet experienced in secure programming. To address this problem, this paper proposes SCPatcher, an automated approach to enrich secure coding practices by mining crowd security discussions on online knowledge-sharing platforms, such as Stack Overflow. In particular, for each security post, SCPatcher first extracts the area of coding examples and coding explanations with a fix-prompt tuned Large Language Model (LLM) via Prompt Learning. Then, it hierarchically slices the lengthy code into coding examples and summarizes the coding explanations with the areas. Finally, SCPatcher matches the CWE and Public SCP, integrating them with extracted coding examples and explanations to form the SCP specifications, which are the wild SCPs with details, proposed by the developers. To evaluate the performance of SCPatcher, we conduct experiments on 3,907 security posts from Stack Overflow. The experimental results show that SCPatcher outperforms all baselines in extracting the coding examples with 2.73 % MLine on average, as well as coding explanations with 3.97 % F1 on average. Moreover, we apply SCPatcher on 447 new security posts to further evaluate its practicality, and the extracted SCP specifications enrich the public SCPs with 3,074 lines of code and 1,967 sentences.

While the Java Virtual Machine (JVM) plays a vital role in ensuring correct executions of Java applications, testing JVMs via generating and running class files on them can be rather challenging. The existing techniques, e.g., ClassFuzz and Classming, attempt to leverage the power of fuzzing and differential testing to cope with JVM intricacies by exposing discrepant execution results among different JVMs, i.e., inter-JVM discrepancies, for testing analytics. However, their adopted fuzzers are insufficiently guided since they include no well-designed seed and mutator scheduling mechanisms, leading to inefficient differential testing. To address such issues, in this paper, we propose SJFuzz, the first JVM fuzzing framework with seed and mutator scheduling mechanisms for automated JVM differential testing. Overall, SJFuzz aims to mutate class files via control flow mutators to facilitate the exposure of inter-JVM discrepancies. To this end, SJFuzz schedules seeds (class files) for mutations based on the discrepancy and diversity guidance. SJFuzz also schedules mutators for diversifying class file generation. To evaluate SJFuzz, we conduct an extensive study on multiple representative real-world JVMs, and the experimental results show that SJFuzz significantly outperforms the state-of-the-art mutation-based and generation-based JVM fuzzers in terms of the inter-JVM discrepancy exposure and the class file diversity. Moreover, SJFuzz successfully reported 46 potential JVM issues, and 20 of them have been confirmed as bugs and 16 have been fixed by the JVM developers.

Forward symbolic execution is a powerful systematic software analysis technique, but suffers from the high cost of constraint solving. During symbolic execution, off-the-shelf constraint solvers are used to check the satisfiability of path conditions whenever they are updated. However, the satisfiability information is sufficient for path exploration, while the concrete solutions are needed only for special cases, e.g., when a property violation is detected. Thus, symbolic execution can be made more efficient by leveraging rapid constraint classification instead of time-consuming constraint solving when the concrete solutions are not necessary. This paper introduces ICON, a novel approach to scaling symbolic execution with intelligent constraint classification, where neural networks are utilized to classify path conditions for satisfiability. Experimental evaluation shows ICON is highly accurate in classifying path conditions, is faster than state-of-the-art techniques for conventional constraint solving, learning based constraint solving, and constraint solution reuse, and enables more efficient symbolic execution.

Android application programming interface (API) enables app developers to harness the functionalities of Android devices by interfacing with services and hardware using a Software Development Kit (SDK). However, API frequently evolves together with its associated SDK, and compatibility issues may arise when the API level supported by the underlying device differs from the API level targeted by app developers. These issues can lead to unexpected behaviors, resulting in a bad user experience. This article presents ACID, a novel approach to detecting Android API compatibility issues induced by API evolution. It detects both API invocation compatibility issues and API callback compatibility issues using API differences and static analysis of the app code. Experiments with 20 benchmark apps show that ACID is more accurate and faster than the state-of-the-art techniques in detecting API compatibility issues. The application of ACID on 2965 real-world apps further demonstrates its practical applicability. To eliminate the false positives reported by ACID, this article also presents a simple yet effective method to quickly verify the compatibility issues by selecting and executing the relevant tests from app's test suite, and experimental results demonstrate the verification method can eliminate most false positives when app's test suite has good coverage of the API usages.

Background: The continuous evolution of the Android operating system necessitates regular API updates, which may affect the functionality of Android apps. Recent studies investigated API evolution to ensure the reliability of Android apps; however, they focused on API methods alone. Aim: We aim to empirically investigate how Android API fields evolve, and how this evolution affects the compatibility of Android apps. Method: We conducted a study based on real-world app development history data involving 11098 tags out of 105 popular open-source Android apps. Results: Our study yields interesting findings, e.g., on average two API field compatibility issues exist per app, different types of checks are preferred when addressing different types of compatibility issues, and fixing compatibility issues induced by API field evolution takes more time than fixing compatibility issues induced by API method evolution. Conclusion: These findings will help developers and researchers better understand, detect, and handle Android compatibility issues induced by API field evolution.

Fuzzing nowadays has been commonly modeled as an optimization problem, e.g., maximizing code coverage under a given time budget via typical search-based solutions such as evolutionary algorithms. However, such solutions are widely argued to cause inefficient computing resource usage, i.e., inefficient mutations. To address this issue, two neural program-smoothing-based fuzzers, Neuzz and MTFuzz, have been recently proposed to approximate program branching behaviors via neural network models, which input byte sequences of a seed and output vectors representing program branching behaviors. Moreover, assuming that mutating the bytes with larger gradients can better explore branching behaviors, they develop strategies to mutate such bytes for generating new seeds as test cases. Meanwhile, although they have been shown to be effective in the original papers, they were only evaluated upon a limited dataset. In addition, it is still unclear how their key technical components and whether other factors can impact fuzzing performance. To further investigate neural program-smoothing-based fuzzing, we first construct a large-scale benchmark suite with a total of 28 popular open-source projects. Then, we extensively evaluate Neuzz and MTFuzz on such benchmarks. The evaluation results suggest that their edge coverage performance can be unstable. Moreover, neither neural network models nor mutation strategies can be consistently effective, and the power of their gradient-guidance mechanisms have been compromised. Inspired by such findings, we propose a simplistic technique, PreFuzz, which improves neural program-smoothing-based fuzzers with a resource-efficient edge selection mechanism to enhance their gradient guidance and a probabilistic byte selection mechanism to further boost mutation effectiveness. Our evaluation results indicate that PreFuzz can significantly increase the edge coverage of Neuzz/MTFuzz, and also reveal multiple practical guidelines to advance future research on neural program-smoothing-based fuzzing.

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

The Internet of Things (IoT) is a rapidly growing system of physical sensors and connected devices, enabling advanced information gathering, interpretation, and monitoring. The realization of a versatile IoT edge computing framework will accelerate seamless integration of the cyber-world with new physical IoT devices, and will fundamentally change and empower the way humans interact with the world. While there are many cloud-based IoT computing frameworks, they cannot support the needs of IoT applications that require local processing and guarantee of consumer’s privacy. This article presents experimentation with the opensource plug-and-play IoT middleware, called Cordova Accesor Host. We demonstrated that Cordova Accessor Host supports the essential ingredients of the composition and reusability of IoT services using the accessor as the basic building block and adopting an accessor-module-plugin design pattern. The portability is demonstrated by using the same accessor for collecting sensor data from radically different IoT devices such as, wearables (e.g., smartwatches) and microcontrollers (e.g., Arduino). Our energy profiling experiments show that IoT services deployed using the Cordova Accessor Host consume around 35% less battery power than the same IoT services deployed in the native Android operating system.

Android has recently become one of the best platforms for mobile app development. The constant evolution of this mobile operating system results in frequent updates to its APIs, which may affect the functionality of Android apps that are built upon them. Given the high frequency of Android API updates, impact analysis plays an important role in achieving high reliability for Android apps. This paper presents Apicia, a novel approach to API change impact analysis for Android Apps. Apicia reports the impact induced when updating the target API in terms of affected program elements (i.e., classes, methods, and statements), affected tests whose executions may exhibit different behaviors due to the API update, as well as untested affected code. We evaluate Apicia on 31 real-world Android apps, and the experimental results show that it can be cost effective on regression test selection as on average only 35.31% of tests per app are affected by API update. Moreover, since many affected statements are not covered by existing tests, Apicia can assist app developers in test suite augmentation for testing these statements. These findings indicate that Apicia is a promising technique for assisting Android developers with understanding, testing, and debugging for an API update.

The major challenge in audio-visual event localization task lies in how to fuse information from multiple modalities effectively. Recent works have shown that the attention mechanism is beneficial to the fusion process. In this paper, we propose a novel joint attention mechanism with multi-modal fusion methods for audio-visual event localization. Particularly, we present a concise yet valid architecture that effectively learns representations from multiple modalities in a joint manner. Initially, visual features are combined with auditory features and then turned into joint representations. Next, we make use of the joint representations to attend to visual features and auditory features, respectively. With the help of this joint co-attention, new visual and auditory features are produced, and thus both features can enjoy the mutually improved benefits from each other. It is worth noting that the joint co-attention unit is recursive meaning that it can be performed multiple times for obtaining better joint representations progressively. Extensive experiments on the public AVE dataset have shown that the proposed method achieves significantly better results than the state-of-the-art methods.

Android apps are developed using a Software Development Kit (SDK), where the Android application programming interface (API) enables app developers to harness the functionalities of Android devices by interacting with services and hardware. However, API frequently evolves together with its associated SDK. The mismatch between the API level supported by the device where apps are installed and the API level targeted by app developers can induce compatibility issues. These issues can manifest themselves as unexpected behaviors, including runtime crashes, creating a poor user experience. In this paper, we propose ACID, a novel approach to detecting compatibility issues caused by API evolution. We leverage API differences and static analysis of the source code of Android apps to detect both API invocation compatibility issues and API callback compatibility issues. Experiments on 20 benchmark apps from previous studies show that ACID is more accurate and faster in detecting compatibility issues than state-of-the-art. We also analyzed 35 more real-world apps to show the practical applicability of our approach.

Systematically checking code against functional correctness properties is costly, especially for complex code annotated with rich behavioral properties.This paper introduces a novel approach to checking properties in parallel using symbolic execution.Our approach partitions a check for the whole set of properties into multiple simpler sub-checks-each sub-check focusing on a single property, so that different properties are checked in parallel among multiple workers.Furthermore, each sub-check is guided by the checked property to avoid exploring irrelevant paths and is prioritized based on distances towards the checked property to provide early feedback.We implement our approach in Symbolic PathFinder, and experiments on systematically checking assertions in Java programs show the effectiveness of our approach.

Crowdsourced testing is an emerging trend in software testing, which relies on crowd workers to accomplish test tasks. Due to the cost constraint, a test task usually involves a limited number of crowd workers. Furthermore, more workers does not necessarily result in detecting more bugs. Different workers, who may have different testing experience and expertise, may make much differences in the test outcomes. For example, some inappropriate workers may miss true bug, introduce false bugs or report duplicated bugs, which decreases the test quality. In current practice, a test task is usually dispatched in a random manner, and the quality of testing cannot be guaranteed. Therefore, it is important to select an appropriate subset of workers to perform a test task to ensure high bug detection rate. This paper introduces ExReDiv, a novel hybrid approach to select a set of workers for a test task. It consists of three key strategies: the experience strategy selects experienced workers, the relevance strategy selects workers with expertise relevant to the given test task, the diversity strategy selects diverse workers to avoid detecting duplicated bugs. We evaluate ExReDiv based on 42 test tasks from one of the largest crowdsourced testing platforms in China, and the experimental results show its effectiveness.

Mobile app testing is challenging since each test needs to be executed in a variety of operating contexts including heterogeneous devices, various wireless networks and different locations. Crowdsourcing enables a mobile app test to be distributed as a crowdsourced task to leverage crowd workers to accomplish the test. However, high test quality and expected test context coverage are difficult to achieve in crowdsourced testing. Upon distributing a test task, mobile app providers neither know who to participate nor predict whether all the expected test contexts can be covered in the task. To address this problem, we put forward a novel research problem called Crowdsourced Testing Quality Maximization Under Context Coverage Constraint (Cocoon). Given a mobile app test task, our objective is to recommend a set of workers, from available crowd workers, such that the expected test context coverage and a high test quality can be achieved. We prove that the Cocoon problem is NP-Complete and then introduce two greedy approaches. Based on a real dataset from the largest Chinese crowdsourced testing platform, our evaluation shows the effectiveness and efficiency of the two approaches, which can be potentially used as online services in practice.

As the mobile platform pervades human life, much research in recent years has focused on improving the reliability of mobile applications on this platform, for example by applying automatic testing.However, researchers have primarily considered testing of single version of mobile applications.Although regression testing has been extensively studied for desktop applications, and many efficient and effective approaches have been proposed, these approaches cannot be directly applied to mobile applications.We first present a bug study on real-world Android bugs to show the existence of regression bugs, which motivates the need for an efficient regression test selection technique for Android applications.Next, we introduce Redroid, a new approach to regression test selection for Android applications.Our approach leverages the combination of static impact analysis and dynamic code coverage, and identifies a subset of test cases for reexecution on the modified application version.We implement our approach for Android applications, and demonstrate its efficacy through an extensive empirical study.

Symbolic execution is a powerful, systematic analysis that has received much visibility in the last decade. Scalability however remains a major challenge for symbolic execution. Compositional analysis is a well-known general purpose methodology for increasing scalability. This paper introduces a new approach for compositional symbolic execution. Our key insight is that we can summarize each analyzed method as a memoization tree that captures the crucial elements of symbolic execution, and leverage these memoization trees to efficiently replay the symbolic execution of the corresponding methods with respect to their calling contexts. Memoization trees offer a natural way to compose in the presence of heap operations, which cannot be dealt with by previous work that uses logical formulas as summaries for compositional symbolic execution. Our approach also enables efficient target oriented symbolic execution for error detection or program coverage. Initial experimental evaluation based on a prototype implementation in Symbolic Path Finder shows that our approach can be up to an order of magnitude faster than traditional non-compositional symbolic execution.

Characterizing software changes is fundamental for software maintenance. However existing techniques are imprecise leading to unnecessary maintenance efforts. We introduce a novel approach that computes a precise numeric characterization of program changes, which quantifies the likelihood of reaching target program events (e.g., assert violations or successful termination) and how that evolves with each program update, together with the percentage of inputs impacted by the change. This precise characterization leads to a natural ranking of different program changes based on their probability of execution and their impact on target events. The approach is based on model counting over the constraints collected with a symbolic execution of the program, and exploits the similarity between program versions to reduce cost and improve the quality of analysis results. We implemented our approach in the Symbolic PathFinder tool and illustrate it on several Java case studies, including the evaluation of different program repairs, mutants used in testing, or incremental analysis after a change.

Global software development (GSD) is considered as the coordinated activities of software development that are geographically and temporally distributed. The management of architectural knowledge, specifically, architectural design decisions (ADDs), becomes important in GSD due to the geographical, temporal, and cultural challenges in global environments. Based on our previous work on ADD management in localized software development, we present five ADD paradigms for GSD projects with different organizational structures. We also investigate the benefits and the challenges of these ADD paradigms by conducting an evaluation of the paradigms using extensive archived semi-structured interview data from industrial GSD projects. We aim to provide a fundamental framework for managing ADD documentation and evolution in GSD, as well as offer useful insights into managing architectural knowledge in a global setting.

This paper introduces iProperty, a novel approach that facilitates incremental checking of programs based on a property differencing technique. Specifically, iProperty aims to reduce the cost of checking properties as they are initially developed and as they co-evolve with the program. The key novelty of iProperty is to compute the differences between the new and old versions of expected properties to reduce the number and size of the properties that need to be checked during the initial development of the properties. Furthermore, property differencing is used in synergy with program behavior differencing techniques to optimize common regression scenarios, such as detecting regression errors or checking feature additions for conformance to new expected properties. Experimental results in the context of symbolic execution of Java programs annotated with properties written as assertions show the effectiveness of iProperty in utilizing change information to enable more efficient checking.

Program invariants can help software developers identify program properties that must be preserved as the software evolves, however, formulating correct invariants can be challenging. In this work, we introduce iDiscovery, a technique which leverages symbolic execution to improve the quality of dynamically discovered invariants computed by Daikon. Candidate invariants generated by Daikon are synthesized into assertions and instrumented onto the program. The instrumented code is executed symbolically to generate new test cases that are fed back to Daikon to help further refine the set of candidate invariants. This feedback loop is executed until a fix-point is reached. To mitigate the cost of symbolic execution, we present optimizations to prune the symbolic state space and to reduce the complexity of the generated path conditions. We also leverage recent advances in constraint solution reuse techniques to avoid computing results for the same constraints across iterations. Experimental results show that iDiscovery converges to a set of higher quality invariants compared to the initial set of candidate invariants in a small number of iterations.

The last few years have seen a resurgence of interest in the use of symbolic execution—a program analysis technique developed more than three decades ago to analyze program execution paths. Scaling symbolic execution to real systems remains challenging despite recent algorithmic and technological advances. An effective approach to address scalability is to reduce the scope of the analysis. For example, in regression analysis, differences between two related program versions are used to guide the analysis. While such an approach is intuitive, finding efficient and precise ways to identify program differences, and characterize their impact on how the program executes has proved challenging in practice. In this article, we present Directed Incremental Symbolic Execution (DiSE), a novel technique for detecting and characterizing the impact of program changes to scale symbolic execution. The novelty of DiSE is to combine the efficiencies of static analysis techniques to compute program difference information with the precision of symbolic execution to explore program execution paths and generate path conditions affected by the differences. DiSE complements other reduction and bounding techniques for improving symbolic execution. Furthermore, DiSE does not require analysis results to be carried forward as the software evolves—only the source code for two related program versions is required. An experimental evaluation using our implementation of DiSE illustrates its effectiveness at detecting and characterizing the effects of program changes.

This tool paper presents a tool for performing memoized symbolic execution (Memoise), an approach we developed in previous work for more efficient application of symbolic execution. The key idea in Memoise is to allow re-use of symbolic execution results across different runs of symbolic execution without having to re-compute previously computed results as done in earlier approaches. Specifically, Memoise builds a trie-based data structure to record path exploration information during a run of symbolic execution, optimizes the trie for the next run, and re-uses the resulting trie during the next run. Our tool optimizes symbolic execution in three standard scenarios where it is commonly applied: iterative deepening, regression analysis, and heuristic search. Our tool Memoise builds on the Symbolic PathFinder framework to provide more efficient symbolic execution of Java programs and is available online for download. The tool demonstration video is available at http://www.youtube.com/watch?v=ppfYOB0Z2vY.

This paper introduces memoized symbolic execution (Memoise), a new approach for more efficient application of forward symbolic execution, which is a well-studied technique for systematic exploration of program behaviors based on bounded execution paths. Our key insight is that application of symbolic execution often requires several successive runs of the technique on largely similar underlying problems, e.g., running it once to check a program to find a bug, fixing the bug, and running it again to check the modified program. Memoise introduces a trie-based data structure that stores the key elements of a run of symbolic execution. Maintenance of the trie during successive runs allows re-use of previously computed results of symbolic execution without the need for re-computing them as is traditionally done. Experiments using our prototype implementation of Memoise show the benefits it holds in various standard scenarios of using symbolic execution, e.g., with iterative deepening of exploration depth, to perform regression analysis, or to enhance coverage using heuristics.

This tool paper presents an embodiment of TestEra - a framework developed in previous work for specification-based testing of Java programs. To test a Java method, TestEra uses the method's pre-condition specification to generate test inputs and the post-condition to check correctness of outputs. TestEra supports specifications written in Alloy - a first-order, declarative language based on relations - and uses the SAT-based back-end of the Alloy tool-set for systematic generation of test suites. Each test case is a JUnit test method, which performs three key steps: (1) initialization of pre-state, i.e., creation of inputs to the method under test; (2) invocation of the method; and (3) checking the correctness of post-state, i.e., checking the method output. The tool supports visualization of inputs and outputs as object graphs for graphical illustration of method behavior. TestEra is available for download to be used as a library or as an Eclipse plug-in.

Model checking is a promising technique for verifying program behavior and is increasingly finding usage in industry. To date, however, researchers have primarily considered model checking of single versions of programs. It is well understood that model checking can be very expensive for large, complex programs. Thus, simply reapplying model checking techniques on subsequent versions of programs as they evolve, in the limited time that is typically available for validating new releases, presents challenges. To address these challenges, we have developed a new technique for regression model checking (RMC), that applies model checking incrementally to new versions of systems. We report results of an empirical study examining the effectiveness of our technique; our results show that it is significantly faster than traditional model checking.