Search

Combinatorial interaction testing (CIT) is an important technique for testing highly configurable software systems with demonstrated effectiveness in practice. The goal of CIT is to generate test cases covering the interactions of configuration options, under certain hard constraints. In this context, constrained covering arrays (CCAs) are frequently used as test cases in CIT. Constrained Covering Array Generation (CCAG) is an NP-hard combinatorial optimization problem, solving which requires an effective method for generating small CCAs. In particular, effectively solving t-way CCAG with t > 4 is even more challenging. Inspired by the success of automated algorithm configuration and automated algorithm selection in solving combinatorial optimization problems, in this paper, we investigate the efficacy of automated algorithm configuration and automated algorithm selection for the CCAG problem, and propose a novel, automated CCAG approach called AutoCCAG. Extensive experiments on public benchmarks show that AutoCCAG can find much smaller-sized CCAs than current state-of-the-art approaches, indicating the effectiveness of AutoCCAG. More encouragingly, to our best knowledge, our paper reports the first results for CCAG with a high coverage strength (i.e., 5-way CCAG) on public benchmarks. Our results demonstrate that AutoCCAG can bring considerable benefits in testing highly configurable software systems. [ABSTRACT FROM AUTHOR]

syntax tree (AST) mapping algorithms are widely used to analyze changes in source code. Despite the foundational role of AST mapping algorithms, little effort has been made to evaluate the accuracy of AST mapping algorithms, i.e., the extent to which an algorithm captures the evolution of code. We observe that a program element often has only one best-mapped program element. Based on this observation, we propose a hierarchical approach to automatically compare the similarity of mapped statements and tokens by different algorithms. By performing the comparison, we determine if each of the compared algorithms generates inaccurate mappings for a statement or its tokens. We invite 12 external experts to determine if three commonly used AST mapping algorithms generate accurate mappings for a statement and its tokens for 200 statements. Based on the experts' feedback, we observe that our approach achieves a precision of 0.98-1.00 and a recall of 0.65-0.75. Furthermore, we conduct a large-scale study with a dataset of ten Java projects containing a total of 263,165 file revisions. Our approach determines that GumTree, MTDiff and IJM generate inaccurate mappings for 20%-29%, 25%-36% and 21%-30% of the file revisions, respectively. Our experimental results show that state-of-the-art AST mapping algorithms still need improvements [ABSTRACT FROM AUTHOR]

One of the main challenges of reactive synthesis, an automated procedure to obtain a correct-by-construction reactive system, is to deal with unrealizable specifications. One means to deal with unrealizability, in the context of GR(1), an expressive assume-guarantee fragment of LTL that enables efficient synthesis, is the computation of an unrealizable core, which can be viewed as a fault-localization approach. Existing solutions, however, are computationally costly, are limited to computing a single core, and do not correctly support specifications with constructs beyond pure GR(1) elements. In this work we address these limitations. First, we present QuickCore, a novel algorithm that accelerates unrealizable core computations by relying on the monotonicity of unrealizability, on an incremental computation, and on additional properties of GR(1) specifications. Second, we present Punch, a novel algorithm to efficiently compute all unrealizable cores of a specification. Finally, we present means to correctly handle specifications that include higher-level constructs beyond pure GR(1) elements. We implemented our ideas on top of Spectra, an opensource language and synthesis environment. Our evaluation over benchmarks from the literature shows that QuickCore is in most cases faster than previous algorithms, and that its relative advantage grows with scale. Moreover, we found that most specifications include more than one core, and that Punch finds all the cores significantly faster than a competing naive algorithm. [ABSTRACT FROM AUTHOR]

It is widely known that the general matching problem on graphs is a non-polynomial optimization problem. Thus all differencing algorithms we know of use heuristics to identify corresponding elements (e.g.[2],[6]) apart from those that rely on unique identifiers (e.g.[5],[3]). We wonder if an exact algorithm can be designed which computes a minimal cost matching between the elements of the class diagrams and which, although it shows a non-polynomial worst case behaviour, delivers its solution much faster in most cases. In this position paper we describe our ongoing work, the idea of an algorithm which works with estimated transformation costs in order to reduce the computation costs. The algorithm has not been implemented yet; it has only been manually tested on a few examples. [ABSTRACT FROM AUTHOR]

Unrealizability is a major challenge for GR(1), an expressive assume-guarantee fragment of LTL that enables effi- cient synthesis. Some works attempt to help engineers deal with unrealizability by generating counter-strategies or computing an unrealizable core. Other works propose to repair the unrealizable specification by suggesting repairs in the form of automatically generated assumptions. In this work we present two novel symbolic algorithms for repairing unrealizable GR(1) specifications. The first algorithm infers new assumptions based on the recently introduced JVTS. The second algorithm infers new assumptions directly from the specification. Both algorithms are sound. The first is incomplete but can be used to suggest many different repairs. The second is complete but suggests a single repair. Both are symbolic and therefore efficient. We implemented our work, validated its correctness, and evaluated it on benchmarks from the literature. The evaluation shows the strength of our algorithms, in their ability to suggest repairs and in their performance and scalability compared to previous solutions. [ABSTRACT FROM AUTHOR]

Many modern applications require low-latency processing of large data sets, often by using approximate algorithms that trade accuracy of the results for faster execution or reduced memory consumption. Although the algorithms provide probabilistic accuracy and performance guarantees, a software developer who implements these algorithms has little support from existing tools. Standard profilers do not consider accuracy of the computation and do not check whether the outputs of these programs satisfy their accuracy specifications. We present AXPROF, an algorithmic profiling framework for analyzing randomized approximate programs. The developer provides the accuracy specification as a formula in a mathematical notation, using probability or expected value predicates. AXPROF automatically generates statistical reasoning code. It first constructs the empirical models of accuracy, time, and memory consumption. It then selects and runs appropriate statistical tests that can, with high confidence, determine if the implementation satisfies the specification. We used AXPROF to profile 15 approximate applications from three domains -- data analytics, numerical linear algebra, and approximate computing. AXPROF was effective in finding bugs and identifying various performance optimizations. In particular, we discovered five previously unknown bugs in the implementations of the algorithms and created fixes, guided by AXPROF. [ABSTRACT FROM AUTHOR]