JavaScript obfuscators are widely deployed to protect intellectual property and resist reverse engineering, yet their correctness has been largely overlooked compared to performance and resilience. Existing evaluations typically measure resistance to deobfuscation, leaving the critical question of whether obfuscators preserve program semantics unanswered. Incorrect transformations can silently alter functionality, compromise reliability, and erode security-undermining the very purpose of obfuscation. To address this gap, we present OBsmith, a novel framework to systematically test JavaScript obfuscators using large language models (LLMs). OBsmith leverages LLMs to generate program sketches-abstract templates capturing diverse language constructs, idioms, and corner cases-which are instantiated into executable programs and subjected to obfuscation under different configurations. Besides LLM-powered sketching, OBsmith also employs a second source: automatic extraction of skeletons from real programs. This extraction path enables more focused testing of project-specific features and lets developers inject domain knowledge into the resulting test cases. OBsmith uses two techniques to derive test oracles: (i) reference-oriented equivalence testing, which takes the original program as reference oracle (ground truth) and checks whether the obfuscated version preserves equivalent functionality, and (ii) metamorphic testing, which applies semantics-preserving transformations to the original program and checks if obfuscation violates expected behavior. We evaluate OBsmith on two widely used obfuscators, Obfuscator.IO and JS-Confuser, generating 600 sketches using six popular LLMs. OBsmith fills these sketches and generates over 3,000 candidate programs and obfuscates them across seven obfuscation configurations. OBsmith uncovers 11 previously unknown correctness bugs. Under an equal program budget, five general purpose state-of-the-art JavaScript fuzzers (FuzzJIT, Jsfunfuzz, Superion, DIE, Fuzzilli) failed to detect these issues, highlighting OBsmith's complementary focus on obfuscation-induced misbehavior. An ablation shows that all components except our generic MRs contribute to at least one bug class; the negative MR result suggests the need for obfuscator-specific metamorphic relations. Our results also seed a discussion on how to balance obfuscation presets and performance cost. We envision OBsmith as an important step towards automated testing and quality assurance of obfuscators and other semantic-preserving toolchains.

Propositional satisfiability (SAT) is an NP-complete problem that impacts many research fields, such as planning, verification, and security. Mainstream modern SAT solvers are based on the Conflict-Driven Clause Learning (CDCL) algorithm. Recent work aimed to enhance CDCL SAT solvers using Graph Neural Networks (GNNs). However, so far this approach either has not made solving more effective, or required substantial GPU resources for frequent online model inferences. Aiming to make GNN improvements practical, this paper proposes an approach called NeuroBack, which builds on two insights: (1) predicting phases (i.e., values) of variables appearing in the majority (or even all) of the satisfying assignments are essential for CDCL SAT solving, and (2) it is sufficient to query the neural model only once for the predictions before the SAT solving starts. Once trained, the offline model inference allows NeuroBack to execute exclusively on the CPU, removing its reliance on GPU resources. To train NeuroBack, a new dataset called DataBack containing 120,286 data samples is created. Finally, NeuroBack is implemented as an enhancement to a state-of-the-art SAT solver called Kissat. As a result, it allowed Kissat to solve 5.2% more problems on the recent SAT competition problem set, SATCOMP-2022. NeuroBack therefore shows how machine learning can be harnessed to improve SAT solving in an effective and practical manner.

Identity and Access Management (IAM) is an access control service employed within cloud platforms. Customers must configure IAM to establish secure access control rules for their cloud organizations. However, IAM misconfigurations can be exploited to conduct Privilege Escalation (PE) attacks, resulting in significant financial losses. Consequently, addressing these PEs is crucial for improving security assurance for cloud customers. Nevertheless, the area of repairing IAM PEs due to IAM mis-configurations is relatively underexplored. To our knowledge, the only existing IAM repair tool called IAM-Deescalate focuses on a limited number of IAM PE patterns, indicating the potential for further enhancements. We propose a novel IAM Privilege Escalation Repair Engine called IAMPERE that efficiently generates an approximately minimal patch for repairing a broader range of IAM PEs. To achieve this, we first formulate the IAM repair problem into a MaxSAT problem. Despite the remarkable success of modern MaxSAT solvers, their scalability for solving complex repair problems remains a challenge due to the state explosion. To improve scalability, we employ deep learning to prune the search space. Specifically, we apply a carefully designed GNN model to generate an intermediate patch that is relatively small, but not necessarily minimal. We then apply a MaxSAT solver to search for a minimum repair within the space defined by the intermediate patch, as the final approximately minimum patch. Experimental results on both synthesized and real-world IAM misconfigurations show that, compared to IAM-Deescalate, IAMPERE repairs a significantly larger number of IAM misconfigurations with markedly smaller patch sizes.

Automatic machine learning, or AutoML, holds the promise of truly democratizing the use of machine learning (ML), by substantially automating the work of data scientists. However, the huge combinatorial search space of candidate pipelines means that current AutoML techniques, generate sub-optimal pipelines, or none at all, especially on large, complex datasets. In this work we propose an AutoML technique SapientML, that can learn from a corpus of existing datasets and their human-written pipelines, and efficiently generate a high-quality pipeline for a predictive task on a new dataset. To combat the search space explosion of AutoML, SapientML employs a novel divide-and-conquer strategy realized as a three-stage program synthesis approach, that reasons on successively smaller search spaces. The first stage uses meta-learning to predict a set of plausible ML components to constitute a pipeline. In the second stage, this is then refined into a small pool of viable concrete pipelines using a pipeline dataflow model derived from the corpus. Dynamically evaluating these few pipelines, in the third stage, provides the best solution. We instantiate SapientML as part of a fully automated tool-chain that creates a cleaned, labeled learning corpus by mining Kaggle, learns from it, and uses the learned models to then synthesize pipelines for new predictive tasks. We have created a training corpus of 1,094 pipelines spanning 170 datasets, and evaluated SapientML on a set of 41 benchmark datasets, including 10 new, large, real-world datasets from Kaggle, and against 3 state-of-the-art AutoML tools and 4 baselines. Our evaluation shows that SapientML produces the best or comparable accuracy on 27 of the benchmarks while the second best tool fails to even produce a pipeline on 9 of the instances. This difference is amplified on the 10 most challenging benchmarks, where SapientML wins on 9 instances with the other tools failing to produce pipelines on 4 or more benchmarks.

Specifying and analyzing critical properties of software systems plays an important role in the development of reliable systems. Alloy is a mature tool-set that provides a first-order relational logic for writing specifications, and a fully automatic powerful backend for analyzing the specifications. It has been widely applied in areas including verification, security, and synthesis.

Data scientists typically practice exploratory programming using computational notebooks, to comprehend new data and extract insights. To do this they iteratively refine their code, actively trying to re-use and re-purpose solutions created by other data scientists, in real time. However, recent studies have shown that a vast majority of publicly available notebooks cannot be executed out of the box. One of the prominent reasons is the deprecation of data science APIs used in such notebooks, due to the rapid evolution of data science libraries. In this work we propose RELANCER, an automatic technique that restores the executability of broken Jupyter Notebooks, in near real time, by upgrading deprecated APIs. RELANCER employs an iterative runtime-error-driven approach to identify and fix one API issue at a time. This is supported by a machine-learned model which uses the runtime error message to predict the kind of API repair needed - an update in the API or package name, a parameter, or a parameter value. Then RELANCER creates a search space of candidate repairs by combining knowledge from API migration examples on GitHub as well as the API documentation and employs a second machine-learned model to rank this space of candidate mappings. An evaluation of RELANCER on a curated dataset of 255 un-executable Jupyter Notebooks from Kaggle shows that RELANCER can successfully restore the executability of 56% of the subjects, while baselines relying on just GitHub examples and just API documentation can only fix 38% and 36% of the subjects respectively. Further, pursuant to its real-time use case, RELANCER can restore execution to 49% of subjects, within a 5 minute time limit, while a baseline lacking its machine learning models can only fix 24%.

Access control is essential for the Operating System (OS) security. Incorrect implementation of access control can introduce new attack surfaces to the OS, known as Kernel Access Control Vulnerabilities (KACVs). To understand KACVs, we conduct our study on the root causes and the security impacts of KACVs. Regarding the complexity of the recognized root causes, we particularly focus on two kinds of KACVs, namely KACV-M (due to missing permission checks) and KACV-I (due to misusing permission checks). We find that over 60% of these KACVs are of critical, high or medium security severity, resulting in a variety of security threats including bypass security checking, privileged escalation, etc. However, existing approaches can only detect KACV-M. The state-of-the-art KACV-M detector called PeX is a static analysis tool, which still suffers from extremely high false-positive rates.

Manual debugging is notoriously tedious and time-consuming. Therefore, various automated fault localization techniques have been proposed to help with manual debugging. Among the existing fault localization techniques, spectrum-based fault localization (SBFL) is one of the most widely studied techniques due to being lightweight. The focus of the existing SBFL techniques is to consider how to differentiate program entities (i.e., one dimension in program spectra); indeed, this focus is aligned with the ultimate goal of finding the faulty lines of code. Our key insight is to enhance the existing SBFL techniques by additionally considering how to differentiate tests (i.e., the other dimension in program spectra), which, to the best of our knowledge, has not been studied in prior work. We present our basic approach, PRFL, a lightweight technique that boosts SBFL by differentiating tests using PageRank algorithm. Specifically, given the original program spectrum information, PRFL uses PageRank to recompute the spectrum by considering the contributions of different tests. Next, traditional SBFL techniques are applied on the recomputed spectrum to achieve more effective fault localization. On top of PRFL, we explore PRFL+ and PRFLMA, two variants which extend PRFL by optimizing its components and integrating Method-level Aggregation technique, respectively. Though being simple and lightweight, PRFL has been demonstrated to outperform state-of-the-art SBFL techniques significantly (e.g., ranking 39.2% / 82.3% more real/artificial faults at Top-1 compared with the most effective traditional SBFL technique) with low overhead (e.g., around 6 minutes average extra overhead on real faults) on 395 real faults from 6 Defects4J projects and 96925 artificial (i.e., mutation) faults from 240 GitHub projects. To further validate PRFL's effectiveness, we compare PRFL with multiple recent proposed fault localization techniques (e.g., Multric, Metallaxis and MBFL-hybrid-avg), and the experimental results show that PRFL outperforms them as well. Furthermore, we study the performance of PRFLMA, and the experimental results present it can locate 137 real faults (73.4% / 24.5% more compared with the most effective SBFL/PRFL technique) and 35058 artificial faults (159.6% / 28.1% more than SBFL/PRFL technique) at Top-1. At last, we study the generalizability of PRFL on another benchmark, Bugs.jar, and the result shows PRFL can help locate around 30 percent more faults at Top 1.

Formal methods have enabled breakthroughs in many fields, such as in hardware verification, machine learning and biological systems. The key object of interest in systems biology, synthetic biology, and molecular programming is chemical reaction networks (CRNs) which formalizes coupled chemical reactions in a well-mixed solution. CRNs are pivotal for our understanding of biological regulatory and metabolic networks, as well as for programming engineered molecular behavior. Although it is clear that small CRNs are capable of complex dynamics and computational behavior, it remains difficult to explore the space of CRNs in search for desired functionality. We use Alloy, a tool for expressing structural constraints and behavior in software systems, to enumerate CRNs with declaratively specified properties. We show how this framework can enumerate CRNs with a variety of structural constraints including biologically motivated catalytic networks and metabolic networks, and seesaw networks motivated by DNA nanotechnology. We also use the framework to explore analog function computation in rate-independent CRNs. By computing the desired output value with stoichiometry rather than with reaction rates (in the sense that X → Y+Y computes multiplication by 2), such CRNs are completely robust to the choice of reaction rates or rate law. We find the smallest CRNs computing the max, minmax, abs and ReLU (rectified linear unit) functions in a natural subclass of rate-independent CRNs where rate-independence follows from structural network properties.

Embedding computation in molecular contexts incompatible with traditional electronics is expected to have wide ranging impact in synthetic biology, medicine, nanofabrication and other fields. A key remaining challenge lies in developing programming paradigms for molecular computation that are well-aligned with the underlying chemical hardware and do not attempt to shoehorn ill-fitting electronics paradigms. We discover a surprisingly tight connection between a popular class of neural networks (binary-weight ReLU aka BinaryConnect) and a class of coupled chemical reactions that are absolutely robust to reaction rates. The robustness of rate-independent chemical computation makes it a promising target for bioengineering implementation. We show how a BinaryConnect neural network trained in silico using well-founded deep learning optimization techniques, can be compiled to an equivalent chemical reaction network, providing a novel molecular programming paradigm. We illustrate such translation on the paradigmatic IRIS and MNIST datasets. Toward intended applications of chemical computation, we further use our method to generate a chemical reaction network that can discriminate between different virus types based on gene expression levels. Our work sets the stage for rich knowledge transfer between neural network and molecular programming communities.

As systems that deploy machine learning models become more and more pervasive, there is an urgent need to ensure their reliability and safety. While recent years have seen a lot of progress in techniques for verification and validation of machine learning models, reasoning about and explaining their behaviors remains challenging. This paper introduces a new approach for creating machine learning models where instead of the traditional supervised learning using data, the models are directly synthesized from specifications, and thus, are correct by construction. Our focus is binary classifiers with boolean features. Specifically, our approach translates relational specifications written in the well-known modeling language Alloy to neural networks that run on the widely used Tensorflow backend. Our key insight is that a slight enhancement of traditional boolean gates can provide a rich intermediate representation that readily translates to neural networks. To translate the enhanced gates to neural networks, we employ a state-of-the-art program synthesis framework that allows us to find minimal neural networks. The translation of Alloy specifications then follows the standard translation to boolean logic with the exception of utilizing the enhanced boolean gates, followed by a translation to neural networks. We embody our approach in a prototype tool and use it for experimental evaluation. The experimental results show that our approach allows synthesis of neural networks that are hard to create using traditional training methods.

Fault localization is a popular research topic and many techniques have been proposed to locate faults in imperative code, e.g. C and Java. In this paper, we focus on the problem of fault localization for declarative models in Alloy - a first order relational logic with transitive closure. We introduce AlloyFLhy, the first fault localization technique for faulty Alloy models which leverages multiple test formulas. AlloyFLhybrings the traditional spectrum-based and mutation-based fault localization techniques to Alloy and combines both techniques to locate faults. To measure the effectiveness of AlloyFLhy, we define three distance metrics and use both distance-based and top-k metrics to measure the effectiveness of AlloyFLhyon 90 real faulty models. The results show that AlloyFLhy is substantially more effective than Alloy's built-in unsat core.

Model counting is the problem for finding the number of solutions to a formula over a bounded universe. This is a classic problem in computer science that has seen many recent advances in techniques and tools that tackle it. These advances have led to applications of model counting in many domains, e.g., quantitative program analysis, reliability, and security. Given the sheer complexity of the underlying problem, today's model counters employ sophisticated algorithms and heuristics, which result in complex tools that must be heavily optimized. Therefore, establishing the correctness of implementations of model counters necessitates rigorous testing. This experience paper presents an empirical study on testing industrial strength model counters by applying the principles of differential and metamorphic testing together with bounded exhaustive input generation and input minimization. We embody these principles in the TestMC framework, and apply it to test four model counters, including three state-of-the-art model counters from three different classes. Specifically, we test the exact model counters projMC and dSharp, the probabilistic exact model counter Ganak, and the probabilistic approximate model counter ApproxMC. As subjects, we use three complementary test suites of input formulas. One suite consists of larger formulas that are derived from a wide range of real-world software design problems. The second suite consists of a bounded exhaustive set of small formulas that TestMC generated. The third suite consists of formulas generated using an off-the-shelf CNF fuzzer. TestMC found bugs in three of the four subject model counters. The bugs led to crashes, segmentation faults, incorrect model counts, and resource exhaustion by the solvers. Two of the tools were corrected subsequent to the bug reports we submitted based on our study, whereas the bugs we reported in the third tool were deemed by the tool authors to not require a fix.

This paper introduces the MCML approach for empirically studying the learnability of relational properties that can be expressed in the well-known software design language Alloy. A key novelty of MCML is quantification of the performance of and semantic differences among trained machine learning (ML) models, specifically decision trees, with respect to entire (bounded) input spaces, and not just for given training and test datasets (as is the common practice). MCML reduces the quantification problems to the classic complexity theory problem of model counting, and employs state-of-the-art model counters. The results show that relatively simple ML models can achieve surprisingly high performance (accuracy and F1-score) when evaluated in the common setting of using training and test datasets -- even when the training dataset is much smaller than the test dataset -- indicating the seeming simplicity of learning relational properties. However, MCML metrics based on model counting show that the performance can degrade substantially when tested against the entire (bounded) input space, indicating the high complexity of precisely learning these properties, and the usefulness of model counting in quantifying the true performance.

Specifying and analyzing desired properties of software systems can play an important role in the development of more dependable systems. Alloy is a mature tool-set that provides a first-order, rela- tional logic with transitive closure for writing the specifications, and a fully automatic backend based on propositional satisfiability (SAT) solvers for analyzing them. Alloy’s intuitive notation and sup- port for modern solvers make it a particularly effective specification and analysis tool, which has been applied in several domains, including verification, security, and synthesis. This paper introduces a new backend for Alloy, which complements SAT solvers, and provides a new method to assist Alloy users to more effectively use the tool-set, specifically in scenarios where multiple solutions to the same formula are desired. We add to the Alloy backend support for model counting, i.e., computing the number of solutions to the given formula. We extend the Alloy grammar to add a new com- mand for model counting, and extend the Alloy GUI to customize it. Our implementation, called AlloyMC, supports two state-of-the-art model counters: the approximate model counter ApproxMC and the exact model counter ProjMC. AlloyMC runs on Linux, Mac, and Windows. To use AlloyMC, users just download and run its integrated JAR file with no need to install dependencies (e.g., model counters and their dependent libraries). The AlloyMC source code, the JAR file, and the data set are available publicly.

Propositional model counting is a classic problem that has recently witnessed many technical advances and novel applications. While the basic model counting problem requires computing the number of all solutions to the given formula, in some important application scenarios, the desired count is not of all solutions, but instead, of all unique solutions up to isomorphism . In such a scenario, the user herself must try to either use the full count that the model counter returns to compute the count up to isomorphism, or ensure that the input formula to the model counter adequately captures the symmetry breaking predicates so it can directly report the count she desires. We study the use of CNF-level and domain-level symmetry breaking predicates in the context of the state-of-the-art in model counting, specifically the leading approximate model counter ApproxMC and the recently introduced exact model counter ProjMC. As benchmarks, we use a range of problems, including structurally complex specifications of software systems and constraint satisfaction problems. The results show that while it is sometimes feasible to compute the model counts up to isomorphism using the full counts that are computed by the model counters, doing so suffers from poor scalability. The addition of symmetry breaking predicates substantially assists model counters. Domain-specific predicates are particularly useful, and in many cases can provide full symmetry breaking to enable highly efficient model counting up to isomorphism. We hope our study motivates new research on designing model counters that directly account for symmetries to facilitate further applications of model counting.

We present Deuterium---a framework for implementing Java methods as executable contracts. Deuterium introduces a novel, type-safe way to write method contracts entirely in Java, as a combination of imperative generators and declarative specifications (written in a first-order relational logic with transitive closure). Existing approaches are typically based on encoding both the specification and the program heap into a constraint language, and then using an off-the-shelf constraint solver---without any additional guidance---to search for a new program heap that satisfies the specification. Deuterium takes advantage of user-provided generators to prune the search space and reduce incurred overhead of constraint solving. Deuterium supports two ways of solving declarative constraints: SAT-based and search-based with in-memory state exploration. We evaluate our approach on a suite of data structures, established as a standard benchmark by prior work. Furthermore, we use random and sequence-based test generation to create a new benchmark designed to mimic realistic execution scenarios. Our results show that generators improve the performance of executable contracts and that in-memory state exploration is the algorithm of choice when heap sizes are small.

Bounded exhaustive testing (BET) techniques have been shown to be effective for detecting faults in software. BET techniques based on imperative predicates, enumerate all test inputs up to the given bounds such that each test input satisfies the properties encoded by the predicate. The search space is bounded by the user, who specifies the number of objects of each type and the list of values for each field of each type. To optimize the search, existing techniques detect isomorphic instances and record accessed fields during the execution of a predicate. However, these optimizations are extension-unaware, i.e., they do not speed up the search when the predicate is modified, say due to a fix or additional properties. We present a technique, named iGen, that speeds up test generation when imperative predicates are extended. iGen memoizes intermediate results of a test generation and reuses the results in a future search - even when the new search space differs from the old space. We integrated our technique in two BET tools (one for Java and one for Python) and evaluated these implementations with several data structure pairs, including two pairs from the Standard Java Library. Our results show that iGen speeds up test generation by up to 46.59x for the Java tool and up to 49.47x for the Python tool. Additionally, we show that the speedup obtained by iGen increases for larger test instances.

Constraint-solving is an expensive phase for scenario finding tools. It has been widely observed that there is no single "dominant" SAT solver that always wins in every case; instead, the performance of different solvers varies by cases. Some SAT solvers perform particularly well for certain tasks while other solvers perform well for other tasks. In this paper, we propose an approach that uses machine learning techniques to automatically select a SAT solver for one of the widely used scenario finding tools, i.e. Alloy Analyzer, based on the features extracted from a given model. The goal is to choose the best SAT solver for a given model to minimize the expensive constraint solving time. We extract features from three different levels, i.e. the Alloy source code level, the Kodkod formula level and the boolean formula level. The experimental results show that our portfolio approach outperforms the best SAT solver by 30% as well as the baseline approach by 128% where users randomly select a solver for any given model.

Regression testing is an important but expensive activity in software development. Among various types of tests, web service tests are usually one of the most expensive (due to network communications) but widely adopted types of tests in commercial software development. Regression test selection (RTS) aims to reduce the number of tests which need to be retested by only running tests that are affected by code changes. Although a large number of RTS techniques have been proposed in the past few decades, these techniques have not been adopted on large-scale web service testing. This is because most existing RTS techniques either require direct code dependency between tests and code under test or cannot be applied on large scale systems with enough efficiency. In this paper, we present a novel RTS technique, TestSage, that performs RTS for web service tests on large scale commercial software. With a small overhead, TestSage is able to collect fine grained (function level) dependency between test and service under test that do not directly depend on each other. TestSage has also been successfully applied to large complex systems with over a million functions. We conducted experiments of TestSage on a large scale backend service at Google. Experimental results show that TestSage reduces 34% of testing time when running all AEC (Analysis, Execution and Collection) phases, 50% of testing time while running without collection phase. TestSage has been integrated with internal testing framework at Google and runs day-to-day at the company.

Deep Neural Networks (DNN) are increasingly used in a variety of applications, many of them with serious safety and security concerns. This paper describes DeepCheck, a new approach for validating DNNs based on core ideas from program analysis, specifically from symbolic execution. DeepCheck implements novel techniques for lightweight symbolic analysis of DNNs and applies them to address two challenging problems in DNN analysis: 1) identification of important input features and 2) leveraging those features to create adversarial inputs. Experimental results with an MNIST image classification network and a sentiment network for textual data show that DeepCheck promises to be a valuable tool for DNN analysis.

Natural language elements, e.g., todo comments, are frequently used to communicate among developers and to describe tasks that need to be performed (actions) when specific conditions hold on artifacts related to the code repository (triggers), e.g., from the Apache Struts project: “remove expectedJDK15 and if() after switching to Java 1.6”. As projects evolve, development processes change, and development teams reorganize, these comments, because of their informal nature, frequently become irrelevant or forgotten. We present the first framework, dubbed TrigIt, to specify trigger-action todo comments in executable format. Thus, actions are executed automatically when triggers evaluate to true. TrigIt specifications are written in the host language (e.g., Java) and are evaluated as part of the build process. The triggers are specified as query statements over abstract syntax trees, abstract representation of build configuration scripts, issue tracking systems, and system clock time. The actions are either notifications to developers or code transformation steps. We implemented TrigIt for the Java programming language and migrated 44 existing trigger-action comments from several popular open-source projects. Evaluation of TrigIt, via a user study, showed that users find TrigIt easy to learn and use. TrigIt has the potential to enforce more discipline in writing and maintaining comments in large code repositories.

Alloy is a well-known tool-set for building and analyzing software designs and models. Alloy’s key strengths are its intuitive notation based on relational logic, and its powerful analysis engine backed by propositional satisfiability (SAT) solvers to help users find subtle design flaws. However, scaling the analysis to the designs of real-world systems remains an important technical challenge. This paper introduces a new approach, iAlloy, for more efficient analysis of Alloy models. Our key insight is that users often make small and frequent changes and repeatedly run the analyzer when developing Alloy models, and the development cost can be reduced with the incremental analysis over these changes. iAlloy is based on two techniques – a static technique based on a lightweight impact analysis and a dynamic technique based on solution re-use – which in many cases helps avoid potential costly SAT solving. Experimental results show that iAlloy significantly outperforms Alloy analyzer in the analysis of evolving Alloy models with more than 50% reduction in SAT solver calls on average, and up to 7x speedup.

Symbolic execution is an effective but expensive technique for automated test generation. Over the years, a large number of refined symbolic execution techniques have been proposed to improve its efficiency. However, the symbolic execution efficiency problem remains, and largely limits the application of symbolic execution in practice. Orthogonal to refined symbolic execution, in this paper we propose to accelerate symbolic execution through semantic-preserving code transformation on the target programs. During the initial stage of this direction, we adopt a particular code transformation, compiler optimization, which is initially proposed to accelerate program concrete execution by transforming the source program into another semantic-preserving target program with increased efficiency (e.g., faster or smaller). However, compiler optimizations are mostly designed to accelerate program concrete execution rather than symbolic execution. Recent work also reported that unified settings on compiler optimizations that can accelerate symbolic execution for any program do not exist at all. Therefore, in this work we propose a machine-learning based approach to tuning compiler optimizations to accelerate symbolic execution, whose results may also aid further design of specific code transformations for symbolic execution. In particular, the proposed approach LEO separates source-code functions and libraries through our program-splitter, and predicts individual compiler optimization (i.e., whether a type of code transformation is chosen) separately through analyzing the performance of existing symbolic execution. Finally, LEO applies symbolic execution on the code transformed by compiler optimization (through our local-optimizer). We conduct an empirical study on GNU Coreutils programs using the KLEE symbolic execution engine. The results show that LEO significantly accelerates symbolic execution, outperforming the default KLEE configurations (i.e., turning on/off all compiler optimizations) in various settings, e.g., with the default training/testing time, LEO achieves the highest line coverage in 50/68 programs, and its average improvement rate on all programs is 46.48%/88.92% in terms of line coverage compared with turning on/off all compiler optimizations.

Effective program repair techniques, which modify faulty programs to fix them with respect to given test suites, can substantially reduce the cost of manual debugging. A common repair approach is to iteratively first generate candidate programs with possible bug fixes and then validate them against the given tests until a candidate that passes all the tests is found. While this approach is conceptually simple, due to the potentially high number of candidates that need to first be generated and then be compiled and tested, existing repair techniques that embody this approach have relatively low effectiveness, especially for faults at a fine granularity.

Software models help improve the reliability of software systems: models can convey requirements, and can analyze design and implementation properties. A key strength of Alloy, a commonly used first-order modeling language, is the Alloy Analyzer tool-set. The Analyzer allows users to execute commands over models by leveraging a fully automatic SAT-based analysis engine. However, prior to the introduction of AUnit - a testing framework for Alloy - users had to rely on ad-hoc practices to validate their models. In this paper, we present our efforts to establish a formal testing environment in the Alloy Analyzer by creating an AUnit extension. We present additional grammar to support test case creation, as well as the details for executing test suites, calculating test suite coverage, and automatically generating test suites. The tool is available as a stand-alone executable at the following URL (https://sites.google.com/view/aunitanalyzer).

Good API design enables many clients to effectively use the core functionality implemented by the APIs. For real-world applications however, correctly using the APIs and identifying what methods to use and how to invoke them appropriately can be challenging. Researchers have developed a number of API synthesis approaches that enable a semantically rich form of API completion where the client provides a description of desired functionality, e.g., in the form of test suites, and the automatic tools create method sequences using the desired APIs based on the given correctness criteria (e.g., all given tests pass). However, existing API synthesis approaches are largely limited to creating single basic blocks of code and do not readily handle multiple blocks in the presence of loops (or recursion) and complex test executions. A key issue with handling multiple blocks is the very large space of possible method sequences and their combinations. This paper introduces EdSynth, an API synthesis approach that explores the sequence spaces on-demand during the test execution; that is, the given tests not only provide a validation mechanism - as is common in test-driven API synthesis - but also play a vital role in guiding the space exploration by helping prune much of it. EdSynth follows the spirit of recent work on test-execution-driven synthesis and lazily initializes candidates during the execution of given tests where the part of the candidate completion that is actually executed directly determines the generation of future candidates. To further optimize the space exploration, EdSynth ranks API candidates based on a set of pre-defined heuristics. We evaluate EdSynth's ability to synthesize complex APIs in the presence of conditional statements, loops and multiple basic blocks. The experimental results show that EdSynth is effective at handling synthesis tasks with multiple API sequences in both the conditions and bodies of loops/branches; moreover, when applied to synthesis of straight-line code, EdSynth compares well with a state-of-the-art API synthesis tool that only handles straight-line code. The experiments show that EdSynth's ranking strategies help reduce synthesis time by 43%.

The paper Test Input Generation With Java PathFinder was published in the International Symposium on Software Testing and Analysis (ISSTA) 2004 Proceedings, and has now been selected to receive the ISSTA 2018 Retrospective Impact Paper Award. The paper described black-box and white-box techniques for the automated testing of software systems. These techniques were based on model checking and symbolic execution and incorporated in the Java PathFinder analysis tool. The main contribution of the paper was to describe how to perform efficient test input generation for code manipulating complex data that takes into account complex method preconditions and evaluate the techniques for generating high coverage tests.

Automated program repair is an active research area. However, existing research focuses mostly on imperative code, e.g. in Java. In this paper, we study the problem of repairing declarative models in Alloy -- a first order relational logic with transitive closure. We introduce ARepair, the first technique for repairing Alloy models. ARepair follows the spirit of traditional automated program repair techniques. Specifically, ARepair takes as input a faulty Alloy model and a test suite that contains some failing test, and outputs a repaired model that is correct with respect to the given tests. ARepair integrates ideas from mutation testing and program synthesis to provide an effective solution for repairing Alloy models. The experimental results show that ARepair can fix 28 out of 38 real-world faulty models we collected.

While Deep Neural Networks (DNNs) have established the fundamentals of image-based autonomous driving systems, they may exhibit erroneous behaviors and cause fatal accidents. To address the safety issues in autonomous driving systems, a recent set of testing techniques have been designed to automatically generate artificial driving scenes to enrich test suite, e.g., generating new input images transformed from the original ones. However, these techniques are insufficient due to two limitations: first, many such synthetic images often lack diversity of driving scenes, and hence compromise the resulting efficacy and reliability. Second, for machine-learning-based systems, a mismatch between training and application domain can dramatically degrade system accuracy, such that it is necessary to validate inputs for improving system robustness.

Manually locating and removing bugs in faulty program is often tedious and error-prone. A common automated program repair approach called generate-and-validate (G&V) iteratively creates candidate fixes, compiles them, and runs these candidates against the given tests. This approach can be costly due to a large number of re-compilations and re-executions of the program. To tackle this limitation, recent work introduced the SketchFix approach that tightly integrates the generation and validation phases, and utilizes runtime behaviors to substantially prune a large amount of repair candidates. This tool paper describes our Java implementation of SketchFix, which is an open-source library that we released on Github. Our experimental evaluation using Defects4J benchmark shows that SketchFix can significantly reduce the number of re-compilations and re-executions compared to other approaches and work particularly well in repairing expression manipulation at the AST node-level granularity.The demo video is at: https://youtu.be/AO-YCH8vGzQ.

Alloy is a declarative modeling language that supports first-order logic with transitive closure. Alloy has been used in a variety of domains to model software systems and find design deficiencies. However, it is often challenging to make an Alloy model correct or to debug a faulty Alloy model. ASketch is a sketching/synthesis technique that can help users write correct Alloy models. ASketch allows users to provide a partial Alloy model with holes, a generator that specifies candidate fragments to be considered for each hole, and a set of tests that capture the desired model properties. Then, the tool completes the holes such that all tests for the completed model pass. ASketch uses tests written for the recently introduced AUnit framework, which provides a foundation of testing (unit tests, test execution, and model coverage) for Alloy models in the spirit of traditional unit testing. This paper describes our Java implementation of ASketch, which is a command-line tool, released as an open-source project on GitHub. Our experimental results show that ASketch can handle partial Alloy models with multiple holes and a large search space. The demo video for ASketch can be found at https://youtu.be/T5NIVsV329E.

Symbolic execution is a well-studied method that has a number of useful applications, including generation of high-quality test suites that find many bugs. However, scaling it to real-world applications is a significant challenge, as it depends on the often expensive process of solving constraints on program inputs. Our insight is that when the goal of symbolic execution is test generation, non-semantics-preserving program transformations can reduce the cost of symbolic execution and the tests generated for the transformed programs can still serve as quality suites for the original program. We present five such transformations based on a few different program simplification heuristics that are designed to lower the cost of symbolic execution for input generation. As enabling technology we use the KLEE symbolic execution engine and the LLVM compiler infrastructure. We evaluate our transformations using a suite of small subjects as well as a subset of the well-studied Unix Coreutils. In a majority of cases, our approach reduces the time for symbolic execution for input generation and increases code coverage of the resultant suite.

We present two novel approaches for automated testing of models written in Alloy – a well-known declarative, first-order language that is supported by a fully automatic SAT-based analysis engine. The first approach introduces automated test generation for Alloy and is embodied by three techniques that create test suites in the traditional spirit of black-box, white-box, and mutation-based testing. The second approach introduces mutation testing for Alloy and defines how to create mutants of Alloy models, compute mutation testing results, and check for equivalent mutants using SAT. The two approaches build on the theoretical foundation defined previously by our AUnit framework, which introduced the idea of unit testing for Alloy in the spirit of unit testing for imperative languages. While test generation and mutation testing are heavily studied problems with many solutions in the context of imperative languages, the key novelty of our work is to introduce and address these problems for the declarative programming paradigm, specifically for the Alloy language. Experimental results using several Alloy subjects, including those with real faults, demonstrate the efficacy of our framework.

Manual debugging is notoriously tedious and time consuming. Therefore, various automated fault localization techniques have been proposed to help with manual debugging. Among the existing fault localization techniques, spectrum-based fault localization (SBFL) is one of the most widely studied techniques due to being lightweight. A focus of existing SBFL techniques is to consider how to differentiate program source code entities (i.e., one dimension in program spectra); indeed, this focus is aligned with the ultimate goal of finding the faulty lines of code. Our key insight is to enhance existing SBFL techniques by additionally considering how to differentiate tests (i.e., the other dimension in program spectra), which, to the best of our knowledge, has not been studied in prior work.

Constraint-based input generation enables systematic testing for effective bug finding, but requires exploration of very large spaces of candidate inputs. This paper introduces a novel approach to optimize input generation using Korat – a solver for constraints written as imperative predicates in Java – when Korat is executed more than once for the same constraint solving problem. Our key insight is that in certain application scenarios the Korat search over the same state space and constraint is repeated across separate runs of Korat, and an earlier run can be summarized to optimize a later run. We introduce invalid ranges to represent parts of the exploration space that do not contain any valid inputs but must be explicitly explored by Korat. Our approach directly prunes these parts in a future run of Korat over the same search problem. We develop our approach for two settings: a sequential setting where the Korat search is run using one worker (i.e., processing unit), and a parallel setting where the search is distributed to several workers. In the parallel setting, we build on a previous technique for parallel Korat, namely SEQ-ON, and integrate invalid ranges with it. Experimental evaluation using 6 subjects show that our approach achieves: in the sequential setting, a speedup of up to 2.82X over sequential Korat (in comparison, SEQ-ON does not provide any speedup in the sequential setting); and in the distributed setting, using up to 32 workers, a speedup of up to 38.84X over sequential Korat (using 1 worker), and up to 3.04X over SEQ-ON in terms of total execution time across the workers.

Sketching is a relatively recent approach to program synthesis, which has shown much promise. The key idea in sketching is to allow users to write partial programs that have ''holes'' and provide test harnesses or reference implementations, and let synthesis tools create program fragments that fill the holes such that the resulting complete program has the desired functionality. Traditional solutions to the sketching problem perform a translation to SAT and employ CEGIS. While effective for a range of programs, when applied to real applications, such translation-based approaches have a key limitation: they require either translating all relevant libraries that are invoked directly or indirectly by the given sketch -- which can lead to impractical SAT problems -- or creating models of those libraries -- which can require much manual effort.

Bounded exhaustive testing is an effective methodology for detecting bugs in a wide range of applications. A well-known approach for bounded exhaustive testing is Korat. It generates all test inputs, up to a given small size, based on a formal specification that is written as an executable predicate and characterizes properties of desired inputs. Korat uses the predicate's executions on candidate inputs to implement a backtracking search based on pruning to systematically explore the space of all possible inputs and generate only those that satisfy the specification. This paper presents a novel approach for speeding up test generation for bounded exhaustive testing using Korat. The novelty of our approach is two-fold. One, we introduce a new technique for writing the specification predicate based on an abstract representation of candidate inputs, so that the predicate executes directly on these abstract structures and each execution has a lower cost. Two, we use the abstract representation as the basis to define the first technique for utilizing GPUs for systematic test generation using executable predicates. Moreover, we present a suite of optimizations that enable effective utilization of the computational resources offered by modern GPUs. We use our prototype tool KoratG to experimentally evaluate our approach using a suite of 7 data structures that were used in prior studies on bounded exhaustive testing. Our results show that our abstract representation can speed up test generation by 5.68 times on a standard CPU, while execution on a GPU speeds up the execution, on average, by 17.46 times.

Debugging remains costly and tedious, especially for code that performs intricate operations that are conceptually complex to reason about. We present MLR, a novel approach for repairing faults in such operations, specifically in the context of complex data structures. Our focus is on faults in conditional statements. Our insight is that an integrated approach based on machine learning and systematic path exploration can provide effective repairs. MLR mines the data-spectra of the passing and failing executions of conditional branches to prune the search space for repair and generate patches that are likely valid beyond the existing test-suite. We apply MLR to repair faults in small but complex data structure subjects to demonstrate its efficacy. Experimental results show that MLR has the potential to repair this fault class more effectively than state-of-the-art repair tools.

Software testing is one of the most widely used approaches for improving software reliability. The effectiveness of testing depends to a large extent on the quality of test suites. Researchers have developed various techniques to evaluate the quality of test suites. Of these techniques, mutation testing is generally considered to be the most advanced but also expensive. A key result of applying mutation testing to a given test suite is the mutation score representing the percentage of mutants killed by the test suite. Ideally the mutation score is computed ignoring the mutants that are semantically equivalent to the original code under test or to one another. In this paper, we investigate a new perspective on mutation testing: evaluating how standard compiler optimizations affect the cost and results of mutation testing performed at the compiler intermediate representation. Our study targets LLVM, a popular compiler infrastructure that supports multiple source and target languages. Our evaluation on 18 Coreutils programs discovers several interesting relations between the numbers of mutants (including the numbers on equivalent and duplicated mutants) and mutation scores on unoptimized and optimized programs.

Despite recent progress in automated test generation research, significant challenges remain for applying these techniques on large-scale software systems. These systems under test often require structurally complex test inputs within a large input domain. It is challenging to automatically generate a reasonable number of tests that are both legal and behaviorally-diverse to exercise these systems. Constraint-based test generation is an effective approach for generating structurally complex inputs for systematic testing. While this approach can typically generate large numbers of tests, it has limited scalability – tests generated are usually only up to a small bound on input size. Combinatorial test generation, e.g., pair-wise testing, is a more scalable approach but is challenging to apply on commercial software systems that require complex input structures that cannot be formed by using arbitrary combinations. This paper introduces comKorat, which unifies constraint-based generation of structurally complex tests with combinatorial testing. Specifically, comKorat integrates Korat and ACTS test generators to generate test suites for large scale software systems with structurally complex test inputs. We have successfully applied comKorat on four software applications developed at eBay and Yahoo!. The experimental results show that comKorat outperforms existing solutions in execution time and test coverage. Furthermore, comKorat found a total of 59 previously unknown bugs in the four applications.

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

Regression testing is widely used in practice for validating program changes. However, running large regression suites can be costly. Researchers have developed several techniques for prioritizing tests such that the higher-priority tests have a higher likelihood of finding bugs. A vast majority of these techniques are based on dynamic analysis, which can be precise but can also have significant overhead (e.g., for program instrumentation and test-coverage collection). We introduce a new approach, REPiR, to address the problem of regression test prioritization by reducing it to a standard Information Retrieval problem such that the differences between two program versions form the query and the tests constitute the document collection. REPiR does not require any dynamic profiling or static program analysis. As an enabling technology we leverage the open-source IR toolkit Indri. An empirical evaluation using eight open-source Java projects shows that REPiR is computationally efficient and performs better than existing (dynamic or static) techniques for the majority of subject systems.

Systematic testing plays a vital role in increasing software reliability. A particularly effective and popular approach for systematic testing is symbolic execution, which analyzes a large number of program behaviors using symbolic inputs. Even though symbolic execution is among the most studied analyses during the last decade, scaling it to real-world applications remains a key challenge. This paper studies how a class of semantics-preserving program transformations, namely compiler optimizations, which are designed to enhance performance of standard program execution (using concrete inputs), influence traditional symbolic execution. As an enabling technology, the study uses KLEE, a well-known symbolic execution engine based on the LLVM compiler infrastructure, and focuses on 33 optimization flags of LLVM. Our specific research questions include: (1) how different optimizations influence the performance of symbolic execution for Unix Coreutils, (2) how the influence varies across two different program classes, and (3) how the influence varies across three different back-end constraint solvers. Some of our findings surprised us. For example, applying the 33 optimizations in a pre-defined order provides a slowdown (compared to applying no optimization) for a majority of the Coreutils when using the basic depth-first search with no constraint caching. The key finding of our work is that standard compiler optimizations need to be used with care when performing symbolic execution for creating tests that provide high code coverage. We hope our study motivates future research on harnessing the power of symbolic execution more effectively for enhancing software reliability, e.g., by designing program transformations specifically to scale symbolic execution or by studying broader classes of traditional compiler optimizations in the context of different search heuristics, memoization, and other strategies employed by modern symbolic execution tools.

Understanding the severity of reported bugs is important in both research and practice. In particular, a number of recently proposed mining-based software engineering techniques predict bug severity, bug report quality, and bug-fix time, according to this information. Many bug tracking systems provide a field "severity" offering options such as "severe", "normal", and "minor", with "normal" as the default. However, there is a widespread perception that for many bug reports the label "normal" may not reflect the actual severity, because reporters may overlook setting the severity or may not feel confident enough to do so. In many cases, researchers ignore "normal" bug reports, and thus overlook a large percentage of the reports provided. On the other hand, treating them all together risks mixing reports that have very diverse properties. In this study, we investigate the extent to which "normal" bug reports actually have the "normal" severity. We find that many "normal" bug reports in practice are not normal. Furthermore, this misclassification can have a significant impact on the accuracy of mining-based tools and studies that rely on bug report severity information.

A software product line (SPL) is a family of programs that are differentiated by features --- increments in functionality. Systematically testing an SPL is challenging because it requires running each test of a test suite against a combinatorial number of programs. Feature models capture dependencies among features and can (1) reduce the space of programs to test and (2) enable accurate categorization of failing tests as failures of programs or the tests themselves, not as failures due to illegal combinations of features. In practice, sadly, feature models are not always available.

Context Bug fixing is an integral part of software development and maintenance. A large number of bugs often indicate poor software quality, since buggy behavior not only causes failures that may be costly but also has a detrimental effect on the user’s overall experience with the software product. The impact of long lived bugs can be even more critical since experiencing the same bug version after version can be particularly frustrating for user. While there are many studies that investigate factors affecting bug fixing time for entire bug repositories, to the best of our knowledge, none of these studies investigates the extent and reasons of long lived bugs. Objective In this paper, we investigate the triaging and fixing processes of long lived bugs so that we can identify the reasons for delay and improve the overall bug fixing process. Methodology We mine the bug repositories of popular open source projects , and analyze long lived bugs from five different perspectives: their proportion, severity, assignment, reasons, as well as the nature of fixes. Results Our study on seven open-source projects shows that there are a considerable number of long lived bugs in each system and over 90% of them adversely affect the user’s experience. The reasons for these long lived bugs are diverse including long assignment time, not understanding their importance in advance, etc. However, many bug-fixes were delayed without any specific reasons. Furthermore, 40% of long lived bugs need only small fixes. Conclusion Our overall results suggest that a significant number of long lived bugs may be minimized through careful triaging and prioritization if developers could predict their severity, change effort, and change impact in advance. We believe our results will help both developers and researchers better to understand factors behind delays, improve the overall bug fixing process, and investigate analytical approaches for prioritizing bugs based on bug severity as well as expected bug fixing effort.

Database-centric programs form the backbone of many enterprise systems. Fixing defects in such programs takes much human effort due to the interplay between imperative code and database-centric logic. This paper presents a novel data-driven approach for automated fixing of bugs in the selection condition of database statements (e.g., WHERE clause of SELECT statements) – a common form of bugs in such programs. Our key observation is that in real-world data, there is information latent in the distribution of data that can be useful to repair selection conditions efficiently. Given a faulty database program and input data, only a part of which induces the defect, our novelty is in determining the correct behavior for the defect-inducing data by taking advantage of the information revealed by the rest of the data. We accomplish this by employing semi-supervised learning to predict the correct behavior for defect-inducing data and by patching up any inaccuracies in the prediction by a SAT-based combinatorial search. Next, we learn a compact decision tree for the correct behavior, including the correct behavior on the defect-inducing data. This tree suggests a plausible fix to the selection condition. We demonstrate the feasibility of our approach on seven realworld examples.

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

Localizing bugs is important, difficult, and expensive, especially for large software projects. To address this problem, information retrieval (IR) based bug localization has increasingly been used to suggest potential buggy files given a bug report. To date, researchers have proposed a number of IR techniques for bug localization and empirically evaluated them to understand their effectiveness. However, virtually all of the evaluations have been limited to the projects written in object-oriented programming languages, particularly Java. Therefore, the effectiveness of these techniques for other widely used languages such as C is still unknown. In this paper, we create a benchmark dataset consisting of more than 7,500 bug reports from five popular C projects and rigorously evaluate our recently introduced IR-based bug localization tool using this dataset. Our results indicate that although the IR-relevant properties of C and Java programs are different, IR-based bug localization in C software at the file level is overall as effective as in Java software. However, we also find that the recent advance of using program structure information in performing bug localization gives less of a benefit for C software than for Java software.

As the use of mobile devices becomes increasingly ubiquitous, the need for systematically testing applications (apps) that run on these devices grows more and more. However, testing mobile apps is particularly expensive and tedious, often requiring substantial manual effort. While researchers have made much progress in automated testing of mobile apps during recent years, a key problem that remains largely untracked is the classic oracle problem, i.e., to determine the correctness of test executions. This paper presents a novel approach to automatically generate test cases, that include test oracles, for mobile apps. The foundation for our approach is a comprehensive study that we conducted of real defects in mobile apps. Our key insight, from this study, is that there is a class of features that we term user-interaction features, which is implicated in a significant fraction of bugs and for which oracles can be constructed - in an application agnostic manner -- based on our common understanding of how apps behave. We present an extensible framework that supports such domain specific, yet application agnostic, test oracles, and allows generation of test sequences that leverage these oracles. Our tool embodies our approach for generating test cases that include oracles. Experimental results using 6 Android apps show the effectiveness of our tool in finding potentially serious bugs, while generating compact test suites for user-interaction features.

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

We present a novel technique for producing bounded exhaustive test suites from hybrid invariants, i.e., invariants that are expressed imperatively, declaratively, or as a combination of declarative and imperative predicates. Hybrid specifications are processed using known mechanisms for the imperative and declarative parts, but combined in a way that enables us to exploit information from the declarative side, such as tight bounds computed from the declarative specification, to improve the search both on the imperative and declarative sides. Moreover, our technique automatically evaluates different possible ways of processing the imperative side, and the alternative settings (imperative or declarative) for parts of the invariant available both declaratively and imperatively, to decide the most convenient invariant configuration with respect to efficiency in test generation. This is achieved by transcoping, i.e., by assessing the efficiency of the different alternatives on small scopes (where generation times are negligible), and then extrapolating the results to larger scopes.

Modern network security rests on the Secure Sockets Layer (SSL) and Transport Layer Security (TLS) protocols. Distributed systems, mobile and desktop applications, embedded devices, and all of secure Web rely on SSL/TLS for protection against network attacks. This protection critically depends on whether SSL/TLS clients correctly validate X.509 certificates presented by servers during the SSL/TLS handshake protocol. We design, implement, and apply the first methodology for large-scale testing of certificate validation logic in SSL/TLS implementations. Our first ingredient is "frankencerts," synthetic certificates that are randomly mutated from parts of real certificates and thus include unusual combinations of extensions and constraints. Our second ingredient is differential testing: if one SSL/TLS implementation accepts a certificate while another rejects the same certificate, we use the discrepancy as an oracle for finding flaws in individual implementations. Differential testing with frankencerts uncovered 208 discrepancies between popular SSL/TLS implementations such as OpenSSL, NSS, CyaSSL, GnuTLS, PolarSSL, MatrixSSL, etc. Many of them are caused by serious security vulnerabilities. For example, any server with a valid X.509 version 1 certificate can act as a rogue certificate authority and issue fake certificates for any domain, enabling man-in-the-middle attacks against MatrixSSL and GnuTLS. Several implementations also accept certificate authorities created by unauthorized issuers, as well as certificates not intended for server authentication. We also found serious vulnerabilities in how users are warned about certificate validation errors. When presented with an expired, self-signed certificate, NSS, Safari, and Chrome (on Linux) report that the certificate has expired-a low-risk, often ignored error-but not that the connection is insecure against a man-in-the-middle attack. These results demonstrate that automated adversarial testing with frankencerts is a powerful methodology for discovering security flaws in SSL/TLS implementations.

Writing declarative models of software designs and analyzing them to detect defects is an effective methodology for developing more dependable software systems. However, writing such models correctly can be challenging for practitioners who may not be proficient in declarative programming, and their models themselves may be buggy. We introduce the foundations of a novel test automation framework, AUnit, which we envision for testing declarative models written in Alloy -- a first-order, relational language that is supported by its SAT-based analyzer. We take inspiration from the success of the family of xUnit frameworks that are used widely in practice for test automation, albeit for imperative or object-oriented programs. The key novelty of our work is to define a basis for unit testing for Alloy, specifically, to define the concepts of test case and coverage, and coverage criteria for declarative models. We reduce the problems of declarative test execution and coverage computation to evaluation without requiring SAT solving. Our vision is to blend how developers write unit tests in commonly used programming languages with how Alloy users formulate their models in Alloy, thereby facilitating the development and testing of Alloy models for both new Alloy users as well as experts. We illustrate our ideas using a small but complex Alloy model. While we focus on Alloy, our ideas generalize to other declarative languages (such as Z, B, ASM).

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

Modern IDEs make many software engineering tasks easier by automating functionality such as code completion and navigation. However, this functionality operates on one version of the code at a time. We envision a new approach that makes code completion and navigation aware of code evolution and enables them to operate on multiple versions at a time, without having to manually switch across these versions. We illustrate our approach on several example scenarios. We also describe a prototype Eclipse plugin that embodies our approach for code completion and navigation for Java code. We believe our approach opens a new line of research that adds a novel, temporal dimension for treating code in IDEs in the context of tasks that previously required manual switching across different code versions.

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

Mutation testing is a well-known but costly approach for determining test adequacy. The central idea behind the approach is to generate mutants, which are small syntactic transformations of the program under test, and then to measure for a given test suite how many mutants it kills. A test t is said to kill a mutant m of program p if the output of t on m is different from the output of t on p. The effectiveness of mutation testing in determining the quality of a test suite relies on the ability to apply it using a large number of mutants. However, running many tests against many mutants is time consuming. We present a family of techniques to reduce the cost of mutation testing by prioritizing and reducing tests to more quickly determine the sets of killed and non-killed mutants. Experimental results show the effectiveness and efficiency of our techniques.

We present a novel approach for parallel analysis of models written in Alloy, a declarative extension of first-order logic based on relations. The Alloy language is supported by the fully automatic Alloy Analyzer, which translates models into propositional formulas and uses off-the-shelf SAT technology to solve them. Our key insight is that the underlying constraint satisfaction problem can be split into subproblems of lesser complexity by using ranges of candidate solutions, which partition the space of all candidate solutions. Conceptually, we define a total ordering among the candidate solutions, split this space of candidates into ranges, and let independent SAT searches take place within these ranges' endpoints. Our tool, Ranger, embodies our insight. Experimental evaluation shows that Ranger provides substantial speedups (in several cases, superlinear ones) for a variety of hard-to-solve Alloy models, and that adding more hardware reduces analysis costs almost linearly.

Locating bugs is important, difficult, and expensive, particularly for large-scale systems. To address this, natural language information retrieval techniques are increasingly being used to suggest potential faulty source files given bug reports. While these techniques are very scalable, in practice their effectiveness remains low in accurately localizing bugs to a small number of files. Our key insight is that structured information retrieval based on code constructs, such as class and method names, enables more accurate bug localization. We present BLUiR, which embodies this insight, requires only the source code and bug reports, and takes advantage of bug similarity data if available. We build BLUiR on a proven, open source IR toolkit that anyone can use. Our work provides a thorough grounding of IR-based bug localization research in fundamental IR theoretical and empirical knowledge and practice. We evaluate BLUiR on four open source projects with approximately 3,400 bugs. Results show that BLUiR matches or outperforms a current state-of-the-art tool across applications considered, even when BLUiR does not use bug similarity data used by the other tool.

Mutation testing is a powerful methodology for evaluating the quality of a test suite. However, the methodology is also very costly, as the test suite may have to be executed for each mutant. Selective mutation testing is a well-studied technique to reduce this cost by selecting a subset of all mutants, which would otherwise have to be considered in their entirety. Two common approaches are operator-based mutant selection, which only generates mutants using a subset of mutation operators, and random mutant selection, which selects a subset of mutants generated using all mutation operators. While each of the two approaches provides some reduction in the number of mutants to execute, applying either of the two to medium-sized, real-world programs can still generate a huge number of mutants, which makes their execution too expensive. This paper presents eight random sampling strategies defined on top of operator-based mutant selection, and empirically validates that operator-based selection and random selection can be applied in tandem to further reduce the cost of mutation testing. The experimental results show that even sampling only 5% of mutants generated by operator-based selection can still provide precise mutation testing results, while reducing the average mutation testing time to 6.54% (i.e., on average less than 5 minutes for this study).

This paper presents a novel methodology for localizing faults in code as it evolves. Our insight is that the essence of failure-inducing edits made by the developer can be captured using mechanical program transformations (e.g., mutation changes). Based on the insight, we present the FIFL framework, which uses both the spectrum information of edits (obtained using the existing FaultTracer approach) as well as the potential impacts of edits (simulated by mutation changes) to achieve more accurate fault localization. We evaluate FIFL on real-world repositories of nine Java projects ranging from 5.7KLoC to 88.8KLoC. The experimental results show that FIFL is able to outperform the state-of-the-art FaultTracer technique for localizing failure-inducing program edits significantly. For example, all 19 FIFL strategies that use both the spectrum information and simulated impact information for each edit outperform the existing FaultTracer approach statistically at the significance level of 0.01. In addition, FIFL with its default settings outperforms FaultTracer by 2.33% to 86.26% on 16 of the 26 studied version pairs, and is only inferior than FaultTracer on one version pair.

Many programs can be configured through dynamic and/or static selection of configuration variables. A software product line (SPL), for example, specifies a family of programs where each program is defined by a unique combination of features. Systematically testing SPL programs is expensive as it can require running each test against a combinatorial number of configurations. Fortunately, a test is often independent of many configuration variables and need not be run against every combination. Configurations that are not required for a test can be pruned from execution. This paper presents SPLat, a new way to dynamically prune irrelevant configurations: the configurations to run for a test can be determined during test execution by monitoring accesses to configuration variables. SPLat achieves an optimal reduction in the number of configurations and is lightweight compared to prior work that used static analysis and heavyweight dynamic execution. Experimental results on 10 SPLs written in Java show that SPLat substantially reduces the total test execution time in many cases. Moreover, we demonstrate the scalability of SPLat by applying it to a large industrial code base written in Ruby on Rails.

SUMMARY Detecting faults in evolving systems is important. Change impact analysis has been shown to be effective for finding faults during software evolution. For example, Chianti represents program edits as atomic changes, selects affected tests, and determines a subset of affecting changes that might have caused test failures. However, the number of affecting changes related to each test failure in practice may still be overwhelming for manual inspection. In this paper, we present a novel approach, FaultTracer, which ranks program edits according to their suspiciousness to reduce developer effort in manually inspecting affecting changes. FaultTracer adapts spectrum‐based fault localization techniques, which assume the statements that are primarily executed by failed tests are more suspicious, and applies them in tandem with an enhanced change impact analysis to identify failure‐inducing edits more precisely. We conducted an experimental study using 23 real versions of four real‐world Java programs from the Software Infrastructure Repository. The experimental results show that FaultTracer localizes a real regression fault within top three atomic changes for 14 out of 22 studied real failures. When ranking only method‐level changes, compared to the existing ranking heuristic, FaultTracer reduces the number of changes to be manually inspected by more than 50% on the data set of real regression faults, and by more than 60% on the data set of seeded faults. The fault localization component of FaultTracer is 80% more effective than traditional spectrum‐based fault localization, and enables similar benefits when using either our enhanced change impact analysis or Chianti. The runtime overhead for FaultTracer to collect extended call graphs is 49.83 s for each subject on average and is only 8.26% more than that for Chianti to collect traditional call graph information. Copyright © 2013 John Wiley & Sons, Ltd.

Dynamically allocated data structures pervade imperative and object-oriented programs. Automated analysis and testing of such programs requires reasoning about their data structures. The structures often have complex structural properties, such as a cyclicity of the object graph rooted at a given pointer. Such properties pose a challenge for automated reasoning. Shape analysis is a class of techniques that address reasoning about such programs. Traditionally, shape analysis is performed using static analysis of the program code. More recently, dynamic techniques for shape analysis have been developed, which inspect program states to identify properties of data structures. This paper presents a novel dynamic technique, which adapts well-studied results from graph theory to determine the shape of the program's key data structures. Specifically, spectral graph theory, a field that studies the properties of a graph in relation to the properties of matrices based on the graph, e.g., eigen values of its adjacency matrix, provides the foundational ideas. Experimental results using a suite of data structures demonstrate the potential the technique holds in identifying data structure properties and detecting likely erroneous program states.

Constraint-based testing is a methodology for finding bugs in code, which has been successfully used for testing real systems. A key element of the methodology is generation of test inputs from input constraints, i.e., properties of desired inputs, which is performed by solving the constraints. We present a novel approach to optimize input generation from imperative constraints, i.e., constraints written as predicates in an imperative language. A well known technique for solving such constraints is execution-driven monitoring, where the given predicate is executed on candidate inputs to filter and prune invalid inputs, and generate valid ones. Our insight is that a lightweight static data-flow analysis of the given imperative constraint can enable more efficient solving. This paper describes an approach that embodies our insight and evaluates it using a suite of well-studied subject constraints. The experimental results show our approach provides substantial speedup over previous work.

A software product line (SPL) is a family of related programs, each of which is uniquely defined by a combination of features. Testing an SPL requires running each of its programs, which may be computationally expensive as the number of programs in an SPL is potentially exponential in the number of features. It is also wasteful since instructions common to many programs must be repeatedly executed, rather than just once. To reduce this waste, we propose the idea of shared execution, which runs instructions just once for a set of programs until a variable read yields multiple values, causing execution to branch for each value until a common execution point that allows shared execution to resume. Experiments show that shared execution can be faster than conventionally running each program from start to finish, despite its overhead.

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

Mutation testing is one of the most powerful approaches for evaluating quality of test suites. However, mutation testing is also one of the most expensive testing approaches. This paper presents Regression Mutation Testing (ReMT), a new technique to speed up mutation testing for evolving systems. The key novelty of ReMT is to incrementally calculate mutation testing results for the new program version based on the results from the old program version; ReMT uses a static analysis to check which results can be safely reused. ReMT also employs a mutation-specific test prioritization to further speed up mutation testing. We present an empirical study on six evolving systems, whose sizes range from 3.9KLoC to 88.8KLoC. The empirical results show that ReMT can substantially reduce mutation testing costs, indicating a promising future for applying mutation testing on evolving software systems.

Fault localization i.e., locating faulty lines of code, is a key step in removing bugs and often requires substantial manual effort. Recent years have seen many automated localization techniques, specifically using the program’s passing and failing test runs, i.e., test spectra. However, the effectiveness of these approaches is sensitive to factors such as the type and number of faults, and the quality of the test-suite. This paper presents a novel technique that applies spectra-based localization in synergy with specification-based analysis to more accurately locate faults. Our insight is that unsatisfiability analysis of violated specifications, enabled by SAT technology, could be used to (1) compute unsatisfiable cores that contain likely faulty statements and (2) generate tests that help spectra-based localization. Our technique is iterative and driven by a feedback loop that enables more precise fault localization. SAT-TAR is a framework that embodies our technique for Java programs, including those with multiple faults. An experimental evaluation using a suite of widely-studied data structure programs, including the ANTLR and JTopas parser applications, shows that our technique localizes faults more accurately than state-of-the-art approaches.

This paper introduces a novel approach to scale symbolic execution --- a program analysis technique for systematic exploration of bounded execution paths---for test input generation. While the foundations of symbolic execution were developed over three decades ago, recent years have seen a real resurgence of the technique, specifically for systematic bug finding. However, scaling symbolic execution remains a primary technical challenge due to the inherent complexity of the path-based exploration that lies at core of the technique.

Constraint-based input generation is an effective technique for testing programs, such as compilers and web browsers, which have complex inputs. However, efficient generation of such inputs remains a challenging problem. We present a novel input generation technique that takes constraints written as recursive predicates in the underlying programming language and uses dynamic programming to solve the constraints efficiently. Our key insight is to leverage the recursive structure of desired inputs and partition the problem of generating an input into several sub-problems of generating smaller inputs that exhibit the same structure, and then to use dynamic programming -- a well-known problem solving methodology designed to exploit common sub-problems -- to combine them. A lazy initialization strategy and symbolic execution optimize our basic technique. Our technique provides not only bounded exhaustive input generation but also enables random input generation. We show the correctness of our technique. Furthermore, we present an experimental evaluation, which shows that our technique can provide over an order of magnitude performance improvement for input generation compared to Korat (an efficient solver for structural constraints) and Pex (a state-of-the-art tool for symbolic execution). Finally, we use our technique to effectively find bugs in production versions of Google Chrome and Apple Safari web browsers.

Keeping evolving software fault-free is hard. In our previous work, we proposed FaultTracer, a change impact and regression fault analysis tool for evolving programs. It takes the old and new versions of a program and a regression test suite as inputs, and then identifies affected tests---a subset of tests relevant to the program differences between the two versions and affecting changes---a subset of atomic changes relevant to each affected test. It adapts spectrum-based fault localization techniques and applies them in tandem with an enhanced change impact analysis to identify and rank failure-inducing program edits. We have shown that FaultTracer, compared to existing techniques (e.g., Chianti), achieves improvement in selecting influenced tests, determining suspicious failure-inducing edits, and ranking failure-inducing program edits. In this paper, we show the design, implementation, and demonstration of our FaultTracer approach as a publicly available toolkit for testing and debugging Java programs.

We present results for the "Impact Project Focus Area" on the topic of symbolic execution as used in software testing. Symbolic execution is a program analysis technique introduced in the 70s that has received renewed interest in recent years, due to algorithmic advances and increased availability of computational power and constraint solving technology. We review classical symbolic execution and some modern extensions such as generalized symbolic execution and dynamic test generation. We also give a preliminary assessment of the use in academia, research labs, and industry.

Keeping evolving systems fault free is hard. Change impact analysis is a well-studied methodology for finding faults in evolving systems. For example, in order to help developers identify failure-inducing edits, Chianti extracts program edits as atomic changes between different program versions, selects affected tests, and determines a subset of those changes that might induce test failures. However, identifying real regression faults is challenging for developers since the number of affecting changes related to each test failure may still be too large for manual inspection. This paper presents a novel approach FAULTTRACER which ranks program edits in order to reduce developers' effort in manually inspecting all affecting changes. FAULTTRACER adapts spectrum-based fault localization techniques and applies them in tandem with an enhanced change impact analysis that uses Extended Call Graphs to identify failure-inducing edits more precisely. We evaluate FAULTTRACER using 23 versions of 4 real-world Java programs from the Software Infrastructure Repository. The experimental results show that FAULTTRACER outperforms Chianti in selecting affected tests (slightly better, but handles safety problems of Chianti) as well as in determining affecting changes (with an improvement of approximately 20%). By ranking the affecting changes using spectrum-based test behavior profile, for 14 out of 22 studied failures, FAULTTRACER places a real regression fault within top 3 atomic changes, significantly reducing developers' effort in inspecting potential failure-inducing edits.

We describe an automated approach for systematic black-box testing of database management systems (DBMS) using a relational constraint solver. We reduce the problem of automated database testing into generating three artifacts: (1) SQL queries for testing, (2) meaningful input data to populate test databases, and (3) expected results of executing the queries on the generated data. We leverage our previous work on ADUSA and the Automated SQL Query Generator to form high-quality test suites for testing DBMS engines. This paper presents a detailed description of our framework for Automated SQL Query Generation using the Alloy tool-set, and experimental results of testing database engines using our framework. We show how the main SQL grammar constraints can be solved by translating them to Alloy constraints to generate semantically and syntactically correct SQL queries. We also present experimental results of combining ADUSA and the Automated SQL Query Generator, and applying our framework to test the Oracle 11g database. Our framework generated 5 new queries, which reveal erroneous behavior of Oracle 11g.

Developers have used data structure repair over the last few decades as an effective means to recover on-the-fly from errors in program state. Traditional repair techniques were based on dedicated repair routines, whereas more recent techniques have used invariants that describe desired structural properties as the basis for repair. All repair techniques are designed with one primary goal: run-time error recovery. However, the actions that any such technique performs to repair an erroneous program state are meant to produce the effect of the actions of a (hypothetical) correct program. The key insight in this paper is that repair actions on the program state can guide debugging of code (when the erroneous program execution is due to a fault in the program and not an external event).This paper presents an approach that abstracts concrete repair actions that a routine performs to repair an erroneous state into a sequence of program statements that perform the same actions using variables visible in the scope of the faulty code. Thus, appending the generated statements to the original code is akin to performing the repair from within the program. Our implementation uses the Juzi data structure repair tool as an enabling technology. Experimental results using a library data structure as well as two applications demonstrate the effectiveness of our approach in enabling repair of faulty code.

The last decade has seen many advances in test input generation, specifically using systematic approaches that can enumerate many tests. While such approaches have enhanced our ability to find bugs in programs, running large numbers of tests remains a time consuming and expensive task, especially for tests that execute operations on external resources, such as a file system or a network. This paper presents a novel technique for optimizing execution of suites of tests, where several tests in a suite may contain common initial execution -- a property often exhibited by systematically generated suites, e.g., those for bounded exhaustive testing. Our insight is that we can cluster execution of such tests by defining abstract-level undo operations, which allow a common execution segment to be performed once, and its result to be shared across the tests, which then perform the rest of their operations. We present our framework for clustered execution of test suites, and evaluate it using three case-studies, which show our technique enables significant performance speed-up over traditional test execution.

As test suites grow larger during software evolution, regression testing becomes expensive. To reduce the cost of regression testing, test-suite reduction aims to select a minimal subset of the original test suite that can still satisfy all the test requirements. While traditional test-suite reduction techniques were intensively studied on C programs with specially generated test suites, there are limited studies for test-suite reduction on programs with real-world test suites. In this paper, we investigate test-suite reduction techniques on Java programs with real-world JUnit test suites. We implemented four representative test-suite reduction techniques for JUnit test suites. We performed an empirical study on 19 versions of four real-world Java programs, ranging from 1.89 KLoC to 80.44 KLoC. Our study investigates both the benefits and the costs of test-suite reduction. The results show that the four traditional test-suite reduction techniques can effectively reduce these JUnit test suites without substantially reducing their fault-detection capability. Based on the results, we provide a guideline for achieving cost-effective JUnit test suite reduction.

Alloy is a declarative modelling language based on first-order logic with sets and relations. Alloy formulas are checked for satisfiability by the fully automatic Alloy Analyzer. The analyzer, given an Alloy formula and a scope, i.e. a bound on the universe of discourse, searches for an instance i.e. a valuation to the sets and relations in the formula, such that it evaluates to true. The analyzer translates the Alloy problem to a propositional formula for which it searches a satisfying assignment via an off-the-shelf propositional satisfiability (SAT) solver. The SAT solver performs an exhaustive search and increasing the scope leads to the combinatorial explosion problem. We envision annotations, a meta-data facility used in imperative languages, as a means of augmenting Alloy models to enable more efficient analysis by specifying the priority, i.e. order of solving, of a given constraint and the slover to be used. This additional information would enable using the solutions to a particular constraint as partial solutions to the next in case constraint priority is specified and using a specific solver for reasoning about a given constraint in case a constraint solver is specified.

The use of specifications provides an effective technique to automate testing. A form of specification that automates generation of test inputs is logical constraints that define properties of desired inputs. Recent advances in constraint solving technology have made the use of constraints particularly attractive. However, manually writing constraints to define complex inputs to real-world programs can pose a significant burden on the user and restrict their wider use. We envision a novel approach to facilitate the use of constraints: to provide a mixed notation for writing the properties. Our key insight is that different properties can lend to easier formulation using different programming paradigms. Thus, a notation that supports more than one paradigm, e.g., declarative and imperative paradigms, can enable achieving a sweet-spot in minimizing the manual effort required in constraint formulation. Moreover, solving such constraints is also likely to be more efficient as different properties may require different paradigms for more direct and accurate representation. This paper presents our vision and gives an illustration to make a case for the usefulness of such a notation.

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

We present an approach for describing tests using non-deterministic test generation programs. To write such programs, we introduce UDITA, a Java-based language with non-deterministic choice operators and an interface for generating linked structures. We also describe new algorithms that generate concrete tests by efficiently exploring the space of all executions of non-deterministic UDITA programs.

We present a novel approach to optimize incremental scope-bounded checking of programs using a relational constraint solver. Given a program and its correctness specification, scope-bounded checking encodes control-flow and data-flow of bounded code segments into declarative formulas and uses constraint solvers to search for correctness violations. For non-trivial programs, the formulas are often complex and represent a heavy workload that can choke the solvers. To scale scope-bounded checking, our previous work introduced an incremental approach that uses the program's control-flow as a basis of partitioning the program and generating several sub-formulas, which represent simpler problem instances for the underlying solvers. This paper introduces a new approach that uses the program's dataflow, specifically variable-definitions, as a basis for incremental checking. Experimental results show that the use of data-flow provides a significant reduction in the number of variables in the encoded formulas over the previous control-flow-based approach, thereby further improving scalability of scopebounded checking.

We present a novel approach for generating syntactically and semantically correct SQL queries as inputs for testing relational databases. We leverage the SAT-based Alloy tool-set to reduce the problem of generating valid SQL queries into a SAT problem. Our approach translates SQL query constraints into Alloy models, which enable it to generate valid queries that cannot be automatically generated using conventional grammar-based generators.

A Software Product Line (SPL) is a family of programs where each program is defined by a unique combination of features. Developing a set of programs with commonalities and variabilities in this way can significantly reduce both the time and cost of software development. However, as the number of programs may be exponential in the number of features, testing an SPL, the phase to which the majority of software development is dedicated, becomes especially challenging [12].

Recent advances in mechanical techniques for systematic testing have increased our ability to automatically find subtle bugs, and hence, to deploy more dependable software. This paper builds on one such systematic technique, scope-bounded testing, to develop a novel specification-based approach for efficiently generating tests for products in a software product line. Given properties of features as first-order logic formulas in Alloy, our approach uses SAT-based analysis to automatically generate test inputs for each product in a product line. To ensure soundness of generation, we introduce an automatic technique for mapping a formula that specifies a feature into a transformation that defines incremental refinement of test suites. Our experimental results using different data structure product lines show that an incremental approach can provide an order of magnitude speedup over conventional techniques. We also present a further optimization using dedicated integer constraint solvers for feature properties that introduce integer constraints, and show how to use a combination of solvers in tandem for solving Alloy formulas.

Java PathFinder (JPF) is a popular model checker for Java programs. JPF was used to generate object graphs as test inputs for object-oriented programs. Specifically, JPF was used as an implementation engine for the Korat algorithm. Korat takes two inputs---a Java predicate that encodes properties of desired object graphs and a bound on the size of the graph---and generates all graphs (within the given bound) that satisfy the encoded properties. Korat uses a systematic search to explore the bounded state space of object graphs. Korat search was originally implemented in JPF using a simple instrumentation of the Java predicate. However, JPF is a general-purpose model checker and such direct implementation results in an unnecessarily slow search. We present our results on speeding up Korat search in JPF. The experiments on ten data structure subjects show that our modifications of JPF reduce the search time by over an order of magnitude.

Constraint solving lies at the heart of several specification-based approaches to automated testing. Korat is a previously developed algorithm for solving constraints in Java programs. Given a Java predicate that represents the desired constraints and a bound on the input size, Korat systematically explores the bounded input space of the predicate and enumerates inputs that satisfy the constraint. Korat search is largely sequential: it considers one candidate input in each iteration and it prunes the search space based on the candidates considered. This paper presents PKorat, a new parallel algorithm that parallelizes the Korat search. PKorat explores the same state space as Korat but considers several candidates in each iteration. These candidates are distributed among parallel workers resulting in an efficient parallel version of Korat. Experimental results using complex structural constraints from a variety of subject programs show significant speedups over the traditional Korat search.

Automated debugging is becoming increasingly important as the size and complexity of software increases. This paper makes a case for using constraint-based data structure repair, a recently developed technique for fault recovery, as a basis for automated debugging. Data structure repair uses given structural integrity constraints for key data structures to monitor their correctness during the execution of a program. If a constraint violation is detected, repair performs mutations on the data structures, i.e., corrupt program state, and transforms it into another state, which satisfies the desired constraints. The primary goal of data structure repair is to transform an erroneous state into an acceptable state. Therefore, the mutations performed by repair actions provide a basis of debugging faults in code (assuming the errors are due to bugs). A key challenge to embodying this insight into a mechanical technique arises due to the difference in the concrete level of the program states and the abstract level of the program code: repair actions apply to concrete data structures that exist at runtime, whereas debugging applies to code. We observe that static structures (program variables) hold handles to dynamic structures (heap-allocated data), which allows bridging the gap between the abstract and concrete levels. We envision a tool-chain where a data structure repair tool generates repair logs that are used by a fault localization tool and a repair abstraction tool that apply in synergy to not only identify the location of fault(s) in code but also to synthesize debugging suggestions. An embodiment of our vision can significantly reduce the cost of developing reliable software.

Several static analysis techniques, e.g., symbolic execution or scope-bounded checking, as well as dynamic analysis techniques, e.g., specification-based testing, use constraint solvers as an enabling technology. To analyze code that manipulates structurally complex data, the underlying solver must support structural constraints. Solving such constraints can be expensive due to the large number of aliasing possibilities that the solver must consider. This paper presents a novel technique to selectively reduce the number of test cases to be generated. Our technique applies across a class of structural constraint solvers. Experimental results show that the technique enables an order of magnitude reduction in the number of test cases to be considered.

Parallel changes are becoming increasingly prevalent in the development of large scale software system. To further study the relationship between parallel changes and faults, we have designed and implemented a semantic conflict analyzer (SCA) to detect semantic interference between parallel changes. SCA combines data dependency analysis and program slicing. Data dependency analysis can disclose the semantic structure of the program. And program slicing can identify which semantic structures are impacted by a change. By comparing the overlap between impacts of two changes, SCA can detect if there are semantic interference between the two changes. An experiment with an industrial project shows that SCA can detect a significant portion of the faults in highly parallel changes. SCA is effective in predicting faults (based on "direct" semantic interference detection) in changes made within a short time period. SCA is both efficient (averaging less than two minutes) and scalable (requiring only the local context)

This paper describes Juzi, a tool for automatic repair of complex data structures. Juzi takes a Java class representing the data structure as well as a predicate method that specifies the structural integrity constraints as inputs. Juzi instruments its inputs and generates a new Java class which behaves similarly to the original class, yet automatically repairs itself when the structural integrity constraints are violated.

Java PathFinder (JPF) is an explicit-state model checker for Java programs. JPF implements a backtrackable Java Virtual Machine (JVM) that provides non-deterministic choices and control over thread scheduling. JPF is itself implemented in Java and runs on top of a host JVM. JPF represents the JVM state of the program being checked and performs three main operations on this state representation: bytecode execution, state backtracking, and state comparison. This paper summarizes four extensions that we have developed to the JPF state representation and operations. One extension provides a new functionality to JPF, and three extensions improve performance of JPF in various scenarios. Some of our code has already been included in publicly available JPF.

Deryaft is a tool for generating likely representation invariants of structurally complex data. Given a small set of concrete structures, Deryaft analyzes their key characteristics to formulate local and global properties that the structures exhibit. For effective formulation of structural invariants, Deryaft focuses on graph properties, including reachability, and views the program heap as an edge-labeled graph. Deryaft outputs a Java predicate that represents the invariants; the predicate takes an input structure and returns true if and only if it satisfies the invariants.

We present a novel specification-based approach for generating tests for products in a software product line. Given properties of features as first-order logic formulas, our approach uses SAT-based analysis to automatically generate test inputs for each product in a product line. To ensure soundness of generation, we introduce an automatic technique for mapping a formula that specifies a feature into a transformation that defines incremental refinement of test suites. Our experimental results using different data structure product lines show that incremental approach can provide an order of magnitude speed-up over conventional techniques.

Structural constraint solving is being increasingly used for software reliability tasks such as systematic testing or error recovery. For example, the Korat algorithm provides constraint-based test generation: given a Java predicate that describes desired input constraints and a bound on the input size, Korat systematically searches the bounded input space of the predicate to generate all inputs that satisfy the constraints. As another example, the STARC tool uses a constraint-based search to repair broken data structures. A key issue for these approaches is the efficiency of search. This paper presents a novel approach that significantly improves the efficiency of structural constraint solvers. Specifically, most existing approaches use backtracking through code re-execution to explore their search space. In contrast, our approach performs checkpoint-based backtracking by storing partial program states and performing abstract undo operations. The heart of our approach is a light-weight search that is performed purely through code instrumentation. The experimental results on Korat and STARC for generating and repairing a set of complex data structures show an order to two orders of magnitude speed-up over the traditionally used searches.

We present a novel approach for black-box testing of database management systems (DBMS) using the Alloy tool-set. Given a database schema and an SQL query as inputs, our approach first formulates Alloy models for both inputs, and then using the Alloy Analyzer, it generates (1) input data to populate test databases, and (2) the expected result of executing the given query on the generated data. The Alloy Analyzer results form a complete test suite (input/oracle) for verifying the execution result of a DBMS query processor. By incorporating both the schema and the query during the analysis, our approach performs query-aware data generation where executing the query on the generated data produces meaningful non-empty results. We developed a prototype tool, ADUSA, and used it to evaluate our approach. Experimental results show the ability of our approach to detect bugs in both open-source as well as commercial database management systems.

Embedded systems typically consist of a composition of a set of hardware and software IP modules. Each module is heavily optimized by itself. However, when these modules are composed together, significant additional opportunities for optimizations are introduced because only a subset of the entire functionality is actually used. We propose COSE-a technique to jointly optimize such designs. We use symbolic execution to compute invariants in each component of the design. We propagate these invariants as constraints to other modules using global flow analysis of the composition of the design. This captures optimizations that go beyond, and are qualitatively different than, those achievable by compiler optimization techniques such as common subexpression elimination, which are localized. We again employ static analysis techniques to perform optimizations subject to these constraints. We implemented COSE in the Metropolis platform and achieved significant optimizations using reasonable computational resources.

This paper describes the Korat tool for constraint-based generation of structurally complex test inputs for Java programs. Korat takes: (1) an imperative predicate that specifies the desired structural integrity constraints and (2) a finitization that bounds the desired test input size. Korat generates all inputs (within the bounds) for which the predicate returns true. To do so, Korat performs a systematic search of the predicate's input space. The inputs that Korat generates enable bounded-exhaustive testing for programs ranging from library classes to stand-alone applications.

This paper presents Kato, a tool that implements a novel class of optimizations that are inspired by program slicing for imperative languages but are applicable to analyzable declarative languages, such as Alloy. Kato implements a novel algorithm for slicing declarative models written in Alloy and leverages its relational engine KodKodfor analysis. Given an Alloy model, Kato identifies a slice representing the model's core: a satisfying instance for the core can systematically be extended into a satisfying instance for the entire model, while unsatisfiability of the core implies unsatisfiability of the entire model. The experimental results show that for a variety of subject models Kato's slicing algorithm enables an order of magnitude speed-up over Alloy's default translation to SAT.

The alloy tool-set has been gaining popularity as an alternative to traditional manual testing and checking for design correctness. Alloy uses a first-order relational logic for modeling designs. The alloy analyzer translates alloy formulas for a given scope, i.e., a bound on the universe of discourse, to Boolean formulas in conjunctive normal form (CNF), which are subsequently checked using prepositional satisfiability solvers. We present SERA, a novel algorithm that compiles a relational logic formula for a given scope to a sequential circuit. There are two key advantages of sequential circuits: they form a more succinct representation than CNF formulas, sometimes by several orders of magnitude. Also sequential circuits are amenable to a range of powerful automatic analysis techniques that have no counterparts for CNF formulas. Our experiments show that SERA, used in conjunction with a sequential circuit analyzer, can check formulas for scopes that are an order of magnitude higher than those feasible with the alloy analyzer.

Parallel developments are becoming increasingly prevalent in the building and evolution of large-scale software systems. Our previous studies of a large industrial project showed that there was a linear correlation between the degree of parallelism and the likelihood of defects in the changes. To further study the relationship between parallel changes and faults, we have designed and implemented an algorithm to detect "direct" semantic interference between parallel changes. To evaluate the analyzer's effectiveness in fault prediction, we designed an experiment in the context of an industrial project. We first mine the change and version management repositories to find sample versions sets of different degrees of parallelism. We investigate the interference between the versions with our analyzer. We then mine the change and version repositories to find out what faults were discovered subsequent to the analyzed interfering versions. We use the match rate between semantic interference and faults to evaluate the effectiveness of the analyzer in predicting faults. Our contributions in this evaluative empirical study are twofold. First, we evaluate the semantic interference analyzer and show that it is effective in predicting faults (based on "direct" semantic interference detection) in changes made within a short time period. Second, the design of our experiment is itself a significant contribution and exemplifies how to mine software repositories rather than use artificial cases for rigorous experimental evaluations.

Programmers have long used assertions to characterize properties of code. An assertion violation signals a corruption in the programstate. At such a state, it is standard to terminate the program, debug it if possible, and re-execute it. We propose a new view: instead of terminating the program, use the violated assertion as a basis of repairing the state of the program and let it continue.

A number of researchers have proposed the use of Boolean satisfiability solvers for verifying C programs. They encode correctness checks as Boolean formulas using finitization: loops and recursion are bounded, as is the size of the input instances. The SAT approach has been shown to find subtle bugs with reasonable resources. However, it does not scale well; in particular, it lacks the ability to handle larger bounds. We present SEBAC, which can handle the same class of programs as the SAT approach, and scales to bounds that are orders of magnitude higher. The key difference between SEBAC and SAT techniques is SEBAC's use of imperative Boolean sequential circuits, which are Boolean formulas with memory elements instead of the Boolean formulas which are stateless

Data structure corruptions are insidious bugs that reduce the reliability of software systems. Constraint-based datastructure repair promises to help programs recover from potentially crippling corruption errors. Prior work repairs a variety of relatively small data structures, usually with hundreds of nodes.

We present novel algorithms for parallel testing of code that takes structurally complex test inputs. The algorithms build on the Korat algorithm for constraint-based generation of structurally complex test inputs. Given an imperative predicate that specifies the desired structural constraints and a finitization that bounds the desired input size, Korat performs a systematic search to generate all test inputs (within the bounds) that satisfy the constraints. We present how to generate test inputs with a parallel search in Korat and how to execute test inputs in parallel, both off-line (when the inputs are saved on disk) and on-line (when execution immediately follows generation).

This paper presents a specification-based approach for systematic testing of products from a software product line. Our approach uses specifications given as formulas in Alloy, a first-order logic based on relations. Alloy formulas can be checked for satisfiability using the Alloy Analyzer. The fully automatic analyzer, given an Alloy formula and a scope, i.e., a bound on the universe of discourse, searches for an instance, i.e., a valuation to the relations in the formula such that it evaluates to true. The analyzer translates an Alloy formula (for the given scope) to a propositional formula and finds an instance using an off-the-shelf SAT solver. The use of an enumerating solver enables systematic test generation.

We present aDeryaft, a novel technique for automating the writing of specifications in Alloy-a first-order relational logic with transitive closure. Alloy is particularly suitable for specifying structural properties of software, and has steadily been gaining popularity due to the rapid feedback that its SAT-based analyzer provides fully automatically. Alloy users however, still have to manually write specifications in a declarative language and use a paradigm that is different from the commonly used imperative programming paradigm. aDeryaft assists Alloy users in writing their specifications by providing a novel specification-writing approach, which is particularly tailored to users, such as engineers or practitioners in industry, who may not have much prior experience or proficiency in Alloy or similar logics. The user constructs by hand a few small concrete instances that represent the constraints of the software structure they want to specify. aDeryaft then fully automatically generates an executable Alloy specification, which represents the constraints that summarize the given structures. The generated specification is fully executable. For example, the Alloy Analyzer can use it to systematically enumerate a large number of concrete instances that satisfy the same constraints as the given instances. Indeed, a user may use aDeryaft to generate partial specifications while the user writes the rest of the specification by hand. To efficiently generate Alloy specifications, aDeryaft exploits the relational basis of Alloy and formulates graph properties that are likely to hold for the given instances. It then checks the properties for these instances and translates the valid properties into Alloy constraints, which it outputs as an Alloy specification. We illustrate aDeryaft's constraint generation on a variety of commonly used data structures.

Forward symbolic execution is a program analysis technique that allows using symbolic inputs to explore program executions. The traditional applications of this technique have focused on programs that manipulate primitive data types, such as integer or boolean. Recent extensions have shown how to handle reference types at their representation level. The extensions have favorably been backed by advances in constraint solving technology, and together they have made symbolic execution applicable, at least in theory, to a large class of programs. In practice, however, the increased potential for applications has created significant issues with scalability of symbolic execution to programs of non-trivial size---the ensuing path conditions rapidly become unfeasibly complex.We present Dianju, a new technique that aims to address the scalability of symbolic execution. The fundamental idea in Dianju is to perform symbolic execution of commonly used library classes (such as strings, sets and maps) at the abstract level rather than the representation level. Dianju defines semantics of operations on symbolic objects of these classes, which allows Dianju to abstract away from the complexity that is normally inherent in library implementations, thus promising scalable analyses based on symbolic execution.

Bounded exhaustive testing (BET) is a verification technique in which software is automatically tested for all valid inputs up to specified size bounds. A particularly interesting case of BET arises in the context of systems that take structurally complex inputs. Early research suggests that the BET approach can reveal faults in small systems with inputs of low structural complexity, but its potential utility for larger systems with more complex input structures remains unclear. We set out to test its utility on one such system. We used Alloy and TestEra to generate inputs to test the Galileo dynamic fault tree analysis tool, for which we already had both a formal specification of the input space and a test oracle. An initial attempt to generate inputs using a straightforward translation of our specification to Alloy did not work well. The generator failed to generate inputs to meaningful bounds. We developed an approach in which we factored the specification, used TestEra to generate abstract inputs based on one factor, and passed the results through a postprocessor that reincorporated information from the second factor. Using this technique, we were able to generate test inputs to meaningful bounds, and the inputs revealed nontrivial faults in the Galileo implementation, our specification, and our oracle. Our results suggest that BET, combined with specification abstraction and factoring techniques, could become a valuable addition to our verification toolkit and that further investigation is warranted.

The contribution of this paper is an experiment that shows the potential value of a combination of selective reverse engineering to formal specifications and bounded exhaustive testing to improve the assurance levels of complex software. A key problem is to scale up test input generation so that meaningful results can be obtained. We present an approach, using Alloy and TestEra for test input generation, which we evaluate by experimental application to the Galileo dynamic fault tree analysis tool.

We show how model checking and symbolic execution can be used to generate test inputs to achieve structural coverage of code that manipulates complex data structures. We focus on obtaining branch-coverage during unit testing of some of the core methods of the red-black tree implementation in the Java TreeMap library, using the Java PathFinder model checker. Three different test generation techniques will be introduced and compared, namely, straight model checking of the code, model checking used in a black-box fashion to generate all inputs up to a fixed size, and lastly, model checking used during white-box test input generation. The main contribution of this work is to show how efficient white-box test input generation can be done for code manipulating complex data, taking into account complex method preconditions.

This paper presents Korat, a novel framework for automated testing of Java programs. Given a formal specification for a method, Korat uses the method precondition to automatically generate all (nonisomorphic) test cases up to a given small size. Korat then executes the method on each test case, and uses the method postcondition as a test oracle to check the correctness of each output.To generate test cases for a method, Korat constructs a Java predicate (i.e., a method that returns a boolean) from the method's pre-condition. The heart of Korat is a technique for automatic test case generation: given a predicate and a bound on the size of its inputs, Korat generates all (nonisomorphic) inputs for which the predicate returns true. Korat exhaustively explores the bounded input space of the predicate but does so efficiently by monitoring the predicate's executions and pruning large portions of the search space.This paper illustrates the use of Korat for testing several data structures, including some from the Java Collections Framework. The experimental results show that it is feasible to generate test cases from Java predicates, even when the search space for inputs is very large. This paper also compares Korat with a testing framework based on declarative specifications. Contrary to our initial expectation, the experiments show that Korat generates test cases much faster than the declarative framework.

The Alloy Annotation Language (AAL) is a language (under development) for annotating Java code based on the Alloy modeling language. It offers a syntax similar to the Java Modeling Language (JML), and the same opportunities for generation of run-time assertions. In addition, however, AAL offers the possibility of fully automatic compile-time analysis. Several kinds of analysis are supported, including: checking the code of a method against its specification; checking that the specification of a method in a subclass is compatible with the specification in the superclass; and checking properties relating method calls on different objects, such as that the equals methods of a class (and its overridings) induce an equivalence. Using partial models in place of code, it is also possible to analyze object-oriented designs in the abstract: investigating, for example, a view relationship amongst objects.The paper gives examples of annotations and such analyses. It presents (informally) a systematic translation of annotations into Alloy, a simple first-order logic with relational operators. By doing so, it makes Alloy's automatic analysis, which is based on state-of-the-art SAT solvers, applicable to the analysis of object-oriented programs, and demonstrates the power of a simple logic as the basis for an annotation language.

We present TestEra, a novel framework for automated testing of Java programs. TestEra automatically generates all non-isomorphic test cases within a given input size and evaluates correctness criteria. As an enabling technology, TestEra uses Alloy, a first-order relational language, and the Alloy Analyzer. Checking a program with TestEra involves modeling the correctness criteria for the program in Alloy and specifying abstraction and concretization translations between instances of Alloy models and Java data structures. TestEra produces concrete Java inputs as counterexamples to violated correctness criteria. The paper discusses TestEra's analyses of several case studies: methods that manipulate singly linked lists and red-black trees, a naming architecture, and a part of the Alloy Analyzer.

Lightweight formal modeling and automatic analysis were used to explore the design of the intentional naming system (INS), a new scheme for resource discovery in a dynamic networked environment. We constructed a model of INS in Alloy a lightweight relational notation, and analyzed it with the Alloy Constraint Analyzer, a fully automatic simulation and checking tool. In doing so, we exposed several serious flaws in both the algorithm of INS and the underlying naming semantics. We were able to characterize the conditions under which the existing INS scheme works correctly, and evaluate proposed fixes.