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.

Runtime Exceptions (REs) are an important class of bugs that occur frequently during code development. Traditional Automatic Program Repair (APR) tools are of limited use in this “in-development” use case, since they require a test-suite to be available as a patching oracle. Thus, developers typically tend to manually resolve their in-development REs, often by referring to technical forums, such as Stack Overflow (SO). To automate this manual process we extend our previous work, MaesTro, to provide real-time assistance to developers for repairing Java REs by recommending a relevant patch-suggesting SO post and synthesizing a repair patch from this post to fix the RE in the developer's code. Maestro exploits a library of Runtime Exception Patterns (REPs) semi-automatically mined from SO posts, through a relatively inexpensive, one-time, incremental process. An REP is an abstracted sequence of statements that triggers a given RE. REPs are used to index SO posts, retrieve a post most relevant to the RE instance exhibited by a developer's code and then mediate the process of extracting a concrete repair from the SO post, abstracting out post-specific details, and concretizing the repair to the developer's buggy code. We evaluate MaesTro on a published RE benchmark comprised of 78 instances. Maestro is able to generate a correct repair patch at the top position in 27% of the cases, within the top-3 in 40% of the cases and overall return a useful artifact in 81% of the cases. Further, the use of REPs proves instrumental to all aspects of Maestro's performance, from ranking and searching of SO posts to synthesizing patches from a given post. In particular, 45% of correct patches generated by MaesTro could not be produced by a baseline technique not using REPs, even when provided with Maestro's SO-post ranking. Maestro is also fast, needing around 1 second, on average, to generate its output. Overall, these results indicate that Maestro can provide effective real-time assistance to developers in repairing REs.

Visualization is very important for machine learning (ML) pipelines because it can show explorations of the data to inspire data scientists and show explanations of the pipeline to improve understandability. In this paper, we present a novel approach that automatically generates visualizations for ML pipelines by learning visualizations from highly-upvoted Kaggle pipelines. The solution extracts both code and dataset features from these high-quality human-written pipelines and corresponding training datasets, learns the mapping rules from code and dataset features to visualizations using association rule mining (ARM), and finally uses the learned rules to predict visualizations for unseen ML pipelines. The evaluation results show that the proposed solution is feasible and effective to generate visualizations for ML pipelines.

Visualizations are widely used to communicate findings and make data-driven decisions. Unfortunately creating bespoke and reproducible visualizations requires the use of procedural tools such as matplotlib. These tools present a steep learning curve as their documentation often lacks sufficient usage examples to help beginners get started or accomplish a specific task. Forums such as StackOverflow have long helped developers search for code online and adapt it for their use. However, developers still have to sift through search results and understand the code before adapting it for their use.We built a tool called VizSmith which enables code reuse for visualizations by mining visualization code from Kaggle notebooks and creating a database of 7176 reusable Python functions. Given a dataset, columns to visualize and a text query from the user, VizSmith searches this database for appropriate functions, runs them and displays the generated visualizations to the user. At the core of VizSmith is a novel metamorphic testing based approach to automatically assess the reusability of functions, which improves end-to-end synthesis performance by 10% and cuts the number of execution failures by 50%.

Programmers often use Q&A sites (e.g., Stack Overflow) to understand a root cause of program bugs. Runtime exceptions is one of such important class of bugs that is actively discussed on Stack Overflow. However, it may be difficult for beginner programmers to come up with appropriate keywords for search. Moreover, they need to switch their attentions between IDE and browser, and it is time-consuming. To overcome these difficulties, we proposed a method, "Q&A MAESTRO", to find suitable Q&A posts automatically for Java runtime exception by utilizing structure information of codes described in programming Q&A website. In this paper, we describe a usage scenario of IDE-plugin, the architecture and user interface of the implementation, and results of user studies. A video is available at https://youtu.be/4X24jJrMUVw. A demo software is available at https://github.com/FujitsuLaboratories/Q-A-MAESTRO.

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%.

Deep neural networks (DNN) have been shown to be notoriously brittle to small perturbations in their input data. This problem is analogous to the over-fitting problem in test-based program synthesis and automatic program repair, which is a consequence of the incomplete specification, i.e., the limited tests or training examples, that the program synthesis or repair algorithm has to learn from. Recently, test generation techniques have been successfully employed to augment existing specifications of intended program behavior, to improve the generalizability of program synthesis and repair. Inspired by these approaches, in this paper, we propose a technique that re-purposes software testing methods, specifically mutation-based fuzzing, to augment the training data of DNNs, with the objective of enhancing their robustness. Our technique casts the DNN data augmentation problem as an optimization problem. It uses genetic search to generate the most suitable variant of an input data to use for training the DNN, while simultaneously identifying opportunities to accelerate training by skipping augmentation in many instances. We instantiate this technique in two tools, Sensei and Sensei-SA, and evaluate them on 15 DNN models spanning 5 popular image data-sets. Our evaluation shows that Sensei can improve the robust accuracy of the DNN, compared to the state of the art, on each of the 15 models, by upto 11.9% and 5.5% on average. Further, Sensei-SA can reduce the average DNN training time by 25%, while still improving robust accuracy.

Using online Q&A forums, such as Stack Overflow (SO), for guidance to resolve program bugs, among other development issues, is commonplace in modern software development practice. Runtime exceptions (RE) is one such important class of bugs that is actively discussed on SO. In this work we present a technique and prototype tool called MAESTRO that can automatically recommend an SO post that is most relevant to a given Java RE in a developer's code. MAESTRO compares the exception-generating program scenario in the developer's code with that discussed in an SO post and returns the post with the closest match. To extract and compare the exception scenario effectively, MAESTRO first uses the answer code snippets in a post to implicate a subset of lines in the post's question code snippet as responsible for the exception and then compares these lines with the developer's code in terms of their respective Abstract Program Graph (APG) representations. The APG is a simplified and abstracted derivative of an abstract syntax tree, proposed in this work, that allows an effective comparison of the functionality embodied in the high-level program structure, while discarding many of the low-level syntactic or semantic differences. We evaluate MAESTRO on a benchmark of 78 instances of Java REs extracted from the top 500 Java projects on GitHub and show that MAESTRO can return either a highly relevant or somewhat relevant SO post corresponding to the exception instance in 71% of the cases, compared to relevant posts returned in only 8% - 44% instances, by four competitor tools based on state-of-the-art techniques. We also conduct a user experience study of MAESTRO with 10 Java developers, where the participants judge MAESTRO reporting a highly relevant or somewhat relevant post in 80% of the instances. In some cases the post is judged to be even better than the one manually found by the participant.

Network verification promises to detect errors, such as black holes and forwarding loops, by logically analyzing the control or data plane. To do so efficiently, the state-of-the-art (e.g., Veriflow) partitions packet headers with identical forwarding behavior into the same packet equivalence class (PEC).Recently, Yang and Lam showed how to construct the minimal set of PECs, called atomic predicates. Their construction uses Binary Decision Diagrams (BDDs). However, BDDs have been shown to incur significant overhead per packet header bit, performing poorly when analyzing large-scale data centers. The overhead of atomic predicates prompted ddNF to devise a specialized data structure of Ternary Bit Vectors (TBV) instead.However, TBVs are strictly less expressive than BDDs. Moreover, unlike atomic predicates, ddNF's set of PECs is not minimal. We show that ddNF's non-minimality is due to empty PECs. In addition, empty PECs are shown to trigger wrong analysis results. This reveals an inherent tension between precision, expressiveness and performance in formal network verification.Our paper resolves this tension through a new lattice-theoretical PEC-construction algorithm, # PEC, that advances the field as follows: (i) # PEC can encode more kinds of forwarding rules (e.g., ip-tables) than ddNF and Veriflow, (ii) # PEC verifies a wider class of errors (e.g., shadowed rules) than ddNF, and (iii) on a broad range of real-world datasets, # PEC is 10\times faster than atomic predicates. By achieving precision, expressiveness and performance, this paper answers a longstanding quest that has spanned three generations of formal network analysis techniques.

Despite significant advances in automatic program repair (APR) techniques over the past decade, practical deployment remains an elusive goal. One of the important challenges in this regard is the general inability of current APR techniques to produce patches that require edits in multiple locations, i.e., multi-hunk patches. In this work, we present a novel APR technique that generalizes single-hunk repair techniques to include an important class of multi-hunk bugs, namely bugs that may require applying a substantially similar patch at a number of locations. We term such sets of repair locations as evolutionary siblings - similar looking code, instantiated in similar contexts, that are expected to undergo similar changes. At the heart of our proposed method is an analysis to accurately identify a set of evolutionary siblings, for a given bug. This analysis leverages three distinct sources of information, namely the test-suite spectrum, a novel code similarity analysis, and the revision history of the project. The discovered siblings are then simultaneously repaired in a similar fashion. We instantiate this technique in a tool called HERCULES and demonstrate that it is able to correctly fix 46 bugs in the Defects4J dataset, the highest of any individual APR technique to date. This includes 15 multi-hunk bugs and overall 11 bugs which have not been fixed by any other technique so far.

Traditional automatic program repair (APR) tools rely on a test-suite as a repair specification. But test suites even when available are not of specification quality, limiting the performance and hence viability of test-suite based repair. On the other hand, static analysis-based bug finding tools are seeing increasing adoption in industry but still face challenges since the reported violations are viewed as not easily actionable. We propose a novel solution that solves both these challenges through a technique for automatically generating high-quality patches for static analysis violations by learning from examples. Our approach uses the static analyzer as an oracle and does not require a test suite. We realize our solution in a system, Phoenix, that implements a fully-automated pipeline that mines and cleans patches for static analysis violations from the wild, learns generalized executable repair strategies as programs in a novel Domain Specific Language (DSL), and then instantiates concrete repairs from them on new unseen violations. Using Phoenix we mine a corpus of 5,389 unique violations and patches from 517 Github projects. In a cross-validation study on this corpus Phoenix successfully produced 4,596 bug-fixes, with a recall of 85% and a precision of 54%. When applied to the latest revisions of a further5 Github projects, Phoenix produced 94 correct patches to previously unknown bugs, 19 of which have already been accepted and merged by the development teams. To the best of our knowledge this constitutes, by far the largest application of any automatic patch generation technology to large-scale real-world systems

Modern mobile malware tend to conduct their malicious exploits through sophisticated patterns of interactions that involve multiple entities, e.g., the mobile platform, human users, and network locations. Such malware often evade the detection by existing approaches due to their limited expressiveness and accuracy in characterizing and detecting these malware. To address these issues, in this paper, we recognize entities in the environment of an app, the app's interactions with such entities, and the provenance of these interactions, i.e., the intent and ownership of each interaction, as the key to comprehensively characterizing modern mobile apps, and mobile malware in particular. With this insight, we propose a novel approach named EnMobile including a new entity-based characterization of mobile-app behaviors, and corresponding static analyses, to accurately characterize an app's interactions with entities. We implement EnMobile and provide a practical application of EnMobile in a signature-based scheme for detecting mobile malware. We evaluate EnMobile on a set of 6614 apps consisting of malware from Genome and Drebin along with benign apps from Google Play. Our results show that EnMobile detects malware with substantially higher precision and recall than four state-of-the-art approaches, namely Apposcopy, Drebin, MUDFLOW, and AppContext.

We present Bugs.jar, a large-scale dataset for research in automated debugging, patching, and testing of Java programs. Bugs.jar is comprised of 1,158 bugs and patches, drawn from 8 large, popular open-source Java projects, spanning 8 diverse and prominent application categories. It is an order of magnitude larger than Defects4J, the only other dataset in its class. We discuss the methodology used for constructing Bugs.jar, the representation of the dataset, several use-cases, and an illustration of three of the use-cases through the application of 3 specific tools on Bugs.jar, namely our own tool, Elixir, and two third-party tools, Ekstazi and JaCoCo.

This work is motivated by the pervasive use of method invocations in object-oriented (OO) programs, and indeed their prevalence in patches of OO-program bugs. We propose a generate-and-validate repair technique, called ELIXIR designed to be able to generate such patches. ELIXIR aggressively uses method calls, on par with local variables, fields, or constants, to construct more expressive repair-expressions, that go into synthesizing patches. The ensuing enlargement of the repair space, on account of the wider use of method calls, is effectively tackled by using a machine-learnt model to rank concrete repairs. The machine-learnt model relies on four features derived from the program context, i.e., the code surrounding the potential repair location, and the bug report. We implement ELIXIR and evaluate it on two datasets, the popular Defects4J dataset and a new dataset Bugs.jar created by us, and against 2 baseline versions of our technique, and 5 other techniques representing the state of the art in program repair. Our evaluation shows that ELIXIR is able to increase the number of correctly repaired bugs in Defects4J by 85% (from 14 to 26) and by 57% in Bugs.jar (from 14 to 22), while also significantly out-performing other state-of-the-art repair techniques including ACS, HD-Repair, NOPOL, PAR, and jGenProg.

Automated unit test generation bears the promise of significantly reducing test cost and hence improving software quality. However, the maintenance cost of the automatically generated tests presents a significant barrier to adoption of this technology. To address this challenge, we propose a novel technique for automated and fine-grained incremental generation of unit tests through minimal augmentation of an existing test suite. The technique uses iterative, incremental refinement of test-drivers and symbolic execution, guided by a diagnostics engine. The diagnostics engine works off a novel precise and efficient byte-level dynamic dependence analysis built using Reduced Ordered Binary Decision Diagrams (ROBDDs). We present a tool FSX implementing this technique and evaluate it under two practical use-cases of incremental unit test generation, on five revisions of the open-source software iPerf, as well as on 3 large subjects, comprising more than 60 thousand lines of code, from in-house commercial network products. The evaluation shows that FSX can generate high-quality unit tests on large industrial software while minimizing the maintenance cost of the overall test-suite.

Search-based program repair automatically searches for a program fix within a given repair space. This may be accomplished by retrofitting a generic search algorithm for program repair as evidenced by the GenProg tool, or by building a customized search algorithm for program repair as in SPR. Unfortunately, automated program repair approaches may produce patches that may be rejected by programmers, because of which past works have suggested using human-written patches to produce templates to guide program repair. In this work, we take the position that we will not provide templates to guide the repair search because that may unduly restrict the repair space and attempt to overfit the repairs into one of the provided templates. Instead, we suggest the use of a set of anti-patterns --- a set of generic forbidden transformations that can be enforced on top of any search-based repair tool. We show that by enforcing our anti-patterns, we obtain repairs that localize the correct lines or functions, involve less deletion of program functionality, and are mostly obtained more efficiently. Since our set of anti-patterns are generic, we have integrated them into existing search based repair tools, including GenProg and SPR, thereby allowing us to obtain higher quality program patches with minimal effort.

Automated unit test generation bears the promise of significantly reducing test cost and hence improving software quality. However, the maintenance cost of the automatically generated tests presents a significant barrier to adoption of this technology. To address this challenge, in previous work, we proposed a novel technique for automated and fine-grained incremental generation of unit tests through minimal augmentation of an existing test suite. In this paper we describe a tool FSX, implementing this technique. We describe the architecture, user-interface, and salient features of FSX, and specific practical use-cases of its technology. We also report on a real, large-scale deployment of FSX, as a practical validation of the underlying research contribution and of automated test generation research in general.

We study the problem of reducing test cases generated by bit vector based symbolic execution test generators. In particular, we first consider a guileless test case generation approach that generates assignment statements for each symbolic scalars, array and structure elements and object fields. We show that test cases generated by this approach can be significantly verbose. We then propose a method for making the generated test cases more succinct using a novel analysis entitled don't care analysis. Don't care analysis identifies assignment statements that can be safely removed from the test cases without affecting the overall code coverage. Our algorithm is based on binary and delta-debugging search. Because it exploits the knowledge of the internal SAT solver, it is effective and efficient in practice. To our knowledge, this is the first fully automatic approach that reduces the sizes of test cases generated using symbolic execution. We implement our test case reduction technique for the KLEE test generation tool and evaluate on 295 programs and functions. Our results are encouraging: in average, the reduced test cases are 50 times smaller than the test cases generated by the guileless test case generator. In addition, since our don't care analysis is tightly integrated into the test case generation tool, its overhead to the overall test generation process is negligible.

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.

With the emergence of new computing platforms, software written for traditional platforms is being re-targeted to reach the users on these new platforms. In particular, due to the proliferation of mobile computing devices, it is common practice for companies to build mobile-specific versions of their existing web applications to provide mobile users with a better experience. Because the differences between desktop and mobile versions of a web application are not only cosmetic, but can also include substantial rewrites of key components, it is not uncommon for these different versions to provide different sets of features. Whereas some of these differences are intentional, such as the addition of location-based features on mobile devices, others are not and can negatively affect the user experience, as confirmed by numerous user reports and complaints. Unfortunately, checking and maintaining the consistency of different versions of an application by hand is not only time consuming, but also error prone. To address this problem, and help developers in this difficult task, we propose an automated technique for matching features across different versions of a multi-platform web application. We implemented our technique in a tool, called FMAP, and used it to perform a preliminary empirical evaluation on nine real-world multi-platform web applications. The results of our evaluation are promising, as FMAP was able to correctly identify missing features between desktop and mobile versions of the web applications considered, as confirmed by our analysis of user reports and software fixes for these applications.

Web applications are popular among developers because of the ease of development and deployment through the ubiquitous web browsing platform. However, differences in a web application's execution across different web browsers manifest as Cross-browser Inconsistencies (XBIs), which are a serious concern for web developers. Testing for XBIs manually is a laborious and error-prone process. In this demo we present X-PERT, which is a tool to identify XBIs in web applications automatically, without requiring any effort from the developer. X-PERT implements a comprehensive technique to identify XBIs and has been found to be effective in detecting real-world XBIs in our empirical evaluation. The source code of X-PERT and XBI reports from our evaluation are available at http://gatech.github.io/xpert.

Due to the increasing popularity of web applications, and the number of browsers and platforms on which such applications can be executed, cross-browser incompatibilities (XBIs) are becoming a serious concern for organizations that develop web-based software. Most of the techniques for XBI detection developed to date are either manual, and thus costly and error-prone, or partial and imprecise, and thus prone to generating both false positives and false negatives. To address these limitations of existing techniques, we developed X-PERT, a new automated, precise, and comprehensive approach for XBI detection. X-PERT combines several new and existing differencing techniques and is based on our findings from an extensive study of XBIs in real-world web applications. The key strength of our approach is that it handles each aspects of a web application using the differencing technique that is best suited to accurately detect XBIs related to that aspect. Our empirical evaluation shows that X-PERT is effective in detecting real-world XBIs, improves on the state of the art, and can provide useful support to developers for the diagnosis and (eventually) elimination of XBIs.

Automated software testing aims to detect errors by producing test inputs that cover as much of the application source code as possible. Applications for mobile devices are typically event-driven, which raises the challenge of automatically producing event sequences that result in high coverage. Some existing approaches use random or model-based testing that largely treats the application as a black box. Other approaches use symbolic execution, either starting from the entry points of the applications or on specific event sequences. A common limitation of the existing approaches is that they often fail to reach the parts of the application code that require more complex event sequences.

One of the consequences of the continuous and rapid evolution of web technologies is the amount of inconsistencies between web browsers implementations. Such inconsistencies can result in cross-browser incompatibilities (XBIs)-situations in which the same web application can behave differently when run on different browsers. In some cases, XBIs consist of tolerable cosmetic differences. In other cases, however, they may completely prevent users from accessing part of a web application's functionality. Despite the prevalence of XBIs, there are hardly any tools that can help web developers detect and correct such issues. In fact, most existing approaches against XBIs involve a considerable amount of manual effort and are consequently extremely time consuming and error prone. In recent work, we have presented two complementary approaches, WEBDIFF and CROSST, for automatically detecting and reporting XBIs. In this paper, we present CROSSCHECK, a more powerful and comprehensive technique and tool for XBI detection that combines and adapts these two approaches in a way that leverages their respective strengths. The paper also presents an empirical evaluation of CROSSCHECK on a set of real-world web applications. The results of our experiments show that CROSSCHECK is both effective and efficient in detecting XBIs, and that it can outperform existing techniques.

With the advent of Web 2.0 applications and new browsers, the cross-browser compatibility issue is becoming increasingly important. Although the problem is widely recognized among web developers, no systematic approach to tackle it exists today. None of the current tools, which provide screenshots or emulation environments, specifies any notion of cross-browser compatibility, much less check it automatically. In this paper, we pose the problem of cross-browser compatibility testing of modern web applications as a 'functional consistency' check of web application behavior across different web browsers and present an automated solution for it. Our approach consists of (1) automatically analyzing the given web application under different browser environments and capturing the behavior as a finite-state machine; (2) formally comparing the generated models for equivalence on a pairwise-basis and exposing any observed discrepancies. We validate our approach on several open-source and industrial case studies to demonstrate its effectiveness and real-world relevance.

We propose a new dynamic method of abstraction, which can be applied during successive steps of the model checking algorithm to further reduce the model produced by traditional static abstraction methods. This is facilitated by information gathered from an analysis of the proof of unsatisfiability of SAT-based bounded model checking problems formulated on the original design. The dynamic abstraction effectively allows the model checker to work with smaller abstract models. Experiments on several industrial benchmarks demonstrate that dynamic abstraction can significantly improve both the performance and the capacity of typical abstraction refinement flows.

Bounded model checking (BMC) based on Boolean satisfiability (SAT) methods has recently gained popularity as a viable alternative to BDD-based techniques for verifying large designs. This work proposes a number of conceptually simple, but extremely effective, optimizations for enhancing the performance of SAT-based BMC flows. The key ideas include: (1) a novel idea to combine SAT-based inductive reasoning and BMC; (2) clever orchestration of variable ordering and learned information in an incremental framework for BMC; and (3) BMC-specific ordering strategies for the SAT solver. Our experiments, conducted on a wide range of industrial designs, show that the proposed optimizations consistently provide between 1-2 orders of magnitude speedup and can be extremely useful in enhancing the efficacy of typical SAT-BMC tools.

We describe a complete method for the latch mapping problem that is based on the efficient integration of previously proposed tech-niques for latch mapping as well as novel optimizations for further improvement. The highlights of the proposed approach include a new method of integrating complete methods and incomplete meth-ods for latch mapping, the use of incremental reasoning to optimize the overall algorithm and the use of a conventional combinational equivalence checking tool as the core engine. Experiments con-firm that the proposed method retains much of the efficiency and capacity of incomplete methods while providing the completeness of complete methods and derives significant performance improve-ments from the proposed optimizations.

We introduce the notion of problem symmetry in search-based SAT algorithms. We develop a theory of essential points to formally characterize the potential search-space pruning that can be realized by exploiting problem symmetry. We unify several search-pruning techniques used in modern SAT solvers under a single framework, by showing them to be special cases of the general theory of essential points. We also propose a new pruning rule exploiting problem symmetry. Preliminary experimental results validate the efficacy of this rule in providing additional search-space pruning beyond the pruning realized by techniques implemented in leading-edge SAT solvers.

This paper addresses the problem of combinational equivalence checking (CEC) which forms one of the key components of the current verification methodology for digital systems. A number of recently proposed BDD based approaches have met with considerable success in this area. However, the growing gap between the capability of current solvers and the complexity of verification instances necessitates the exploration of alternative, better solutions. This paper revisits the application of Satisfiability (SAT) algorithms to the combinational equivalence checking (CEC) problem. We argue that SAT is a more robust and flexible engine of Boolean reasoning for the CEC application than BDDs, which have traditionally been the method of choice. Preliminary results on a simple framework for SAT based CEC show a speedup of up to two orders of magnitude compared to state-of-the-art SAT based methods for CEC and also demonstrate that even with this simple algorithm and untuned prototype implementation it is only moderately slower and sometimes faster than a state-of-the-art BDD based mixed engine commercial CEC tool. While SAT based CEC methods need further research and tuning before they can surpass almost a decade of research in BDD based CEC, the recent progress is very promising and merits continued research.

Empirical observation shows that practically encountered instances of ATPG are efficiently solvable. However, it has been known for more than two decades that ATPG is an NP-complete problem. This work is one of the first attempts to reconcile these seemingly disparate results. We introduce the concept of circuit cut-width and characterize the complexity of ATPG in terms of this property. We provide theoretical and empirical results to argue that an interestingly large class of practical circuits have cut-width characteristics which ensure a provably efficient solution of ATPG on them. 1

The dramatic increase in the processor memory gap in recent years has led to the development of techniques like data prefetching that hide the latency of cache misses. Two such hardware techniques are the stream buffer and the stride predictor. They have dissimilar architectures, are effective for different kinds of memory access patterns and require different amounts of extra memory bandwidth. We compare the performance of these two techniques and propose a scheme that unifies them. Simulation studies on six benchmark programs confirm that the combined scheme is more effective in reducing the average memory access time (AMAT) than either of the two individually.