Abstract Model checking in TLA+ provides strong correctness guarantees, yet practitioners continue to face significant challenges in interpreting counterexamples, understanding large state-transition graphs, and repairing faulty models. These difficulties stem from the limited explainability of raw model-checker output and the substantial manual effort required to trace violations back to source specifications. Although the TLA+ Toolbox includes a state diagram viewer, it offers only a static, fully expanded graph without folding, color highlighting, or semantic explanations, which limits its scalability and interpretability. We present ModelWisdom , an interactive environment that uses visualization and large language models to make TLA+ model checking more interpretable and actionable. ModelWisdom offers: (i) Model Visualization, with colorized violation highlighting, click-through links from transitions to TLA+ code, and mapping between violating states and broken properties; (ii) Graph Optimization, including tree-based structuring and node/edge folding to manage large models; (iii) Model Digest, which summarizes and explains subgraphs via large language models (LLMs) and performs preprocessing and partial explanations; and (iv) Model Repair, which extracts error information and supports iterative debugging. Together, these capabilities turn raw model-checker output into an interactive, explainable workflow, improving understanding and reducing debugging effort for nontrivial TLA+ specifications. This tool is available: https://github.com/ModelWisdom/ModelWisdom . A demonstrative video can be found at https://www.youtube.com/watch?v=plyZo30VShA .

The data-centric paradigm has emerged as a pivotal direction in artificial intelligence (AI), emphasizing the role of high-quality training data. This shift is especially critical in the Text-to-SQL task, where the scarcity, limited diversity, and structural simplicity of existing datasets constrain model performance. To address these challenges, we propose Text2SQL-Flow, a SQL-aware data augmentation framework that systematically generates large-scale, semantically valid, and structurally diverse Text-to-SQL pairs from limited seed data. Our framework spans six augmentation dimensions and integrates an end-to-end pipeline with auxiliary database selection, SQL executability verification, natural language (NL) question generation, NL-SQL correspondence verification, and chain-of-thought (CoT) reasoning trace generation. Leveraging this framework, we construct SQLFlow, a high-quality dataset comprising 75,386 annotated examples. We demonstrate the utility of SQLFlow in both fine-tuning and prompt-based settings. (1) For open-source large language models (LLMs), fine-tuning with SQLFlow improves problem-solving ability, delivering competitive gains across multiple benchmarks under the same data budget. (2) For closed-source LLMs, we propose a masked alignment retrieval method that uses SQLFlow as both a knowledge base and training data for the retrieval model, enabling structure-aware example matching via fine-grained NL-SQL alignments. Experiments show that our retrieval strategy outperforms existing example retrieval methods, highlighting the combined value of SQLFlow's data quality and our retrieval technique. Overall, our work provides a scalable, data-centric foundation for advancing Text-to-SQL systems and underscores the importance of structured, high-fidelity data in modern AI development. Our code is available at https://github.com/TechNomad-ds/Text2SQL-Flow.

Static analysis has profoundly improved software quality over the past decades, evolving from compiler-integrated optimizations and simple linting to sophisticated analyses for bug detection, security, and program understanding. In contrast, static analysis for hardware remains underexploited, resembling the early state of software analysis. Most existing hardware static analyses are confined to compiler optimizations and linting, lacking the sophistication needed to uncover complex design flaws. Furthermore, we observe that many hardware bugs reported in recent literature could have been identified by sophisticated static analyses that account for hardware-specific semantics and data flow; however, such bug detection analyses are absent today. To exploit the untapped potential of sophisticated hardware analysis, we present a series of bug detection analyses for Verilog, the predominant hardware description language (HDL). Moreover, these analyses are built upon our fundamental analyses that capture essential hardware-specific characteristics---such as bit-vector arithmetic, register synchronization, and digital component concurrency---and enable the examination of hardware data and control flows. Together, these analyses form a well-organized analysis suite with a modular design, in which diverse fundamental analyses combine to support bug detection, hardware understanding, and other potential clients. To implement these analyses, we further offer dedicated infrastructure, including a Verilog front end, an intermediate representation (IR) for analysis, and an analysis manager. To validate the utility of our analyses, we applied them to real-world hardware projects. Unlike software, real-world hardware projects tend to contain fewer but harder-to-detect bugs, as they typically undergo extensive simulation and rigorous verification to prevent the prohibitive costs of hardware defects. Despite this, our preliminary experimental results are highly promising: applying these proposed analyses to popular real-world Verilog projects (averaging 1.5K+ GitHub stars) uncovered nine previously unknown bugs, all confirmed by developers; moreover, we successfully identified a total of 18 bugs beyond the capabilities of existing static analyses for Verilog bug detection (i.e., linters). These results underscore the transformative potential of sophisticated static analysis in hardware design. Our analysis suite and infrastructure are also highly reusable: on average, each bug-detection client built on our analysis suite requires about 270 LoC, compared to 5,700 LoC when developed from scratch. By open-sourcing the entire system, involving substantial engineering effort (100K+ LoC), we aim to encourage further innovation and applications of sophisticated static analysis for hardware, hopefully fostering a similarly vibrant ecosystem that software analysis enjoys.

Understanding the Linux kernel is challenging due to its large and complex program state. While existing kernel debugging tools provide full access to kernel states at arbitrary levels of detail, developers often spend a significant amount of time sifting through redundant information to find what is truly useful. Additionally, the textual results provided by traditional debuggers are often insufficient for expressing high-dimensional information in a readable manner.

Java offers the Java Native Interface (JNI), which allows programs running in the Java Virtual Machine to invoke and be manipulated by native applications and libraries written in other languages, typically C. While JNI mechanism significantly enhances the Java platform's capabilities, it also presents challenges for static analysis of Java programs due to the complex behaviors introduced by native code. Therefore, effectively resolving the interactions between Java and native code is crucial for static analysis. In this paper, we introduce JNIFER, the first interactive cross-language pointer analysis for resolving native code in Java programs. JNIFER integrates both Java and C pointer analyses, equipped with advanced native call and JNI function analyses, enabling the simultaneous analysis of both Java and native code. During the analysis of crosslanguage interactions, the two analyzers interact with each other, constructing cross-language points-to relations and call graphs, thereby approximating the runtime behavior at the interaction sites. Our evaluation shows that JNIFER outperforms state-of-the-art approaches in terms of soundness while maintaining high precision and comparable efficiency, as evidenced by extensive experiments on OpenJDK and real-world Java applications.

Database-backed applications form the backbone of modern software, yet their complexity poses significant challenges for static analysis. These applications involve intricate interactions among application code, diverse database frameworks such as JDBC, Hibernate, and Spring Data JPA, and languages like Java and SQL. In this paper, we introduce DBridge, the first pointer analysis specifically designed for Java database-backed applications, capable of statically constructing comprehensive Java-to-database value flows. DBridge unifies application code analysis, database access specification modeling, SQL analysis, and database abstraction within a single pointer analysis framework, capturing interactions across a wide range of database access APIs and frameworks. Additionally, we present DB-Micro, a new micro-benchmark suite with 824 test cases crafted to systematically evaluate static analysis for database-backed applications. Experiments on DB-Micro and large, complex, real-world applications demonstrate DBridge’s effectiveness, achieving high recall and precision in building Java-to-database value flows efficiently and outperforming state-of-the-art tools in SQL statement identification. To further validate DBridge’s utility, we develop three client analyses for security and program understanding. Evaluation on these real-world applications reveals 30 Stored XSS attack vulnerabilities and 3 horizontal broken access control vulnerabilities, all previously undiscovered and real, as well as a high detection rate in impact analysis for schema changes. By open-sourcing DBridge (14K LoC) and DB-Micro (22K LoC), we seek to help advance static analysis for modern database-backed applications in the future.

ABSTRACT Self‐adaptive applications are becoming increasingly attractive, with the ability to smartly understand their runtime environments (or contexts) and deliver adaptive services, for example, location‐aware navigation or resource‐sensitive suggestions. However, due to inherent noises in the process of sensing and interpreting environmental information, there is a growing demand for guarding the consistency of collected contexts to avoid application misbehaviour and, at the same time, minimize extra costs. Existing work attempted to achieve this by speeding up the kernel constraint checking module inside the consistency guarding process. Most of these efforts were spent on reusing previous checking results or parallelizing the checking process, but they all leave one central step of constraint checking, that is, link generation, untouched. In this step, the checking engine provides reasons to explain the violation of constraints under check. It occupies a substantial part of the total time cost. Focusing on this key link generation step, we proposed MG, which deploys a rigourous analysis to automatically identify and avoid redundancy in the link generation without harming any correctness of the checking results. MG has been proven sound (always guaranteeing correctness) and complete (entirely removing redundancy). Moreover, based on our observation that MG's redundancy elimination also assists another core step of constraint checking to reduce unnecessary computation further, we additionally enhance MG with an escape‐condition optimization to escape unnecessary evaluation of truth values to further improve the efficiency of constraint checking in an aspect other than link generation. We call it MG+ for distinguishing. Our experiments with synthesized and real‐world consistency constraints reported that, compared with existing work, MG eliminates all link redundancy (83% to 0%), and based on it, MG+ further reduces significant truth value calculations (e.g., 49.74% reduction when combined with ECC and Con‐C). Generally, MG brought 14–500 speed‐ups in link generation, and MG+ further made 1.2–1.9 speed‐ups in truth value evaluation. Altogether, MG reduced the total constraint checking time up to 45.4%, and MG+ reduced it up to 61.0%.

We introduce the concept of compilation space as a new pivot for the comprehensive validation of just-in-time (JIT) compilers in modern language virtual machines (LVMs). The compilation space of a program encompasses a wide range of equivalent JIT-compilation choices, which can be cross-validated to ensure the correctness of the program’s JIT compilations. To thoroughly explore the compilation space in a lightweight and LVM-agnostic manner, we strategically mutate test programs with JIT-relevant but semantics-preserving code constructs, aiming to provoke diverse JIT compilation optimizations. We primarily implement this approach in Artemis , a tool for validating Java Virtual Machines (JVMs). Within three months, Artemis successfully discovered 85 bugs in three widely used production JVMs—HotSpot, OpenJ9, and the Android Runtime—where 53 were already confirmed or fixed and many of which were classified as critical. It is noteworthy that all reported bugs concern JIT compilers, highlighting the effectiveness and practicality of our technique. Building on the promising results with JVMs, we experimentally applied our technique to a state-of-the-art JavaScript Engine (JSE) fuzzer called Fuzzilli, aiming to augment it to find mis-compilation bugs without significantly sacrificing its ability to detect crashes. Our experiments demonstrate that our enhanced version of Fuzzilli namely Apollo could achieve comparable code coverage with a considerably smaller number of generated programs with a similar number of crashes. Additionally, Apollo successfully uncovered four mis-compilations in JavaScriptCore and SpiderMonkey within seven days. Following Artemis ’ and Apollo ’s success, we are expecting that the generality and practicability of our approach will make it broadly applicable for understanding and validating the JIT compilers of other LVMs.

Searching the occurrences of specific code patterns (code search) is a common task in software engineering, and programming by example (PBE) techniques have been applied to ease customizing code patterns. However, previous PBE tools only synthesize programs meeting the input-output examples, which may not always align with the user intent. To bridge this gap, this paper proposesExcalibur, a multi-modal (example and natural language description) and interactive synthesizer for code search.Excaliburensures that the generated programs are correct for the provided examples (soundness) and include the user-intended program (bounded completeness). Furthermore,Excaliburhelps the user identify the user-intended program through question-answer interaction. To minimize the required interaction efforts, question selection is crucial. To improve question selection for code search, we propose probabilistic version spaces (ProbVS), in which the user-intended program’s probability is high and others are low. ProbVS combines traditional version spaces for compactly representing extensive programs and large language models (on the user-provided natural language description) for adjusting programs’ probabilities to align with users’ intents. Extensive experiments on a benchmark of 44 tasks demonstrated the effectiveness ofExcaliburand ProbVS and demystified how ProbVS affects probability distributions and how the configurable parameters affect ProbVS.

Deep Neural Networks (DNNs) have demonstrated remarkable accuracy in vision classification tasks. However, they exhibit vulnerability to additional noises known as adversarial attacks. Previous studies hypothesize that this vulnerability might stem from the fact that high-accuracy DNNs heavily rely on irrelevant and non-robust features, such as textures and the background. In this work, we reveal that edge information extracted from images can provide relevant and robust features related to shapes and the foreground. These features assist pretrained DNNs in achieving improved adversarial robustness without compromising their accuracy on clean images. A lightweight and plug-and-play EdgeNet is proposed, which can be seamlessly integrated into existing pretrained DNNs, including Vision Transformers, a recent family of state-of-the-art models for vision classification. Our EdgeNet can process edges derived from either clean nature images or noisy adversarial images, yielding robust features which can be injected into the intermediate layers of the frozen backbone DNNs. The cost of obtaining such edges using conventional edge detection algorithms (e.g., Canny edge detector) is marginal, and the cost of training the EdgeNet is equivalent to that of fine-tuning the backbone network with techniques such as Adapter.

Crafting high-quality mutators-the core of mutation-based fuzzing that shapes the search space-is challenging. It requires human expertise and creativity, and their implementation demands knowledge of compiler internals. This paper presents MetaMut framework for developing new, useful mutators for compiler fuzzing. It integrates our compiler-domain knowledge into prompts and processes that can best harness the capabilities of a large language model. With MetaMut, we have successfully created 118 semantic-aware mutators at approximately $0.5 each, with only moderate human effort. With these mutators, our fuzzer uncovered 131 bugs in GCC and Clang, 129 of which were confirmed or fixed. The success of MetaMut suggests that the integration of AI into software and system engineering tasks traditionally thought to require expert human intervention could be a promising research direction.

The increasing complexity of software and its execution environment makes in-house software testing challenging. Field testing, which conducts software testing in production environments, is a potential solution to this issue. However, existing field testing systems have not seen widespread use due to their inconvenience, lack of generality, and limited capabilities. We identify four essential requirements that a practical field testing system must fulfill: robust, efficient, handy, and versatile. This paper presents the design and implementation of Jaft, a field testing system for Java software meeting the aforementioned requirements through its design of field testing API, isolation mechanism, and runtime module. Evaluation results show that it has acceptable runtime overhead and can improve test effectiveness.

Code generation benchmarks such as HumanEval are widely adopted to evaluate LLMs' capabilities. However, after consolidating the latest 24 benchmarks, we noticed three significant imbalances. First, imbalanced programming language. 95.8% of benchmarks involve Python, while only 5 benchmarks involve Java, resulting in an insufficient understanding of LLMs' capability to generate Java code. Second, imbalanced code granularity. Function-/statement-level benchmarks account for over 83.3% of benchmarks. Only a mere handful extends to class-/project-levels, and all are limited to Python. Third, lacking advanced features. Existing benchmarks primarily assess basic coding skills (e.g., variables, operators, and control structures), while overlooking advanced Object-Oriented Programming (OOP) features (i.e., encapsulation, inheritance, and polymorphism). Considering the prevalence of these advanced features in real-world Java project development, constructing benchmarks to test LLMs on handling OOP features is necessary.

Constraint checking techniques are being widely used for ensuring the consistency of software artifacts during their development and evolution (e.g., detecting inconsistency in an application's running contexts or identifying rule violation in the code being developed). Typically, consistency constraints are formulated and checked upon the changes of software artifacts under checking. When any constraint is violated, an inconsistency is said to occur and then follow-up actions can be taken to remedy the problem. Currently, various constraint checking techniques have been proposed and implemented with sophisticated mechanisms for higher efficiency and scalability. However, these implementations could be far from being well tested due to their oracle problems, i.e., hardly able to tell what the checking result should be, given any software artifacts and their consistency constraints to check. In this paper, we leverage metamorphic testing and propose a family of metamorphic relations catered for testing constraint checking implementations. We dedicatedly design these relations by following the sensitivity principle via a fine-granularity control and the diversity principle via input-oriented transformations. Our experiments reported promising results (disclosing 80 % mutation bugs and five real bugs) without the need of any manual labeling.

Programming by example (PBE) is an emerging programming paradigm that automatically synthesizes programs specified by user-provided input-output examples. Despite the convenience for end-users, implementing PBE tools often requires strong expertise in programming language and synthesis algorithms. Such a level of knowledge is uncommon among software developers. It greatly limits the broad adoption of PBE by the industry. To facilitate the adoption of PBE techniques, we propose a PBE framework called Bee , which leverages an “entity-action” model based on relational tables to ease PBE development for a wide but restrained range of domains. Implementing PBE tools with Bee only requires adapting domain-specific data entities and user actions to tables, with no need to design a domain-specific language or an efficient synthesis algorithm. The synthesis algorithm of Bee exploits bidirectional searching and constraint-solving techniques to address the challenge of value computation nested in table transformation. We evaluated Bee ’s effectiveness on 64 PBE tasks from three different domains and usability with a human study of 12 participants. Evaluation results show that Bee is easier to learn and use than the state-of-the-art PBE framework, and the bidirectional algorithm achieves comparable performance to domain-specifically optimized synthesizers.

Python projects grow quickly by code reuse and building automation based on third-party libraries. However, the version constraints associated with these libraries are prone to mal-configuration, and this forms a major obstacle to correct project building (known as dependency-conflict (DC) building failure). Our empirical findings suggest that such mal-configured version constraints were mainly prepared manually, and could essentially be refined for better quality to improve the chance of successful project building. We propose a LooCo approach to refining Python projects’ library version constraints by automatically loosening them to maximize their solutions, while keeping the libraries to observe their original behaviors. Our experimental results with real-life Python projects report that LooCo could efficiently refine library version constraints (0.4s per version loosening) by effective loosening (5.5 new versions expanded on average) automatically, and transform 54.8% originally unsolvable cases into solvable ones (i.e., successful building) and significantly increase solutions (21 more on average) for originally solvable cases.

This paper introduces the novel concept of compilation space, which facilitates the thorough validation of just-in-time (JIT) compilers in modern language virtual machines (LVMs). The compilation space, even for a single program, consists of an extensive array of JIT compilation choices, which can be cross-validated for the correctness of JIT compilation. To thoroughly explore the compilation space in a lightweight and LVM-agnostic manner, we strategically mutate test programs with JIT-relevant, yet semantics-preserving code structures to trigger diverse JIT compilation choices. We realize our technique in Artemis, a tool for the Java virtual machine (JVM). Our evaluation has led to 85 bug reports for three widely used production JVMs, namely HotSpot, OpenJ9, and the Android Runtime. Among them, 53 have already been confirmed or fixed with many being critical. It is also worth mentioning that all the reported bugs concern JIT compilers, demonstrating the clear effectiveness and strong practicability of our technique. We expect that the generality and practicability of our approach will make it broadly applicable for understanding and validating JIT compilers.

With the increasing need to apply modern software techniques to hardware design, Verilog, the most popular Hardware Description Language (HDL), plays an infrastructure role. However, Verilog has several semantic pitfalls that often confuse software and hardware developers. Although prior research on formal semantics for Verilog exists, it is not comprehensive and has not fully addressed these issues. In this work, we present a novel scheme inspired by previous work on defining core languages for software languages like JavaScript and Python. Specifically, we define the formal semantics of Verilog using a core language called λ V , which captures the essence of Verilog using as few language structures as possible. λ V not only covers the most complete set of language features to date, but also addresses the aforementioned pitfalls. We implemented λ V with about 27,000 lines of Java code, and comprehensively tested its totality and conformance with Verilog. As a reliable reference semantics, λ V can detect semantic bugs in real-world Verilog simulators and expose ambiguities in Verilog’s standard specification. Moreover, as a useful core language, λ V has the potential to facilitate the development of tools such as a state-space explorer and a concolic execution tool for Verilog.

Over the past decades, context sensitivity has been considered as one of the most effective ideas for improving the precision of pointer analysis for Java. Different from the extremely fast context-insensitivity approach, context sensitivity requires every program method to be analyzed under different contexts for separating the static abstractions of different dynamic instantiations of the method’s variables and heap objects, and thus reducing spurious object flows introduced by method calls. However, despite great precision benefits, as each method is equivalently cloned and analyzed under each context, context sensitivity brings heavy efficiency costs. Recently, numerous selective context-sensitive approaches have been put forth for scaling pointer analysis to large and complex Java programs by applying contexts only to the selected methods while analyzing the remaining ones context-insensitively; however, because the selective approaches do not fundamentally alter the primary methodology of context sensitivity (and do not thus remove its efficiency bottleneck), they produce much improved but still limited results. In this work, we present a fundamentally different approach called Cut-Shortcut for fast and precise pointer analysis for Java. Its insight is simple: the main effect of cloning methods under different contexts is to filter spurious object flows that have been merged inside a callee method; from the view of a typical pointer flow graph (PFG), such effect can be simulated by cutting off (Cut) the edges that introduce precision loss to certain pointers and adding Shortcut edges directly from source pointers to the target ones circumventing the method on PFG. As a result, we can achieve the effect of context sensitivity without contexts. We identify three general program patterns and develop algorithms based on them to safely cut off and add shortcut edges on PFG, formalize them and formally prove the soundness. To comprehensively validate Cut-Shortcut’s effectiveness, we implement two versions of Cut-Shortcut for two state-of-the-art pointer analysis frameworks for Java, one in Datalog for the declarative Doop and the other in Java for the imperative Tai-e, and we consider all the large and complex programs used in recent literatures that meet the experimental requirements. The evaluation results are extremely promising: Cut-Shortcut is even able to run faster than context insensitivity for most evaluated programs while obtaining high precision that is comparable to context sensitivity (if scalable) in both frameworks. This is for the first time that we have been able to achieve such a good efficiency and precision trade-off for those hard-to-analyze programs, and we hope Cut-Shortcut could offer new perspectives for developing more effective pointer analysis for Java in the future.

Greetings and welcome to the third issue of IEEE TRANSACTIONS ON COMPUTATIONAL SOCIAL SYSTEMS (TCSS) for 2023. The authors are delighted to share some exciting news with our esteemed readership.

Cyber-physical systems (CPSs) are complex ensembles of physical and cyber components that cooperate to offer dynamic and adaptive functionalities. Uncertainty can arise from a plethora of sources in the entangled components, ranging from the unreliable perception, the nondeterministic action effects, to even the changes in the environment. Existing controlling approaches, such as those using Markov decision process, have limited ability in handling uncertainty. To address the challenge, in this article, we novelly propose using partially observable Markov decision processes (POMDPs) to model CPS under uncertainty and show that common types of uncertainties can be modeled by partial observations and nondeterministic actions over probabilistic distributions. With POMDPs, strategies that can optimally control CPS are synthesized. We further propose a strategywise verification method, which resolves the difficult problem of verifying the entire POMDP, to offer reliable controlling strategies. Experiments on two representative cases of CPS show promising results compared with existing approaches.

Vulnerabilities are known reported security threats that affect a large amount of packages in thenpmecosystem. To mitigate these security threats, the open-source community strongly suggests vulnerable packages to timely publish vulnerability fixes and recommends affected packages to update their dependencies. However, there are still serious lags in the propagation of vulnerability fixes in the ecosystem. In our preliminary study on the latest versions of 356,283 activenpmpackages, we found that 20.0% of them can still introduce vulnerabilities via direct or transitive dependencies although the involved vulnerable packages have already published fix versions for over a year. Prior study by (Chinthanet et al. 2021) lays the groundwork for research on how to mitigate propagation lags of vulnerability fixes in an ecosystem. They conducted an empirical investigation to identify lags that might occur between the vulnerable package release and its fixing release. They found that factors such as the branch upon which a fix landed and the severity of the vulnerability had a small effect on its propagation trajectory throughout the ecosystem. To ensure quick adoption and propagation of a release that contains the fix, they gave several actionable advice to developers and researchers. However, it is still an open question how to design an effective technique to accelerate the propagation of vulnerability fixes. Motivated by this problem, in this paper, we conducted an empirical study to learn the scale of packages that block the propagation of vulnerability fixes in the ecosystem and investigate their evolution characteristics. Furthermore, we distilled the remediation strategies that have better effects on mitigating the fix propagation lags. Leveraging our empirical findings, we propose an ecosystem-level technique,Plumber, for deriving feasible remediation strategies to boost the propagation of vulnerability fixes. To precisely diagnose the causes of fix propagation blocking,Plumbermodels the vulnerability metadata, andnpmdependency metadata and continuously monitors their evolution. By analyzing a full-picture of the ecosystem-level dependency graph and the corresponding fix propagation statuses, it derives remediation schemes for pivotal packages. In the schemes,Plumberprovides customized remediation suggestions with vulnerability impact analysis to arouse package developers’ awareness. We appliedPlumberto generating 268 remediation reports for the identified pivotal packages, to evaluate its remediation effectiveness based on developers’ feedback. Encouragingly, 47.4% our remediation reports received positive feedback from many well-knownnpmprojects, such asTensorflow/tfjs,Ethers.js, andGoogleChrome/workbox. Our reports have boosted the propagation of vulnerability fixes into 16,403 root packages through 92,469 dependency paths. On average, each remediated package version is receiving 72,678 downloads per week by the time of this work.

Android introduces a new permission model that allows apps to request permissions at runtime rather than at the installation time since 6.0 (Marshmallow, API level 23). While this runtime permission model provides users with greater flexibility in controlling an app's access to sensitive data and system features, it brings new challenges to app development. First, as users may grant or revoke permissions at any time while they are using an app, developers need to ensure that the app properly checks and requests required permissions before invoking any permission-protected APIs. Second, Android's permission mechanism keeps evolving and getting customized by device manufacturers. Developers are expected to comprehensively test their apps on different Android versions and device models to make sure permissions are properly requested in all situations. Unfortunately, these requirements are often impractical for developers. In practice, many Android apps suffer from various runtime permission issues (ARP issues). While existing studies have explored ARP issues, the understanding of such issues is still preliminary. To better characterize ARP issues, we performed an empirical study using 135 Stack Overflow posts that discuss ARP issues and 199 real ARP issues archived in popular open-source Android projects on GitHub. Via analyzing the data, we observed 11 types of ARP issues that commonly occur in Android apps. For each type of issues, we systematically studied: (1) how they can be manifested, (2) how pervasive and serious they are in real-world apps, and (3) how they can be fixed. We also analyzed the evolution trend of different types of issues from 2015 to 2020 to understand their impact on the Android ecosystem. Furthermore, we conducted a field survey and in-depth interviews among the practitioners from open-source community and industry, to gain insights from practitioners’ practices and learn their requirements of tools that can help combat ARP issues. Finally, to understand the strengths and weaknesses of the existing tools that can detect ARP issues, we builtARPBench, an open benchmark consisting of 94 real ARP issues, and evaluated the performance of three available tools. The experimental results indicate that the existing tools have very limited supports for detecting our observed issue types and report a large number of false alarms. We further analyzed the tools’ limitations and summarized the challenges of designing an effective ARP issue detection technique. We hope that our findings can shed light on future research and provide useful guidance to practitioners.

Most Android apps lack their counterparts on convenient smart-watch devices, possibly due to non-trivial engineering efforts required in the new app design and code development. Inspired by the observation that widgets on a smartphone can be mirrored to a smartwatch, this paper presents the Jigsaw framework to greatly alleviate such engineering efforts. Particularly, Jigsaw enables a pushbutton development of smartphone's companion watch apps by leveraging the programming by example paradigm, version space algebra, and constraint solving. Our experiments on 16 popular open-source apps validated the effectiveness of our synthesis algorithm, as well as their practical usefulness in synthesizing usable watch companions.

Nowadays applications are getting increasingly attractive by being capable of adapting their behaviors based on their understanding to running environments (a.k.a. contexts). However, such capability can be subject to illness or even unexpected crash, when contexts, for suffering environmental noises, become inaccurate or even conflict with each other. Fortunately, various constraint checking techniques have been proposed to validate contexts against consistency constraints, in order to guard context consistency for applications in a timely manner. However, with the growth of environmental dynamics and context volume, it is getting more and more challenging to check context consistency in time. In this paper, we propose a novel approach, INFuse, to soundly fuse together two lines of techniques, namely, incremental checking and concurrent checking, for efficient constraint checking. Realizing such check fusion has to address the challenges rising from the gap between the micro analysis for reusable elements in incremental checking and the macro collection of parallel tasks in concurrent checking. INFuse solves the challenges by automatically deciding maximal concurrent boundaries for context changes under checking (i.e., what-correctness problem), and soundly fusing incremental and concurrent checking for context consistency (i.e., how-correctness problem), with theoretical guarantees. Our experimental evaluation with real-world data shows that INFuse could improve constraint checking efficiency by 18.6x–171.1x, as compared with existing state-of-the-art techniques.

Adaptive applications rely on conditions about their environments (or contexts) to deliver smart services, e.g., location-aware services. Due to inherent noises in environmental sensing and interpretation, there is an increasing demand for guarding the consistency of contexts to avoid application misbehavior, and at the same time minimizing the guarding cost. Existing work has tried to reduce the cost by speeding up the kernel constraint checking module inside the consistency guarding process. Most efforts have been spent on reusing previous checking results or checking constraints in parallel, while leaving untouched one central problem of link generation, the step that consumes a substantially large part of the total time cost for explaining why constraints have been violated. In this paper, we propose a novel technique, MG, to automatically identify and remove redundant link generation, without harming any checking result. We show that MG is sound (always checking correctly) and complete (removing all redundancy). Our experiments with synthesized and real-world consistency constraints reported that compared with existing work, MG achieved significant efficiency improvements on the link generation (tens to hundreds times speedup), and could reduce the total constraint checking time up to 45.4%.

Cross-device replay for Android apps is challenging because apps have to adapt or even restructure their GUIs responsively upon screen-size or orientation change across devices. As a first exploratory work, this paper demonstrates that cross-device record and replay can be made simple and practical by a one-pass, greedy algorithm by the Rx framework leveraging the least surprise principle in the GUI design. The experimental results of over 1,000 replay settings encouragingly show that our implemented Rx prototype tool effectively solved non-trivial cross-device replay cases beyond any known non-search-based work's scope, and had still competitive capabilities on same-device replay with start-of-the-art techniques.

Non-crashing functional bugs of Android apps can seriously affect user experience. Often buried in rare program paths, such bugs are difficult to detect but lead to severe consequences. Unfortunately, very few automatic functional bug oracles for Android apps exist, and they are all specific to limited types of bugs. In this paper, we introduce a novel technique named deep-state differential analysis, which brings the classical "bugs as deviant behaviors" oracle to Android apps as a generic automatic test oracle. Our oracle utilizes the observations on the execution of automatically generated test inputs that (1) there can be a large number of traces reaching internal app states with similar GUI layouts, and only a small portion of them would reach an erroneous app state, and (2) when performing the same sequence of actions on similar GUI layouts, the outcomes will be limited. Therefore, for each set of test inputs terminating at similar GUI layouts, we manifest comparable app behaviors by appending the same events to these inputs, cluster the manifested behaviors, and identify minorities as possible anomalies. We also calibrate the distribution of these test inputs by a novel input calibration procedure, to ensure the distribution of these test inputs is balanced with rare bug occurrences.

Git, a cross-platform and open source distributed version control tool, provides strong support for non-linear development and is capable of handling everything from small to large projects with speed and efficiency. It has become an indispensable tool for millions of software developers and is the de facto standard of version control in software development nowadays. However, despite its widespread use, developers still frequently face difficulties when using various Git commands to manage projects and collaborate. To better help developers use Git, it is necessary to understand the issues and difficulties that they may encounter when using Git. Unfortunately, this problem has not yet been comprehensively studied. To fill this knowledge gap, in this article, we conduct a large-scale study on Stack Overflow, a popular Q&A forum for developers. We extracted and analyzed 80,370 relevant questions from Stack Overflow, and reported the increasing popularity of the Git command questions. By analyzing the questions, we identified the Git commands that are frequently asked and those that are associated with difficult questions on Stack Overflow to help understand the difficulties developers may encounter when using Git commands. In addition, we conducted a survey to understand how developers learn Git commands in practice, showing that self-learning is the primary learning approach. These findings provide a range of actionable implications for researchers, educators, and developers.

Java projects are often built on top of various third-party libraries. If multiple versions of a library exist on the classpath, JVM will only load one version and shadow the others, which we refer to asdependency conflicts. This would give rise tosemantic conflict(SC) issues, if the library APIs referenced by a project have identical method signatures but inconsistent semantics across the loaded and shadowed versions of libraries. SC issues are difficult for developers to diagnose in practice, since understanding them typically requires domain knowledge. Although adapting the existing test generation technique for dependency conflict issues,Riddle, to detect SC issues is feasible, its effectiveness is greatly compromised. This is mainly becauseRiddlerandomly generates test inputs, while the SC issues typically require specific arguments in the tests to be exposed. To address that, we conducted an empirical study of 316 real SC issues to understand the characteristics of such specific arguments in the test cases that can capture the SC issues. Inspired by our empirical findings, we propose an automated testing techniqueSensor, which synthesizes test cases using ingredients from the project under test to trigger inconsistent behaviors of the APIs with the same signatures in conflicting library versions. Our evaluation results show thatSensoris effective and useful: it achieved a$Precision$of 0.898 and a$Recall$of 0.725 on open-source projects and a$Precision$of 0.821 on industrial projects; it detected 306 semantic conflict issues in 50 projects, 70.4 percent of which had been confirmed as real bugs, and 84.2 percent of the confirmed issues have been fixed quickly.

Image displaying in Android apps is resource-intensive. Improperly displayed images result in performance degradation or even more severe consequences like app crashes. Existing static performance anti-pattern checkers are conservative and limited to a small set of bugs. This paper presents ImMut, the first test augmentation approach to performance testing for image displaying in Android apps to complement these static checkers. Given a functional test case, ImMut mutates it towards a performance test case by either (1) injecting external-source images with large ones or (2) copy-pasting a repeatable fragment and slightly mutating the copies to display many (potentially distinct) images. Evaluation on our prototype implementation showed promising results that ImMut revealed 14 previously unknown performance bugs that are beyond the capability of state-of-the-art static checkers.

Ever since its first release in 2009, the Go programming language (Golang) has been well received by software communities. A major reason for its success is the powerful support of library-based development, where a Golang project can be conveniently built on top of other projects by referencing them as libraries. As Golang evolves, it recommends the use of a new library-referencing mode to overcome the limitations of the original one. While these two library modes are incompatible, both are supported by the Golang ecosystem. The heterogeneous use of library-referencing modes across Golang projects has caused numerous dependency management (DM) issues, incurring reference inconsistencies and even build failures. Motivated by the problem, we conducted an empirical study to characterize the DM issues, understand their root causes, and examine their fixing solutions. Based on our findings, we developed Hero, an automated technique to detect DM issues and suggest proper fixing solutions. We applied Hero to 19,000 popular Golang projects. The results showed that Hero achieved a high detection rate of 98.5% on a DM issue benchmark and found 2,422 new DM issues in 2,356 popular Golang projects. We reported 280 issues, among which 181 (64.6%) issues have been confirmed, and 160 of them (88.4%) have been fixed or are under fixing. Almost all the fixes have adopted our fixing suggestions.

There is an increasing demand for evolving software systems to deliver continuous services of no restart. Dynamic software update (DSU) aims to achieve this goal by patching the system state on the fly but is currently hindered from practice due to non-trivial cross-version object state transformations. This paper revisits this problem through an in-depth empirical study of over 190 class changes from Tomcat 8. The study produced an important finding that most non-trivial object state transformers can be constructed by reassembling existing old/new version code snippets. This paper presents a domain-specific language and an efficient algorithm for synthesizing non-trivial object transformers over code reuse. We experimentally evaluated our tool implementation PASTA with real-world software systems, reporting PASTA's effectiveness in succeeding in 7.5X non-trivial object transformation tasks compared with the best existing DSU techniques.

Control-based approaches to self-adaptive software-intensive systems (SASs) are hailed for their optimal performance and theoretical guarantees on the reliability of adaptation behavior. However, in practice the guarantees are often threatened by model deviations occurred at runtime. In this paper, we propose a Model-guided Deviation Detector (MoD2) for timely and accurate detection of model deviations. To ensure reliability, a SAS can switch a control-based optimal controller for a mandatory controller once an unsafe model deviation is detected. MoD2 achieves both high timeliness and high accuracy through a deliberate fusion of parameter deviation estimation, uncertainty compensation, and safe region quantification. Empirical evaluation with three exemplar systems validated the efficacy of MoD2 (93.3% shorter detection delay, 39.4% lower FN rate, and 25.2% lower FP rate), as well as the benefits of the adaptation-switching mechanism (abnormal rate dropped by 29.2%).

Traditional context-sensitive pointer analysis is hard to scale for large and complex Java programs. To address this issue, a series of selective context-sensitivity approaches have been proposed and exhibit promising results. In this work, we move one step further towards producing highly-precise pointer analyses for hard-to-analyze Java programs by presenting the Unity-Relay framework, which takes selective context sensitivity to the next level. Briefly, Unity-Relay is a one-two punch: given a set of different selective context-sensitivity approaches, say S = S1, . . . , Sn, Unity-Relay first provides a mechanism (called Unity)to combine and maximize the precision of all components of S. When Unity fails to scale, Unity-Relay offers a scheme (called Relay) to pass and accumulate the precision from one approach Si in S to the next, Si+1, leading to an analysis that is more precise than all approaches in S. As a proof-of-concept, we instantiate Unity-Relay into a tool called Baton and extensively evaluate it on a set of hard-to-analyze Java programs, using general precision metrics and popular clients. Compared with the state of the art, Baton achieves the best precision for all metrics and clients for all evaluated programs. The difference in precision is often dramatic — up to 71% of alias pairs reported by previously-best algorithms are found to be spurious and eliminated.

Many applications use contexts to understand their environments and make adaptation. However, contexts are often inaccurate or even conflicting with each other (a.k.a. context inconsistency). To prevent applications from behaving abnormally or even failing, one promising approach is to deploy constraint checking to detect context inconsistencies. A variety of constraint checking techniques have been proposed, based on different incremental or parallel mechanisms for the efficiency. They are commonly deployed with the strategy that schedules constraint checking immediately upon context changes. This assures no missed inconsistency, but also limits the detection efficiency. One may break the limit by grouping context changes for checking together, but this can cause severe inconsistency missing problem (up to 79.2 percent). In this article, we propose a novel strategy GEAS to isolate latent interferences among context changes and schedule constraint checking with adaptive group sizes. This makes GEAS not only improve the detection efficiency, but also assure no missed inconsistency with theoretical guarantee. We experimentally evaluated GEAS with large-volume real-world context data. The results show that GEAS achieved significant efficiency gains for context inconsistency detection by 38.8-566.7 percent (or 1.4x-6.7x). When enhanced with an extended change-cancellation optimization, the gains were up to 2,755.9 percent (or 28.6x).

Generating high-quality system call sequences is not only important to testing file system implementations, but also challenging due to the astronomically large input space. This paper introduces a new approach to the workload generation problem by building layered models and abstract workloads refinement. This approach is instantiated as a three-layer file system model for file system workload generation. In a short-period experiment run, sequential workloads (system call sequences) manifested over a thousand crashes in mainline Linux Kernel file systems, with 12 previously unknown bugs being reported. We also provide evidence that such workloads benefit other domain-specific testing techniques including crash consistency testing and concurrency testing.

Deep learning (DL) applications are becoming increasingly popular. Their reliabilities largely depend on the performance of DL models integrated in these applications as a central classifying module. Traditional techniques need to retrain the models or rebuild and redeploy the applications for coping with unexpected conditions beyond the models' handling capabilities. In this paper, we take a fault tolerance approach, Dissector, to distinguishing those inputs that represent unexpected conditions (beyond-inputs) from normal inputs that are still within the models' handling capabilities (within-inputs), thus keeping the applications still function with expected reliabilities. The key insight of Dissector is that a DL model should interpret a within-input with increasing confidence, while a beyond-input would probably cause confused guesses in the prediction process. Dissector works in an application-specific way, adaptive to DL models used in applications, and extremely efficiently, scalable to large-size datasets from complex scenarios. The experimental evaluation shows that Dissector outperformed state-of-the-art techniques in the effectiveness (AUC: avg. 0.8935 and up to 0.9894) and efficiency (runtime overhead: only 3.3--5.8 milliseconds). Besides, it also exhibited encouraging usefulness in defensing against adversarial inputs (AUC: avg. 0.9983) and improving a DL model's actual accuracy in use (up to 16% for CIFAR-100 and 20% for ImageNet).

Android apps demand high-quality test inputs, whose generation remains an open challenge. Existing techniques fall short on exploring complex app functionalities reachable only by a long, meaningful, and effective test input. Observing that such test inputs can usually be decomposed into relatively independent short use cases, this paper presents ComboDroid, a fundamentally different Android app testing framework. ComboDroid obtains use cases for manifesting a specific app functionality (either manually provided or automatically extracted), and systematically enumerates the combinations of use cases, yielding high-quality test inputs.

The PyPI ecosystem has indexed millions of Python libraries to allow developers to automatically download and install dependencies of their projects based on the specified version constraints. Despite the convenience brought by automation, version constraints in Python projects can easily conflict, resulting in build failures. We refer to such conflicts as Dependency Confict (DC) issues. Although DC issues are common in Python projects, developers lack tool support to gain a comprehensive knowledge for diagnosing the root causes of these issues. In this paper, we conducted an empirical study on 235 real-world DC issues. We studied the manifestation patterns and fixing strategies of these issues and found several key factors that can lead to DC issues and their regressions. Based on our findings, we designed and implemented Watchman, a technique to continuously monitor dependency conflicts for the PyPI ecosystem. In our evaluation, Watchman analyzed PyPI snapshots between 11 Jul 2019 and 16 Aug 2019, and found 117 potential DC issues. We reported these issues to the developers of the corresponding projects. So far, 63 issues have been confirmed, 38 of which have been quickly fixed by applying our suggested patches.

Context-Aware Systems (a.k.a. CASs) integrate cyber and physical space to provide context-aware adaptive functionalities. Building context-aware systems is challenging due to the uncertainty of the real physical environment. Therefore, input validation for context-aware systems plays a significant role in keeping the systems executing safely. Input validation approaches have been proposed to monitor and guard the executions of context-aware systems. However, few of these works (17%, 2 out of 12) evaluated their approaches with a real context-aware system in a real physical environment. In this paper, we study and compare the effectiveness of input validation approaches for context-aware system in both a simulated and a physical environment. We built a testing platform, RM-Testing, based on DJI RoboMaster S1 robot car. We implemented three up-to-date input validation approaches, and evaluated their effectiveness in improving the success rate of the robot car’s executions. The results show that the selected input validation approaches are effective in guarantee the safe execution of context-aware systems, which improve the success rate by 82% in the simulated environment, and 50% in the physical environment. However, the effectiveness of these approaches does vary in different environment. Thus, we believe that such CASs-based input validation works should be evaluated in the physical environment to better validate their effectiveness and usefulness.

Trained DNN models are increasingly adopted as integral parts of software systems, but they often perform deficiently in the field. A particularly damaging problem is that DNN models often give false predictions with high confidence, due to the unavoidable slight divergences between operation data and training data. To minimize the loss caused by inaccurate confidence, operational calibration, i.e., calibrating the confidence function of a DNN classifier against its operation domain, becomes a necessary debugging step in the engineering of the whole system.

Cyber-physical software delivers context-aware services through continually interacting with its physical environment and adapting to the changing surroundings. However, when the software's assumptions on the environment no longer hold, the interactions can introduce errors for leading to unexpected behaviors and even system failures. One promising solution to this problem is to conduct runtime monitoring of invariants. Violated invariants reflect latent erroneous states (i.e., abnormal states that could lead to failures). In turn, monitoring when program executions violate the invariants can allow the software to take alternative measures to avoid danger. In this article, we present context-based Multiinvariant detection (CoMID), an approach that automatically infers invariants and detects abnormal states for cyber-physical programs. CoMID consists of two novel techniques, namely context-based trace grouping and multiinvariant detection. The former infers contexts to distinguish different effective scopes for CoMID's derived invariants, and the latter conducts ensemble evaluation of multiple invariants to detect abnormal states during runtime monitoring. We evaluate CoMID on real-world cyber-physical software. The results show that CoMID achieves a 5.7-28.2% higher true-positive rate and a 6.8-37.6% lower false-positive rate in detecting abnormal states, as compared with the existing approaches. When deployed in field tests, CoMID's runtime monitoring improves the success rate of cyber-physical software in its task executions by 15.3-31.7%.

Software systems assisted with deep neural networks (DNNs) are gaining increasing popularities. However, one outstanding problem is to judge whether a given application scenario suits a DNN model, whose answer highly affects its concerned system's performance. Existing work indirectly addressed this problem by seeking for higher test coverage or generating adversarial inputs. One pioneering work is SynEva, which exactly addressed this problem by synthesizing mirror programs for scenario suitableness evaluation of general machine learning programs, but fell short in supporting DNN models. In this paper, we propose VISION to eValuatIng Scenario suItableness fOr DNN models, specially catered for DNN characteristics. We conducted experiments on a real-world self-driving dataset Udacity, and the results show that VISION was effective in evaluating scenario suitableness for DNN models with an accuracy of 75.6-89.0% as compared to that of SynEva, 50.0-81.8%. We also explored different meta-models in VISION, and found out that the decision tree logic learner meta-model could be the best one for balancing VISION's effectiveness and efficiency.

This paper introduces a new, fully automated modelbased approach for effective testing of Android apps. Different from existing model-based approaches that guide testing with a static GUI model (i.e., the model does not evolve its abstraction during testing, and is thus often imprecise), our approach dynamically optimizes the model by leveraging the runtime information during testing. This capability of model evolution significantly improves model precision, and thus dramatically enhances the testing effectiveness compared to existing approaches, which our evaluation confirms.We have realized our technique in a practical tool, APE. On 15 large, widely-used apps from the Google Play Store, APE outperforms the state-of-the-art Android GUI testing tools in terms of both testing coverage and the number of detected unique crashes. To further demonstrate APE's effectiveness and usability, we conduct another evaluation of APE on 1,316 popular apps, where it found 537 unique crashes. Out of the 38 reported crashes, 13 have been fixed and 5 have been confirmed.

Spreadsheets are widely used but subject to various defects. In this paper, we present SGuard to effectively detect spreadsheet defects. SGuard learns spreadsheet features to cluster cells with similar computational semantics, and then refines these clusters to recognize anomalous cells as defects. SGuard well balances the trade-off between the precision (87.8%) and recall rate (71.9%) in the defect detection, and achieves an F-measure of 0.79, exceeding existing spreadsheet defect detection techniques. We introduce the SGuard implementation and its usage by a video presentation (https://youtu.be/gNPmMvQVf5Q), and provide its public download repository (https://github.com/sheetguard/sguard).

Spreadsheets are widely used, but subject to various defects and severe consequences due to poor maintenance by end users. Existing spreadsheet defect detection techniques fall short of effectiveness, either due to limited scopes or relying on rigid patterns. In this paper, we discuss and improve one state-of-the-art technique, CUSTODES, which uses cell clustering and anomaly detection to extend its scope and make its patterns adaptive to varying spreadsheet styles, but is prone to fragile clustering when involving irrelevant cells, leading to a largely reduced detection precision. We present WARDER to refine CUSTODES's cell clustering based on validity properties, and experimental results show that WARDER improves the precision by 20.7% on average or reach 100% for 79.8% worksheets on cell clustering, which contributes to a precision improvement of 23.1% for defect detection. WARDER also exhibits satisfactory results, against other spreadsheet defect detection techniques, and on another large-scale spreadsheet corpus VEnron2.

With the increasing adoption of Deep Neural Network (DNN) models as integral parts of software systems, efficient operational testing of DNNs is much in demand to ensure these models' actual performance in field conditions. A challenge is that the testing often needs to produce precise results with a very limited budget for labeling data collected in field.

Mobile applications (apps for short) often need to display images. However, inefficient image displaying (IID) issues are pervasive in mobile apps, and can severely impact app performance and user experience. This paper presents an empirical study of 162 real-world IID issues collected from 243 popular open-source Android apps, validating the presence and severity of IID issues, and then sheds light on these issues' characteristics to support future research on effective issue detection. Based on the findings of this study, we developed a static IID issue detection tool TAPIR and evaluated it with real-world Android apps. The experimental evaluations show encouraging results: TAPIR detected 43 previously-unknown IID issues in the latest version of the 243 apps, 16 of which have been confirmed by respective developers and 13 have been fixed.

Android fragmentation is a double-edged sword of the Android ecosystem. On the one hand, it promotes Android's prevalence. On the other hand, the numerous combinations of various system versions, customized features, system drivers, and device models make it infeasible, if not impossible, for developers to exhaustively test their apps for potential compatibility issues. Previous research has proposed promising techniques for detecting these issues. However, they suffer from severe false positive problems due to their lack of third-party library detection or imprecise program analysis. In this paper, we present ELEGANT, an automated tool to effectively detect and locate fragmentation-induced compatibility issues for Android apps. ELEGANT exploits whitelist-enhanced or obfuscation-insensitive techniques to detect and alleviate the impact of third-party libraries on the analysis precision, and uses a three-step static detection algorithm to increase the precision of its program analysis. We experimentally evaluated ELEGANT with 22 real-world popular Android apps. The experimental results confirmed ELEGANT's effectiveness on detecting and locating Android fragmentation-induced compatibility issues, as well as realizing an impressive reduction on false positives by around 70%.

Dynamic software updating (DSU) is a technique to upgrade a running software system on the fly without stopping the system. During updating, the runtime state of the modified components of the system needs to be properly transformed into a new state, so that the modified components can still correctly interact with the rest of the system. However, the transformation is non-trivial to realize due to the gap between the low-level implementations of two versions of a program. This paper presents AOTES, a novel approach to automating object transformations for dynamic updating of Java programs. AOTES bridges the gap by abstracting the old state of an object to a history of method invocations, and re-invoking the new version of all methods in the history to get the desired new state. AOTES requires no instrumentation to record any data and thus has no overhead during normal execution. We propose and implement a novel technique that can synthesize an equivalent history of method invocations based on the current object state only. We evaluated AOTES on software updates taken from Apache Commons Collections, Tomcat, FTP Server and SSHD Server. Experimental results show that AOTES successfully handled 51 of 61 object transformations of 21 updated classes, while two state-of-the-art approaches only handled 11 and 6 of 61, respectively.

With the rapid development of mobile devices, Android applications (apps) are universally used. However, attackers repackage Android apps and release them to the markets for illegal purposes, which brings great threats to the Android ecosystem. To leverage the popularity of original apps, they keep similar software behaviors to confuse app users. Furthermore, repackaged apps can be obfuscated or encrypted to avoid being detected. Besides, hybrid mobile apps, built by combining web technology and native elements, are becoming a preferred choice for developers. The structure of hybrid apps differs a lot from that of native apps which would raise great challenges to repackaging detection. Existing works still have some limitations in detecting repackaging from obfuscated and encrypted apps. Besides, few of them can deal with hybrid apps. In this paper, we proposed an approach based on the app UI regions extracted from app's runtime UI traces. We also implement a tool named RegionDroid based on the approach. We apply RegionDroid to tree datasets with totally 369 apps. It successfully finds all the 98 obfuscated or encrypted repackaged pairs in dataset S1. It also shows good credibility in distinguishing another 114 commercial apps in dataset S2. We also test our approach in dataset S3with 157 hybrid apps by comparing them pairwisely and the false positive rate is 0.016%.

Services are widely used in Android apps. However, services may leak such that they are no longer used but cannot be recycled by the Garbage Collector. Service leaks may cause an app to misbehave, and are vulnerable to malicious external apps when the service is exported or it is accessible through other exported services. In this paper, we present LESDroid for exported service leaks detection. LESDroid automatically generates service instances and workloads (start/stop or bind/unbind of exported services) of the app under test, and applies a designated oracle to the heap snapshot for service leak detection. We evaluated LESDroid using 375 commercial apps, and found 97 leaked services and 98 distinct leak entries in 70 apps.

Regular expression (regex) with modern extensions is one of the most popular string processing tools. However, poorly-designed regexes can yield exponentially many matching steps, and lead to regex Denial-of-Service (ReDoS) attacks under well-conceived string inputs. This paper presents Rescue, a three-phase gray-box analytical technique, to automatically generate ReDoS strings to highlight vulnerabilities of given regexes. Rescue systematically seeds (by a genetic search), incubates (by another genetic search), and finally pumps (by a regex-dedicated algorithm) for generating strings with maximized search time. We implemenmted the Rescue tool and evaluated it against 29,088 practical regexes in real-world projects. The evaluation results show that Rescue found 49% more attack strings compared with the best existing technique, and applying Rescue to popular GitHub projects discovered ten previously unknown ReDoS vulnerabilities.

Nowadays statistical machine learning is widely adopted in various domains such as data mining, image recognition and automated driving. However, software quality assurance for machine learning is still in its infancy. While recent efforts have been put into improving the quality of training data and trained models, this paper focuses on code-level bugs in the implementations of machine learning algorithms. In this explorative study we simulated program bugs by mutating Weka implementations of several classification algorithms. We observed that 8%-40% of the logically non-equivalent executable mutants were statistically indistinguishable from their golden versions. Moreover, other 15%-36% of the mutants were stubborn, as they performed not significantly worse than a reference classifier on at least one natural data set. We also experimented with several approaches to killing those stubborn mutants. Preliminary results indicate that bugs in machine learning code may have negative impacts on statistical properties such as robustness and learning curves, but they could be very difficult to detect, due to the lack of effective oracles.

Machine learning (ML) programs are being widely used in various human-related applications. However, their testing always remains to be a challenging problem, and one can hardly decide whether and how the existing knowledge extracted from training scenarios suit new scenarios. Existing approaches typically have restricted usages due to their assumptions on the availability of an oracle, comparable implementation, or manual inspection efforts. We solve this problem by proposing a novel program synthesis based approach, SynEva, that can systematically construct an oracle-alike mirror program for similarity measurement, and automatically compare it with the existing knowledge on new scenarios to decide how the knowledge suits the new scenarios. SynEva is lightweight and fully automated. Our experimental evaluation with real-world data sets validates SynEva's effectiveness by strong correlation and little overhead results. We expect that SynEva can apply to, and help evaluate, more ML programs for new scenarios.

A multithreaded program's interleaving space is discrete and astronomically large, making effectively sampling thread schedules for manifesting concurrency bugs a challenging task. Observing that concurrency bugs can be manifested by adjusting thread relative speeds, this paper presents the new concept of speed space in which each vector denotes a family of thread schedules. A multithreaded program's speed space is approximately continuous, easy-to-sample, and preserves certain categories of concurrency bugs. We discuss the design, implementation, and evaluation of our speed-controlled scheduler for exploring adversarial/abnormal schedules. The experimental results confirm that our technique is effective in sampling diverse schedules. Our implementation also found previously unknown concurrency bugs in real-world multithreaded programs.

Cyber-Physical Systems (CPS) intrinsically combine hardware and physical systems with software and network, which are together creating complex and correlated interactions. CPS applications often experience uncertainty in interacting with environment through unreliable sensors. They can be faulty and exhibit runtime errors if developers have not considered environmental interaction uncertainty adequately. Existing work in verifying CPS applications ignores interaction uncertainty and thus may overlook uncertainty-related faults. To improve verification accuracy, in this article we propose a novel approach to verifying CPS applications with explicit modeling of uncertainty arisen in the interaction between them and the environment. Our approach builds an Interactive State Machine network for a CPS application and models interaction uncertainty by error ranges and distributions. Then it encodes both the application and uncertainty models to Satisfiability Modulo Theories (SMT) formula to leverage SMT solvers searching for counterexamples that represent application failures. The precision of uncertainty model can affect the verification results. However, it may be difficult to model interaction uncertainty precisely enough at the beginning, because of the uncontrollable noise of sensors and insufficient data sample size. To further improve the accuracy of the verification results, we propose an approach to identifying and calibrating imprecise uncertainty models. We exploit the inconsistency between the counterexamples’ estimate and actual occurrence probabilities to identify possible imprecision in uncertainty models, and the calibration of imprecise models is to minimize the inconsistency, which is reduced to a Search-Based Software Engineering problem. We experimentally evaluated our verification and calibration approaches with real-world CPS applications, and the experimental results confirmed their effectiveness and efficiency.

Context-aware applications adapt their behavior based on collected contexts. However, contexts can be inaccurate due to sensing noise, which might cause applications to misbehave. One promising approach is to check contexts against consistency constraints at runtime, so as to detect context inconsistencies for applications and resolve them in time. The checking is typically immediate upon each collected context change. Such a scheduling strategy is intuitive for avoiding missing context inconsistencies in the detection, but may cause low-efficiency problems for heavy-workload checking scenarios, even if equipped with existing incremental or parallel constraint checking techniques. One may choose to check contexts in a batch way to increase the efficiency by reducing the number of constraint checking. However, this can easily cause missed context inconsistencies, denying the purpose of inconsistency detection. In this paper, we propose a novel scheduling strategy GEAS of two nice properties: (1) adaptively tuning the batch window to avoid missing any context inconsistency; (2) generic to checking techniques with no or little adjustment. We experimentally evaluated GEAS against the immediate strategy with existing constraint checking techniques. The experimental results show that GEAS achieved 143-645% efficiency improvement without missing any context inconsistency, while alternatives caused 39.2-65.3% loss of detected context inconsistencies.

Many smartphone applications suffer from energy inefficiency problems, but locating these problems is quite difficult and labor-intensive. Automated tools for detecting energy inefficiency bugs have been shown to be effective. Existing approaches generally consist of two parts, namely the simulation part and the monitor part. The simulation part explores an application's state space guided by an application execution model, and the monitor part checks for occurrences of energy inefficiency patterns. However, existing approaches might miss energy inefficiency bugs due to their imprecise application execution models and oversimplified energy inefficiency diagnosis policies. In this paper, we proposed NavyDroid, an approach to diagnosing energy inefficiency problems more effectively. We summarized a comprehensive application execution model from Android specifications and expressed it as a state machine. By considering multiple patterns of wake lock misuses, our approach is able to detect more complex energy bugs caused by wake lock misuses. We implemented NavyDroidon top of Java Pathfinder (JPF) and applied it to real-world applications. We evaluated NavyDroid with 17 real-world Android applications, and NavyDroid located more energy inefficiency bugs in these applications than the existing work E-GreenDroid did. The results of our experiments demonstrate that our approach can effectively locate real energy inefficiency bugs in Android applications, suggesting its effectiveness.

In recent years, with the explosive growth of mobile smart phonesnes, the number of Android applications (apps) increases rapidly. Attackers usually leverage the popumobile smart phoneslarity of Android apps by inserting malwares, modifying the original apps, repackaging and releasing them for their own illegal purposes. To avoid repackaged apps from being detected, they usually use sorts of obfuscation and encryption tools. As a result, it's important to detect which apps are repackaged. People often intuitively judge whether two apps are a repackaged pair by executing them and observing their runtime user interface (UI) traces. Hence, we propose layout group graph (LGG) built from UI trances to model those UI behaviors and use LGG as the birthmark of Android apps for identification. Based on LGG, we also implement a dynamic repackaging detection tool, RepDroid. Since our method does not require the apps' source code, it is resilient to app obfuscation and encryption. We conducted an experiment with two data sets. The first set contains 98 pairs of repackaged apps. The original apps and repackaged ones are compared and we can detect all of these repackaged pairs. The second set contains 125 commercial apps. We compared them pair-wisely and the false positive rate was 0.08%.

Spreadsheets are widely used by end users for numerical computation in their business. Spreadsheet cells whose computation is subject to the same semantics are often clustered in a row or column as a cell array. When a spreadsheet evolves, the cells in a cell array can degenerate due to ad hoc modifications. Such degenerated cell arrays no longer keep cells prescribing the same computational semantics, and are said to exhibit ambiguous computation smells. We propose CACheck, a novel technique that automatically detects and repairs smelly cell arrays by recovering their intended computational semantics. Our empirical study on the EUSES and Enron corpora finds that such smelly cell arrays are common. Our study also suggests that CACheck is useful for detecting and repairing real spreadsheet problems caused by smelly cell arrays. Compared with our previous work AmCheck, CACheck detects smelly cell arrays with higher precision and recall rate.

Dynamic software updating (DSU) is a technique that can update running software systems without stopping them. Most existing approaches require programmer participation to guarantee the correctness of dynamic updating. However, manually preparing dynamic updating is error-prone and time-consuming. Therefore, other approaches prefer to aggressively perform updating without programmer intervention, which may definitely lead to unanticipated runtime errors. To reduce human effort and enhance the reliability for dynamic updating, we leverage automatic runtime recovery (ARR) techniques to recover runtime errors caused by improper dynamic updating. This paper presents ADSU, a fully automatic DSU system using ARR. We evaluate ADSU with real updates from widely used open source software systems, i.e., Apache Tomcat, Apache FTP Server and jEdit. The preliminary results have shown that ADSU succeeds in automatically applying 11 of 16 real-world updates that existing counterparts cannot.

Smartphones are indispensable in people's daily lives. As smartphone apps are being increasingly concurrent, developers are increasingly unable to tackle the complexity and to avoid subtle concurrency bugs. To better address this issue, we propose a novel approach to manifesting concurrency bugs in Android apps based on the fact that one can simultaneously generate input events and their schedules for an app. We conduct static-dynamic hybrid analysis to find potentially conflicting resource accesses in an app. The app is then automatically pressure-tested by guided event and schedule generation. We implemented the prototype tool AATT and evaluated it over thirteen popular real-world open-source apps. AATT successfully found 9 concurrency bugs out of which 7 were previously unknown.

Mobile applications (apps) are mostly driven by touch gestures whose interactions are natural to human beings. However, generating gesture events for effective and efficient testing of such apps remains to be a challenge. Existing event generation techniques either feed the apps under test with random gestures or exhaustively enumerate all possible gestures. While the former strategy leads to incomplete test coverage, the latter suffers from efficiency issues. In this paper, we study the particular problem of gesture event generation for Android apps. We present a static analysis technique to obtain the gesture information: each UI component's potentially relevant gestures, so as to reduce the amount of gesture events to be delivered in the automated testing. We implemented our technique as a prototype tool GAT and evaluated it with real-world Android apps. The experimental results show that GAT is both effective and efficient in covering more code as well as detecting gesturerelated bugs.

Dynamic software updating (DSU) aims to patch software for fixing bugs or adding functions while it is running. Before update, developers need to make a dynamic patch ready, which includes update points, state transformers and a corresponding code patch. Existing practice mostly assumes manual preparation of dynamic patches, but this process can be both time-consuming and error-prone. Some pioneer work attempts to automate this process, but cannot guarantee the generation of safe dynamic patches for most updates. This paper presents a novel approach CURE to automatically generating safe dynamic patches. CURE takes two versions of software and their test cases as input, and automatically synthesizes state transformers and selects update points. We applied CURE to 28 updates for three real-world server software. The experimental results show that CURE generated safe dynamic patches automatically and their corresponding updates achieved an 88.7% success rate, as compared to 74.3% for TOS and 61.2% for default patches.

Various techniques have been proposed to detect smells in spreadsheets, which are susceptible to errors. These techniques typically detect spreadsheet smells through a mechanism based on a fixed set of patterns or metric thresholds. Unlike conventional programs, tabulation styles vary greatly across spreadsheets. Smell detection based on fixed patterns or metric thresholds, which are insensitive to the varying tabulation styles, can miss many smells in one spreadsheet while reporting many spurious smells in another. In this paper, we propose CUSTODES to effectively cluster spreadsheet cells and detect smells in these clusters. The clustering mechanism can automatically adapt to the tabulation styles of each spreadsheet using strong and weak features. These strong and weak features capture the invariant and variant parts of tabulation styles, respectively. As smelly cells in a spreadsheet normally occur in minority, they can be mechanically detected as clusters' outliers in feature spaces. We implemented and applied CUSTODES to 70 spreadsheets files randomly sampled from the EUSES corpus. These spreadsheets contain 1,610 formula cell clusters. Experimental results confirmed that CUSTODES is effective. It successfully detected harmful smells that can induce computation anomalies in spreadsheets with an F-measure of 0.72, outperforming state-of-the-art techniques.

Energy inefficiency of smartphone apps is one of the important non-functional issues. It is common, but difficult to diagnose, and often involves sensor usage. GreenDroid provides a novel approach to systematically diagnose energy inefficiency problems in smartphone apps running on Android platforms. It derives an application execution model (AEM) from Android framework and leverages it to realistically simulate an application's runtime behaviors. It also automatically analyzes an application's sensory data utilization, monitors sensor listener and wake lock usage, and reports actionable information to developers.

Controllers restrict systems to behave only in good manners. Different from controlling monolithic systems where controllers can be automatically synthesized from specifications, controlling distributed systems often has to use distributed controllers that are manually programmed. To ensure their correctness, manually programmed controllers themselves need to be formally verified. This task can be challenging due to the complexity caused by the autonomy and asynchrony of distributed controllers. The limited scalability of existing model checkers also exacerbates the problem. In this paper we explore the modeling and verification of distributed controllers using Alloy. Besides resorting to the Small Scopes Hypothesis of the Alloy methodology, we also leverage local invariant based modular verification techniques for better scalability. A local invariant characterizes a logical relationship between a local sub-system and its neighbors and abstracts away the concrete interactions. These concrete interactions would otherwise explode the system state space during verification. The approach is first illustrated with the well-understood Two-Phase Commit protocol, and then is applied to the verification of several dynamic software update protocols, which gives an initial evidence of its effectiveness.

Combinatorial testing detects faults by trying different value combinations for program inputs. Traditional combinatorial testing treats programs as black box and focuses on manipulating program inputs (named input-based combinatorial testing or ICT). In this paper, we explore the possibility of conducting combinatorial testing via white-box branch information. Similarly, different combinations of branches taken in an execution are tried to test whether they help detect faults and to what extent. We name this technique branch-based combinatorial testing (BCT). We propose ways to address challenges in realizing BCT, and evaluate BCT with Java programs. The results reported that BCT can effectively detect faults even with low-level combinations, say 3-4 ways, which suggest it to be a strong test adequacy criterion. We also found that our greedy strategy for minimizing test suites reduces over 50% tests for reaching certain way levels, and merging nested branches detects faults more cost-effectively than considering them separately.

Software should behave correctly even in adverse conditions. Particularly, we study the problem of automated validation of crash consistency, i.e., file system data safety when systems crash. Existing work requires non-trivial manual efforts of specifying checking scripts and workloads, which is an obstacle for software developers. Therefore, we propose C3, a novel approach that makes crash consistency validation as easy as pressing a single button. With a program and an input, C3 automatically reports inconsistent crash sites. C3 not only exempts developers from the need of writing crash site checking scripts (by an algorithm that computes editing distance between file system snapshots) but also reduces the reliance on dedicated workloads (by test amplification). We implemented C3 as an open-source tool. With C3, we found 14 bugs in open-source software that have severe consequences at crash and 11 of them were previously unknown to the developers, including in highly mature software (e.g., GNU zip and GNU coreutils sort) and popular ones being actively developed (e.g., Adobe Brackets and TeXstudio).

Order of shared memory accesses, known as the shared memory dependence, is the cornerstone of dynamic analyses of concurrent programs. In this paper, we study the problem of reducing shared memory dependences. We present the first online software-only algorithm to reduce shared memory dependences without vector clock maintenance, opening a new direction to a broad range of applications (e.g., deterministic replay and data race detection). Our algorithm exploits a simple yet effective observation, that adaptive variable grouping can recognize and match spatial locality in shared memory accesses, to reduce shared memory dependences. We designed and implemented the bisectional coordination protocol, which dynamically maintains a partition of the program's address space without its prior knowledge, such that shared variables in each partitioned interval have consistent thread and spatial locality properties. Evaluation on a set of real-world programs showed that by paying a 0--54.7% (median 21%) slowdown, bisectional coordination reduced 0.95--97% (median 55%) and 16--99.99% (median 99%) shared memory dependences compared with RWTrace and LEAP, respectively.

Spreadsheets are widely used by end users for various business tasks, such as data analysis and financial reporting. End users may perform similar tasks by cloning a block of cells (table) in their spreadsheets. The corresponding cells in these cloned tables are supposed to keep the same or similar computational semantics. However, when spreadsheets evolve, thus cloned tables can become inconsistent due to ad-hoc modifications, and as a result suffer from smells. In this paper, we propose TableCheck to detect table clones and related smells due to inconsistency among them. We observe that two tables with the same header information at their corresponding cells are likely to be table clones. Inspired by existing fingerprint-based code clone detection techniques, we developed a detection algorithm to detect this kind of table clones. We further detected outliers among corresponding cells as smells in the detected table clones. We implemented our idea into TableCheck, and applied it to real-world spreadsheets from the EUSES corpus. Experimental results show that table clones commonly exist (21.8%), and 25.6% of the spreadsheets with table clones suffer from smells due to inconsistency among these clones. TableCheck detected table clones and their smells with a precision of 92.2% and 85.5%, respectively, while existing techniques detected no more than 35.6% true smells that TableCheck could detect.

Wake locks are widely used in Android apps to protect critical computations from being disrupted by device sleeping. Inappropriate use of wake locks often seriously impacts user experience. However, little is known on how wake locks are used in real-world Android apps and the impact of their misuses. To bridge the gap, we conducted a large-scale empirical study on 44,736 commercial and 31 open-source Android apps. By automated program analysis and manual investigation, we observed (1) common program points where wake locks are acquired and released, (2) 13 types of critical computational tasks that are often protected by wake locks, and (3) eight patterns of wake lock misuses that commonly cause functional and non-functional issues, only three of which had been studied by existing work. Based on our findings, we designed a static analysis technique, Elite, to detect two most common patterns of wake lock misuses. Our experiments on real-world subjects showed that Elite is effective and can outperform two state-of-the-art techniques.

Software building is recurring and time-consuming. Based on the finding that a significant portion of compilations in incremental build is unnecessary, we propose by path compilation, an efficient build technique that avoids unnecessary recompilation with automated detection of redundant dependencies and unessential changes in source files. The technique is lightweight and transparent to software developers, and can be easily applied to existing build systems. We evaluated our approach on a set of real-world open source projects. The results show that 83% ~ 97% of the recompilations are unnecessary and our approach can accelerate the incremental build up to 44.20%.

Debugging is challenging and labor-intensive. Debugging programs with weak or no oracle is even more difficult due to lack of passing and failing test runs as well as their comparisons. To address these challenges, we exploit metamorphic relations to construct new programs that are enhanced with synthesized oracle, and combine concolic testing and branch-switching debugging to localize potentially faulty places in original programs. We name our approach concolic metamorphic debugging (or Comedy for short). We experimentally evaluated Comedy with real-world Java programs. The experimental results reported that Comedy successfully generated debugging report for 88.4% of 2,330 faulty programs. The average branch distance between the reported locations and the real fault places is only 1.68. Besides, 36% of the debugging reports precisely locate the fault.

Smartphone applications are becoming increasingly popular. However, these applications can suffer limited power budgets or malfunctioned sensing issues from their host devices. Computation offloading addresses this issue by delegating local computation workloads to remote servers. In this paper, we present Cose Droid, a framework that supports dynamic computation- and sensing-offloading across different Android mobile devices. This enables Android applications to virtually "borrow" computation or sensing resources from other devices. We experimentally evaluated Cose Droid with real-world Android applications. The experimental results confirmed Cose Droid's effectiveness in on-demand offloading, as well as supporting sensor variety and spontaneous sensing recovery.

Mobile apps are prevalent in everyone's daily life. However, apps are oftentimes defective, undermining their convenience, and therefore automated testing and analysis of apps are developed to enhance apps' quality. As these advanced technologies become increasingly effective and complicated, prototyping such a tool also becomes a challenge. To facilitate easy development of high-quality testing and analysis tools that work with real-world apps, we in this paper present the design and implementation of ATT (Android Testing Toolkit), for crafting reusable and scalable testing and analysis on Android apps. ATT consists of integrated tools and APIs for event generation, profiling and program instrumentation, and can be distributed over cloud platforms for scalable testing and analysis. We qualitatively evaluated the applicability of ATT by demonstrating implementation of a series of existing and enhanced work (RERAN, Monkey+ and UGA) upon ATT, and quantitatively studied the scalability of parallelized UGA on a cloud platform with five real-world apps. We believe that our ATT tool would facilitate development of more advanced testing and analysis approaches for Android apps.

Inter-thread shared memory dependences are crucial to understanding the behavior of concurrent systems, as such dependences are the cornerstone of time-travel debugging and further predictive trace analyses. To enable effective and efficient shared memory dependence tracing, we present an optimistic scheme addressing the challenge of capturing exact dependences between unsynchronized events to reduce the probe effect of program instrumentation. Specifically, our approach achieved a wait-free fast path for thread-local reads on x86-TSO relaxed memory systems, and simultaneously achieved precise tracing of exact read-after-write, write-after-write and write-after-read dependences on the fly. We implemented an open-source RWTrace tool, and evaluation results show that our approach not only achieves efficient shared memory dependence tracing, but also scales well on a multi-core computer system.

Dynamic Software Update (DSU) is a technique to upgrade running programs without shutting them down. DSU can improve system availability and maintenance flexibility. However, its adoption in practice is still limited due to the risk of system misbehavior that careless DSU may bring. To reduce this risk we propose a formal framework for the specification and verification of DSU. Different from previous approaches where DSU is described from the viewpoint of program's internal state transitions, our framework focuses on program's external behavior and its effect on its environment. This more abstract view avoids over specification of DSU and allows for better DSU flexibility. Based on this framework, we also devise a mechanism that automatically synthesizes runtime monitors to improve DSU timeliness without compromising its safety.

Context-aware applications adapt their behavior based on contexts. Contexts can, however, be incorrect. A popular means to build dependable applications is to augment them with a set of constraints to govern the consistency of context values. These constraints are evaluated upon context changes to detect inconsistencies so that they can be timely handled. However, we observe that many context inconsistencies are unstable. They vanish by themselves and do not require handling. Such inconsistencies are detected due to misaligned sensor sampling or improper inconsistency detection scheduling. We call them unstable context inconsistencies (or STINs). STINs should be avoided to prevent unnecessary inconsistency handling and unstable behavioral adaptation to applications. In this article, we study STINs systematically, from examples to theoretical analysis, and present algorithms to suppress their detection. Our key insight is that only certain patterns of context changes can make a consistency constraint subject to the detection of STINs. We derive such patterns and proactively use them to suppress the detection of STINs. We implemented our idea and applied it to real-world applications. Experimental results confirmed its effectiveness in suppressing the detection of numerous STINs with negligible overhead, while preserving the detection of stable context inconsistencies that require inconsistency handling.

Mobile devices are gradually taking over traditional computers' dominance in human lives. With the ever-increasing shipment of mobile apps running on these devices, their quality issues become a severe challenge. Although automated testing techniques are being widely studied, they mostly fall short of handling mobile apps' complex interactions, e.g., A finger swipe or device shaking gesture, leading to inadequate testing. In this paper, we present a novel User Guided Automation (UGA) technique to address testing challenges incurred by such complex interactions. UGA exploits user insights to complement automated testing techniques by recording user-guided app executions, replaying apps to certain stop points, and systematically exploring state space from these stop points. We implemented our work as a prototype UGA tool on Android platform and evaluated it on seven real-world Android apps. Evaluation results show that UGA achieved 1.59-21.78× improvement in terms of method coverage over state-of-the-art automated techniques in testing mobile apps.

Applications in pervasive computing are often context-aware. However, due to uncontrollable environmental noises, contexts collected by applications can be distorted or even conflicting with each other. This is known as the context inconsistency problem. To provide reliable services, applications need to validate contexts before using them. One promising approach is to check contexts against consistency constraints at the runtime of applications. However, this can bring heavy computations due to tremendous amounts of contexts, thus leading to deteriorated performance to applications. Previous work has proposed incremental or concurrent checking techniques to improve the checking performance, but they heavily rely on CPU computing. In this paper, we propose a novel technique GAIN to exploit GPU computing to improve the checking performance. GAIN can automatically recognize parallel units in a constraint and schedule their checking in parallel on GPU cores. We evaluated GAIN with various constraints under different workloads. Our evaluation results show that, compared to CPU-based computing, GAIN saves CPU computing resources for pervasive applications while checks constraints much more efficiently.

Context-aware applications rely on contexts derived from sensory data to adapt their behavior. However, contexts can be inconsistent and cause application anomaly or crash. One popular solution is to detect and resolve context inconsistencies at runtime. However, we observe that many detected inconsistencies do not indicate real context problems. Instead, they are caused by improper inconsistency detection. These inconsistencies are harmless, and their resolution is unnecessary or may even cause new problems. We name them inconsistency hazards. Inconsistency hazards should be suppressed, but their occurrences resemble normal inconsistencies. In this paper, we present a pattern-learning based approach SHAP to suppressing the detection of inconsistency hazards. Our key insight is that the detection of such hazards is subject to certain patterns of context changes. These patterns, although difficult to specify manually, can be learned effectively from historical inconsistency detection data. We evaluated our SHAP experimentally through three context-aware applications. The results reported that SHAP can automatically suppress the detection of over 90% inconsistency hazards, while preserving the detection of over 98% normal inconsistencies, with only negligible overhead.

Deterministic replay tools help programmers debug concurrent programs. However, for long-running programs, a replay tool may generate huge log of shared memory access dependences. In this paper, we present CARE, an application-level deterministic record and replay technique to reduce the log size. The key idea of CARE is logging read-write dependences only at per-thread value prediction cache misses. This strategy records only a subset of all exact read-write dependences, and reduces synchronizations protecting memory reads in the instrumented code. Realizing that such record strategy provides only value-deterministic replay, CARE also adopts variable grouping and action prioritization heuristics to synthesize sequentially consistent executions at replay in linear time. We implemented CARE in Java and experimentally evaluated it with recognized benchmarks. Results showed that CARE successfully resolved all missing read-write dependences, producing sequentially consistent replay for all benchmarks. CARE exhibited 1.7--40X (median 3.4X) smaller runtime overhead, and 1.1--309X (median 7.0X) smaller log size against state-of-the-art technique LEAP.

Smartphone applications’ performance has a vital impact on user experience. However, many smartphone applications suffer from bugs that cause significant performance degradation, thereby losing their competitive edge. Unfortunately, people have little understanding of these performance bugs. They also lack effective techniques to fight with such bugs. To bridge this gap, we conducted a study of 70 real-world performance bugs collected from eight large-scale and popular Android applications. We studied the characteristics (e.g., bug types and how they manifested) of these bugs and identified their common patterns. These findings can support follow-up research on performance bug avoidance, testing, debugging and analysis for smartphone applications. To demonstrate the usefulness of our findings, we implemented a static code analyzer, PerfChecker, to detect our identified performance bug patterns. We experimentally evaluated PerfChecker by applying it to 29 popular Android applications, which comprise 1.1 million lines of Java code. PerfChecker successfully detected 126 matching instances of our performance bug patterns. Among them, 68 were quickly confirmed by developers as previously-unknown issues that affect application performance, and 20 were fixed soon afterwards by following our optimization suggestions.

Due to the demand for bugs fixing and feature enhancements, developers inevitably need to update in-use software systems. Instead of shutting down a running system before updating, it is often desirable and sometimes mandatory to patch the running software system on the fly, with a mechanism generally referred as dynamic software updating (DSU). Practical DSU strategies often require manual specification of update points in the program for performing dynamic updates. At these points DSU systems will update the program code, and also migrate the program state to the new version program (using transformation functions). However, finding appropriate update points is non-trivial because the choice of update points has great influence on two competing factors: the timeliness of DSU and the complexity of transformation functions; and to strike a good balance between them requires a deep understanding of both versions of the program. In this exploratory paper, we conceive an automated approach to the recommendation of update points for developers. We conduct a set of preliminary experiments with a real world software update case to examine the feasibility of the approach.

Self-adaptive applications address environmental dynamics systematically. They can be faulty and exhibit runtime errors when environmental dynamics are not considered adequately. It becomes more severe when uncertainty exists in their sensing and adaptation to environments. Existing work verifies self-adaptive applications, but does not explicitly consider environmental constraints or uncertainty. This gives rise to inaccurate verification results. In this paper, we address this problem by proposing a novel approach to verifying self-adaptive applications suffering uncertainty in their environmental interactions. It builds Interactive State Machine (ISM) models for such applications and verifies them with explicit consideration of environmental constraints and uncertainty. It then refines verification results by prioritizing counterexamples according to their probabilities. We experimentally evaluated our approach with real-life self-adaptive applications, and the experimental results confirmed its effectiveness. Our approach reported 200-660% more counterexamples than not considering uncertainty, and eliminated all false counterexamples caused by ignoring environmental constraints.

Recent research has made significant progress in automatic patch generation, an approach to repair programs with less or no manual intervention. However, direct deployment of auto-generated patches remains difficult, for reasons such as patch quality variations and developers' intrinsic resistance. In this study, we take one step back and investigate a more feasible application scenario of automatic patch generation, that is, using generated patches as debugging aids. We recruited 95 participants for a controlled experiment, in which they performed debugging tasks with the aid of either buggy locations (i.e., the control group), or generated patches of varied qualities. We observe that: a) high-quality patches significantly improve debugging correctness; b) such improvements are more obvious for difficult bugs; c) when using low-quality patches, participants' debugging correctness drops to an even lower point than that of the control group; d) debugging time is significantly affected not by debugging aids, but by participant type and the specific bug to fix. These results highlight that the benefits of using generated patches as debugging aids are contingent upon the quality of the patches. Our qualitative analysis of participants' feedback further sheds light on how generated patches can be improved and better utilized as debugging aids.

Smartphone applications' energy efficiency is vital, but many Android applications suffer from serious energy inefficiency problems. Locating these problems is labor-intensive and automated diagnosis is highly desirable. However, a key challenge is the lack of a decidable criterion that facilitates automated judgment of such energy problems. Our work aims to address this challenge. We conducted an in-depth study of 173 open-source and 229 commercial Android applications, and observed two common causes of energy problems: missing deactivation of sensors or wake locks, and cost-ineffective use of sensory data. With these findings, wepropose an automated approach to diagnosing energy problems in Android applications. Our approach explores an application's state space by systematically executing the application using Java PathFinder (JPF). It monitors sensor and wake lock operations to detect missing deactivation of sensors and wake locks. It also tracks the transformation and usage of sensory data and judges whether they are effectively utilized by the application using our state-sensitive data utilization metric. In this way, our approach can generate detailed reports with actionable information to assist developers in validating detected energy problems. We built our approach as a tool, GreenDroid, on top of JPF. Technically, we addressed the challenges of generating user interaction events and scheduling event handlers in extending JPF for analyzing Android applications. We evaluated GreenDroid using 13 real-world popular Android applications. GreenDroid completed energy efficiency diagnosis for these applications in a few minutes. It successfully located real energy problems in these applications, and additionally found new unreported energy problems that were later confirmed by developers.

Cyber-physical systems are systems that integrate the digital computational world with the real physical world, often using sensors and actuators as interfaces. There exist many application domains of cyber-physical systems such as autonomous systems, process control systems, robotic systems, and context-aware systems. The physical world is a complex and continuous world that changes in real-time while the computational world is a simplified and discrete world that often stores a delayed, likely inaccurate image of the physical world using sensory data. The mismatch between these two worlds poses unique challenges of developing software for cyber-physical systems.

Self-adaptive applications can easily contain faults. Existing approaches detect faults, but can still leave some undetected and manifesting into failures at runtime. In this paper, we study the correlation between occurrences of application failure and those of consistency failure. We propose fixing consistency failure to reduce application failure at runtime. We name this environment rematching, which can systematically reconnect a self-adaptive application to its environment in a consistent way. We also propose enforcing atomicity for application semantics during the rematching to avoid its side effect. We evaluated our approach using 12 self-adaptive robot-car applications by both simulated and real experiments. The experimental results confirmed our approach's effectiveness in improving dependability for all applications by 12.5-52.5%.

Smartphone applications have millions of users. Their energy efficiency is very important. However, we investigated 174 Android applications and found 33 of them suffering serious energy inefficiency problems. Many of these problems are due to ineffective use of sensors and their data. In this paper, we propose a novel approach to systematically diagnose energy inefficiency problems in Android applications. We derive an application execution model from Android specifications, and leverage it to realistically simulate an application's runtime behavior. Our approach can automatically analyze an application's sensory data utilization at different states, and report actionable information to help developers locate energy inefficiency problems and identify their root causes. We built a tool called GreenDroid on top of Java PathFinder and evaluated it using six popularly downloaded Android applications. GreenDroid analyzed these applications in a few minutes, and successfully located real energy inefficiency problems in them.

Practical software systems are subject to frequent updates for fixing their bugs or addressing new requirements. Updating a software system without stopping and restarting it is desired, as this helps reduce the redeployment cost as well as achieving the high availability. Existing techniques for dynamically updating Java programs may introduce noticeable pauses during which these programs are unable to function. We in this paper present Javelus, a dynamic Java update system with greatly reduced pausing time but without sacrificing update flexibility and system efficiency. Different from previous approaches, Javelus uses a lazy update mechanism with which an object-to-update will not be updated until it is really used. We implemented Javelus on top of an industry-strength OpenJDK HotSpot VM. We evaluated Javelus with real updates to Tomcat 7 and the same micro array benchmark used in evaluating Jvolve and DCE VM. The experiments report promising results that Javelus only incurred a pausing time two orders of magnitude smaller than those of Jvolve and DCE VM.

Self-adaptive systems are attractive due to their ability of adapting to changeable environments automatically. However, such systems may be subject to runtime failures when all environmental dynamics cannot be adequately considered at design time. When such failures occur at runtime, a system's internal adaptation logic usually has become inconsistent with its environment, according to our observation. We call this inconsistency sync-loss error. From our project experiences, we empirically identified a strong correlation between sync-loss error and system failure. This motivated us to fix sync-loss error in order to reduce failure for self-adaptive systems. In this paper, we formulate the problem of detecting sync-loss error, and present a framework ReSync to automatically fix sync-loss errors by desynchronizing a system with its environment. We experimentally evaluated ReSync on real robot cars with 20 different system versions. The evaluation reported promising results that ReSync can automatically recover our robot car systems from sync-loss errors, and significantly reduce the failure rate from 90.9% to 11.7-28.8%.

Detecting and resolving context inconsistency is critical to pervasive computing applications and infrastructures. Context inconsistency occurs when an application perceives contexts that breach predefined consistency constraints. This can drive an application to behave abnormally or even cause failure. Existing work commonly assumes the presence of a single application suffering from context inconsistency, such that specific repair actions can be taken to resolve the inconsistency for this application. However, when multiple applications run on the same infrastructure, they may impose conflicting requirements on resolving context inconsistency. In this paper, we propose a novel view-based approach ConsView to address such conflicting requirements. In ConsView, each application has a specific view to its own contexts that satisfy its own requirement on resolving context inconsistency. Such views are called consistent context views. We discuss the challenges of doing so and our ideas for addressing them. We implemented a prototype infrastructure supporting consistent context views, and evaluated it experimentally with simulated applications of real-life settings. The results confirmed the effectiveness and efficiency of our ConsView approach.

Internetware applications are context-aware and adaptive to their environmental changes. Faulty adaptation may arise when these applications face unexpected situations. Such adaptation faults can be difficult to detect at design time. The recent Adaptation Finite-State Machine (A-FSM) approach proposes to statically analyze model-based context-aware applications for adaptation faults. However, this approach may suffer expressiveness and precision problems. To address these limitations, we propose an Adaptation Model (AM) approach. As compared with A-FSM, AM offers increased expressive power to model complex rules, and guarantees soundness in fault detection. Besides, AM deploys an efficient rule evaluation technique to cater for context-aware applications that are subject to continual environmental changes. We evaluated our AM approach using both simulated and real-world experiments with two applications. The experimental results confirmed that AM can detect real faults missed by A-FSM, and avoid false positives that were misreported otherwise.

Recent pervasive systems are designed to be context-aware so that they are able to adapt to continual changes of their environments. Rule-based adaptation, which is commonly adopted by these applications, introduces new challenges in software design and verification. Recent research results have identified some faulty or unwanted adaptations caused by factors such as asynchronous context updating, and missing or faulty context reading. In addition, adaptation rules based on simple event models and propositional logic are not expressive enough to address these factors and to satisfy users' expectation in the design. We tackle these challenges at design stage by introducing sequential event patterns in adaptation rules to eliminate faulty and unwanted adaptations with features provided in the event pattern query language. We illustrate our approach using the recent published examples of adaptive applications, and show that it is promising on designing more reliable context-aware adaptive applications.

Pervasive computing environments typically change frequently in terms of available resources and their properties. Applications in pervasive computing use contexts to capture these changes and adapt their behaviors accordingly. However, contexts available to these applications may be abnormal or imprecise due to environmental noises. This may result in context inconsistencies, which imply that contexts conflict with each other. The inconsistencies may set such an application into a wrong state or lead the application to misadjust its behavior. It is thus desirable to detect and resolve the context inconsistencies in a timely way. One popular approach is to detect context inconsistencies when contexts breach certain consistency constraints. Existing constraint checking techniques recheck the entire expression of each affected consistency constraint upon context changes. When a changed context affects only a constraint's subexpression, rechecking the entire expression can adversely delay the detection of other context inconsistencies. This article proposes a rigorous approach to identifying the parts of previous checking results that are reusable without entire rechecking. We evaluated our work on the Cabot middleware through both simulation experiments and a case study. The experimental results reported that our approach achieved over a fifteenfold performance improvement on context inconsistency detection than conventional approaches.

Atomicity is a highly desirable property for achieving application consistency in service compositions. To achieve atomicity, a service composition should satisfy the atomicity sphere, a structural criterion for the backend processes of involved services. Existing analysis techniques for atomicity sphere generally assume complete knowledge of all involved backend processes. Such an assumption is invalid when some service providers do not release all details of their backend processes to service consumers outside the organizations. To address this problem, we propose a process algebraic framework to publish atomicity-equivalent public views from the backend processes. These public views extract relevant task properties and reveal only partial process details that service providers need to expose. Our framework enables the analysis of atomicity sphere for service compositions using these public views instead of their backend processes. This allows service consumers to choose suitable services such that their composition satisfies the atomicity sphere without disclosing the details of their backend processes. Based on the theoretical result, we present algorithms to construct atomicity-equivalent public views and to analyze the atomicity sphere for a service composition. Two case studies from supply chain and insurance domains are given to evaluate our proposal and demonstrate the applicability of our approach.

Context-awareness allows pervasive applications to adapt to changeable computing environments. Contexts, the pieces of information that capture the characteristics of environments, are often error-prone and inconsistent due to noises. Various strategies have been proposed to enable automatic context inconsistency resolution. They are formulated on different assumptions that may not hold in practice. This causes applications to be less context-aware to different extents. In this paper, we investigate such impacts and propose our new resolution strategy. We conducted experiments to compare our work with major existing strategies. The results showed that our strategy is both effective in resolving context inconsistencies and promising in its support of applications using contexts.

Context-awareness is a capability that allows applications in pervasive computing to adapt themselves continuously to changing contexts of their environments. However, contexts from physical environments may be inconsistent. It affects the correctness of these applications. Existing resolution strategies for context inconsistency have diverse adverse impacts on the context awareness of applications, such as feeding different amounts of contexts to the applications. In this paper, we examine the impacts of inconsistency resolution and study the extent to which their effects on context-awareness can be reduced. We conduct simulation experiments of two pervasive computing applications. The experimental results show that existing inconsistency resolution strategies adversely affect the context-awareness of applications. This motivates the importance of deploying an impact-oriented approach to respect context-awareness in inconsistency resolution.

Atomicity is a desirable property that safeguards application consistency for service compositions. A service composition exhibiting this property could either complete or cancel itself without any side effects. It is possible to achieve this property for a service composition by selecting suitable web services to form an atomicity sphere. However, this property might still be breached at runtime due to the interference between various service compositions caused by implicit interactions. Existing approaches to addressing this problem by restricting concurrent execution of services to avoid all implicit interactions however compromise the performance of service compositions due to the long running nature of web services. In this paper, we propose a novel static approach to analyzing the implicit interactions a web service may incur and their impacts on the atomicity property in each of its service compositions. By locating afflicted implicit interactions in a service composition, behavior constraints based on property propagation are formulated as local safety properties, which can then be enforced by the affected web services at runtime to suppress the impacts of the afflicted implicit interactions. We show that the satisfaction of these safety properties exempts the atomicity property of this service composition from being interfered by other services at runtime. The approach is illustrated using two service applications.

Applications in pervasive computing are typically required to interact seamlessly with their changing environments. To provide users with smart computational services, these applications must be aware of incessant context changes in their environments and adjust their behaviors accordingly. As these environments are highly dynamic and noisy, context changes thus acquired could be obsolete, corrupted or inaccurate. This gives rise to the problem of context inconsistency, which must be timely detected in order to prevent applications from behaving anomalously. In this paper, we propose a formal model of incremental consistency checking for pervasive contexts. Based on this model, we further propose an efficient checking algorithm to detect inconsistent contexts. The performance of the algorithm and its advantages over conventional checking techniques are evaluated experimentally using Cabot middleware.

Atomicity is a desirable property for business processes to conduct transactions in Business-to-Business (B2B) collaboration. Although it is possible to reason about atomicity of B2B collaboration using the public views, yet such reasoning requires the presence of a trustworthy party who has complete knowledge of these views. It is inapplicable when some parties may want to keep the confidentiality of their collaborative partners for privacy and other business reasons, or the trustworthy party is not available. To address this problem, we propose a novel approach that allows each party to jointly conduct local atomicity checking with its direct partners. It is based on iterative forwarding and regression of compensability properties between each pair of direct partners. This approach is applied to a case study based on a real-life insurance process in the motor damage claims domain.

Context-awareness is a key feature of pervasive computing whose environments keep evolving. The support of context-awareness requires comprehensive management including detection and resolution of context inconsistency, which occurs naturally in pervasive computing. In this paper we present a framework for realizing dynamic context consistency management. The framework supports inconsistency detection based on a semantic matching and inconsistency triggering model, and inconsistency resolution with proactive actions to context sources. We further present an implementation based on the Cabot middleware. The feasibility of the framework and its performance are evaluated through a case study and a simulated experiment, respectively.

As a key component of J2EE application servers, the distributed transaction manager following JTS and JTA specifications plays an important role in the distributed transaction environment. This paper explores the conformance test of a distributed transaction service by broadening the application of protocol conformance test theory and techniques. This paper also presents the formal representation of a distributed transaction service and the corresponding test case generation not based on personal experience.