Documenting the functionality of software units with code comments, e.g., Javadoc comments, is a common programmer best-practice in software engineering. This paper introduces a novel test generation technique that exploits the code-comment documentation constructively. We originally address those behaviors as test objectives, which we pursue in search-based fashion. We deliver test cases with names and oracles properly contextualized on the target behaviors. Our experiments against a benchmark of 118 Java classes indicate that the proposed approach successfully tests many software behaviors that may remain untested with coverage-driven test generation approaches, and distinctively detects unknown failures.

Integration testing is a fundamental step of the software development process. Due to the high costs, testers may like to automatically generate the test cases, but unfortunately current test generators are designed for unit testing or system testing, while they are generally ill-suited for integration testing. In this paper, we discuss the challenges of generating test cases for integration testing, and the limitations of current test generators thereby. We elaborate on a novel approach to automatically generating test cases for integration testing, and report initial evidence in support of our approach.

Recently, the Ethereum blockchain changed its consensus algorithm from Proof-of-Work (PoW) to Proof-of-Stake (PoS). This change has greatly reduced overall energy consumption but has paved the way for the profiling of numerous mechanisms and actors that can operate off-chain to achieve Maximal Extractable Value (MEV). This raises questions about how transparent such a scenario is, both from the point of view of block validation power and from the point of view of the rewards achieved by distinct actors within the platform. To address this concern and to mitigate potential negative externalities, a permissionless ecosystem has recently been proposed, which should be transparent and fair for the extraction of MEV. In this article, after briefly describing the new ecosystem, we conduct an in-depth analysis of Ethereum blocks and other information about the actors operating in the ecosystem, to highlight potential critical situations.

Many automatic Web testing techniques generate test cases by analyzing the GUI of the Web applications under test, aiming to exercise sequences of actions that are similar to the ones that testers could manually execute. However, the efficiency of the test generation process is severely limited by the cost of analyzing the content of the GUI screens after executing each action. In this paper, we introduce an inference component, Sibilla, which accumulates knowledge about the behavior of the GUI after each action. Sibillaenables the test generators to reuse the results computed for GUI screens that recur multiple times during the test generation process, thus improving the efficiency of Web testing techniques.We experimented Sibillawith Web testing techniques based on three different GUI exploration strategies (Random, Depth-first, and Q-learning) and nine target systems, observing reductions from 22% to 96% of the test generation time.

The generation of syntactically and semantically valid input data, able to exercise functionalities imposing constraints on the validity of the inputs, is a key challenge in automatic GUI (Graphical User Interface) testing.Existing test case generation techniques often rely on manually curated catalogs of values, although they might require significant effort to be created and maintained, and could hardly scale to applications with several input forms. Alternatively, it is possible to extract values from external data sources, such as the Web or publicly available knowledge bases. However, external sources are unlikely to provide the domain-specific and application-specific data that are often required to thoroughly exercise applications.This paper proposes DBINPUTS, a novel approach that automatically identifies domain-specific and application-specific inputs to effectively fulfill the validity constraints present in the tested GUI screens. The approach exploits syntactic and semantic similarities between the identifiers of the input fields shown on GUI screens and those of the tables of the target GUI application database, and extracts valid inputs from such database, automatically resolving the mismatch between the user interface and the database schema. DBINPUTS can properly cope with system testing and maintenance testing efforts, since databases are naturally and inexpensively available in those phases.Our experiments with 4 Web applications and 11 Mobile apps provide evidence that DBINPUTS can outperform techniques like random input selection and LINK, a competing approach for searching inputs from knowledge bases, in both Web and Mobile domains.

This paper presents Prevent, a fully unsupervised approach to predict and localize failures in distributed enterprise applications.Software failures in production are unavoidable. Predicting failures and locating failing components online are the first steps to proactively manage faults in production. Many techniques predict failures from anomalous combinations of system metrics with supervised, weakly supervised, and semi-supervised learning models. Supervised approaches require large sets of labelled data not commonly available in large enterprise pplications, and address failure types that can be either captured with predefined rules or observed while training supervised odels.Preventintegrates the core ingredients of unsupervised approaches into a novel fully unsupervised approach to predict failures and localize failing resources. The results of experimenting with Preventon a commercially-compliant distributed cloud system indicate that Preventprovides more stable, reliable and timely predictions than supervised learning approaches, without requiring the often impractical training with labeled data.

In this paper we propose an approach for reusing formula solutions to reduce the impact of Satisfiability Modulo Theories (SMT) solvers on the scalability of symbolic program analysis. SMT solvers can efficiently handle huge expressions in relevant logic theories, but they still represent a main bottleneck to the scalability of symbolic analyses, like symbolic execution and symbolic model checking. Reusing proofs of formulas solved during former analysis sessions can reduce the amount of invocations of SMT solvers, thus mitigating the impact of SMT solvers on symbolic program analysis. Early approaches to reuse formula solutions exploit equivalence and inclusion relations among structurally similar formulas, and are strongly tighten to the specific target logics. In this paper, we present an original approach that reuses both satisfiability and unsatisfiability proofs shared among many formulas beyond only equivalent or related-by-implication formulas. Our approach straightforwardly generalises across multiple logics. It is based on the original concept of distance between formulas, which heuristically approximates the likelihood of formulas to share either satisfiability or unsatisfiability proofs. We show the efficiency and the generalisability of our approach, by instantiating the underlying distance function for formulas that belong to most popular logic theories handled by current SMT solvers, and confirm the effectiveness of the approach, by reporting experimental results on over nine millions formulas from five logic theories.

A key challenge in automatic Web testing is the generation of syntactically and semantically valid input values that can exercise the many functionalities that impose constraints on the validity of the inputs. Existing test case generation techniques either rely on manually curated catalogs of values, or extract values from external data sources, such as the Web or publicly available knowledge bases. Unfortunately, relying on manual effort is generally too expensive for most practical applications, while domain-specific and application-specific data can be hardly found either on the Web or in general purpose knowledge bases.

Summary Performance profiling can benefit from test cases that hit high‐cost executions of programs. In this paper, we investigate the problem of automatically generating test cases that trigger the worst‐case execution of programs and propose a novel technique that solves this problem with an unprecedented combination of symbolic execution and evolutionary algorithms. Our technique, which we refer to as ‘Evolutionary Symbolic Execution’, embraces the execution cost of the program paths as the fitness function to pursue the worst execution. It defines an original set of evolutionary operators, based on symbolic execution, which suitably sample the possible program paths to make the search process effective. Specifically, our technique defines a memetic algorithm that (i) incrementally evolves by steering symbolic execution to traverse new program paths that comply with execution conditions combined and refined from the currently collected worse program paths and (ii) periodically applies local optimizations to the execution conditions of the worst currently identified program path to further speed up the identification of the worst path. We report on a set of initial experiments indicating that our technique succeeds in generating good worst‐case test cases for programs with which existing approaches cannot cope. Also, we show that, as far as the problem of generating worst‐case test cases is concerned, the distinguishing evolutionary operators based on symbolic execution that we define in this paper are more effective than traditional operators that directly manipulate the program inputs.

The execution of Spark applications is based on the execution order and parallelism of the different jobs, given data and available resources. Spark reifies these dependencies in a graph that we refer to as the (parallel) execution plan of the application. All the approaches that have studied the estimation of the execution times and the dynamic provisioning of resources for this kind of applications have always assumed that the execution plan is unique, given the computing resources at hand. This assumption is at least simplistic for applications that include conditional branches or loops and limits the precision of the prediction techniques.

Worst-case execution time testing amounts to constructing a test case triggering the worst-case execution time of a program, and has many important applications to identify, debug and fix performance bottlenecks and security holes of programs. We propose a novel technique for worst-case execution time testing combining symbolic execution and evolutionary algorithms, which we call "Evolutionary Symbolic Execution", that (i) considers the set of the feasible program paths as the search space, (ii) embraces the execution cost of the program paths as the fitness function to pursue the worst path, (iii) exploits symbolic execution with random path selection to collect an initial set of feasible program paths, (iv) incrementally evolves by steering symbolic execution to traverse new program paths that comply with execution conditions combined and refined from the currently collected program paths, and (v) periodically applies local optimizations to the worst currently identified program path to speed up the identification of the worst path. We report on a set of initial experiments indicating that our technique succeeds in generating good worst-case execution time test cases for programs with which existing approaches cannot cope.

Many symbolic program analysis techniques rely on SMT solvers to verify properties of programs. Despite the remarkable progress made in the development of such tools, SMT solvers still represent a main bottleneck to the scalability of these techniques. Recent approaches tackle this bottleneck by reusing solutions of formulas that recur during program analysis, thus reducing the number of queries to SMT solvers. Current approaches only reuse solutions across formulas that are equivalent to, contained in or implied by other formulas, as identified through a set of predefined rules, and cannot reuse solutions across formulas that differ in their structure, even if they share some potentially reusable solutions. In this paper, we propose a novel approach that can reuse solutions across formulas that share at least one solution, regardless of their structural resemblance. Our approach exploits a novel heuristic to efficiently identify solutions computed for previously solved formulas and most likely shared by new formulas. The results of an empirical evaluation of our approach on two different logics show that our approach can identify on average more reuse opportunities and is markedly faster than competing approaches.

Despite the recent improvements in automatic test case generation, handling complex data structures as test inputs is still an open problem. Search-based approaches can generate sequences of method calls that instantiate structured inputs to exercise a relevant portion of the code, but fall short in building inputs to execute program elements whose reachability is determined by the structural features of the input structures themselves. Symbolic execution techniques can effectively handle structured inputs, but do not identify the sequences of method calls that instantiate the input structures through legal interfaces. In this paper, we propose a new approach to automatically generate test cases for programs with complex data structures as inputs. We use symbolic execution to generate path conditions that characterise the dependencies between the program paths and the input structures, and convert the path conditions to optimisation problems that we solve with search-based techniques to produce sequences of method calls that instantiate those inputs. Our preliminary results show that the approach is indeed effective in generating test cases for programs with complex data structures as inputs, thus opening a promising research direction.

We present the Java Bytecode Symbolic Executor (JBSE), a symbolic executor for Java programs that operates on complex heap inputs. JBSE implements both the novel Heap EXploration Logic (HEX), a symbolic execution approach to deal with heap inputs, and the main state-of-the-art approaches that handle data structure constraints expressed as either executable programs (repOk methods) or declarative specifications. JBSE is the first symbolic executor specifically designed to deal with programs that operate on complex heap inputs, to experiment with the main state-of-the-art approaches, and to combine different decision procedures to explore possible synergies among approaches for handling symbolic data structures.

Structural coverage metrics, and in particular branch coverage, are popular approaches to measure the thoroughness of test suites. Unfortunately, the presence of elements that are not executable in the program under test and the difficulty of generating test cases for rare conditions impact on the effectiveness of the coverage obtained with current approaches. In this paper, we propose a new approach that combines symbolic execution and symbolic reachability analysis to improve the effectiveness of branch testing. Our approach embraces the ideal definition of branch coverage as the percentage of executable branches traversed with the test suite, and proposes a new bidirectional symbolic analysis for both testing rare execution conditions and eliminating infeasible branches from the set of test objectives. The approach is centered on a model of the analyzed execution space. The model identifies the frontier between symbolic execution and symbolic reachability analysis, to guide the alternation and the progress of bidirectional analysis towards the coverage targets. The experimental results presented in the paper indicate that the proposed approach can both find test inputs that exercise rare execution conditions that are not identified with state-of-the-art approaches and eliminate many infeasible branches from the coverage measurement. It can thus produce a modified branch coverage metric that indicates the amount of feasible branches covered during testing, and helps team leaders and developers in estimating the amount of not-yet-covered feasible branches. The approach proposed in this paper suffers less than the other approaches from particular cases that may trap the analysis in unbounded loops.

Data flow testing has recently attracted new interest in the context of testing object oriented systems, since data flow information is well suited to capture relations among the object states, and can thus provide useful information for testing method interactions. Unfortunately, classic data flow testing, which is based on static analysis of the source code, fails to identify many important data flow relations due to the dynamic nature of object oriented systems. In this paper, we propose a new technique to generate test cases for object oriented software. The technique exploits useful inter-procedural data flow information extracted dynamically from execution traces for object oriented systems. The technique is designed to enhance an initial test suite with test cases that exercise complex state based method interactions. The experimental results indicate that dynamic data flow testing can indeed generate test cases that exercise relevant behaviors otherwise missed by both the original test suite and by test suites that satisfy classic data flow criteria.

Symbolic analysis techniques have largely improved over the years, and are now approaching an industrial maturity level. One of the main limitations to the scalability of symbolic analysis is the impact of constraint solving that is still a relevant bottleneck for the applicability of symbolic techniques, despite the dramatic improvements of the last decades. In this paper we discuss a novel approach to deal with the constraint solving bottleneck. Starting from the observation that constraints may recur during the analysis of the same as well as different programs, we investigate the advantages of complementing constraint solving with searching for the satisfiability proof of a constraint in a repository of constraint proofs. We extend recent proposals with powerful simplifications and an original canonical form of the constraints that reduce syntactically different albeit equivalent constraints to the same form, and thus facilitate the search for equivalent constraints in large repositories. The experimental results we attained indicate that the proposed approach improves over both similar solutions and state of the art constraint solvers.

Symbolic analysis is a core component of many automatic test generation and program verication approaches. To verify complex software systems, test and analysis techniques shall deal with the many aspects of the target systems at different granularity levels. In particular, testing software programs that make extensive use of heap data structures at unit and integration levels requires generating suitable input data structures in the heap. This is a main challenge for symbolic testing and analysis techniques that work well when dealing with numeric inputs, but do not satisfactorily cope with heap data structures yet. In this paper we propose a language HEX to specify invariants of partially initialized data structures, and a decision procedure that supports the incremental evaluation of structural properties in HEX. Used in combination with the symbolic execution of heap manipulating programs, HEX prevents the exploration of invalid states, thus improving the eefficiency of program testing and analysis, and avoiding false alarms that negatively impact on verication activities. The experimental data conrm that HEX is an effective and efficient solution to the problem of testing and analyzing heap manipulating programs, and outperforms the alternative approaches that have been proposed so far.

This paper investigates the limits of current data flow testing approaches from a radically novel viewpoint, and shows that the static data flow techniques used so far in data flow testing to identify the test objectives fail to represent the universe of data flow relations entailed by a program. This paper compares the data flow relations computed with static data flow approaches with the ones observed while executing the program. To this end, the paper introduces a dynamic data flow technique that collects the data flow relations observed during testing. The experimental data discussed in the paper suggest that data flow testing based on static techniques misses many data flow test objectives, and indicate that the amount of missing objectives (false negatives) can be more limiting than the amount of infeasible data flow relations identified statically (false positives). This opens a new area of research of (dynamic) data flow testing techniques that can better encompass the test objectives of data flow testing.

Symbolic execution suffers from problems when analyzing programs that handle complex data structures as their inputs and take decisions over non-linear expressions. For these programs, symbolic execution may incur invalid inputs or unidentified infeasible traces, and may raise large amounts of false alarms. Some symbolic executors tackle these problems by introducing executable preconditions to exclude invalid inputs, and some solvers exploit rewrite rules to address non linear problems. In this paper, we discuss the core limitations of executable preconditions, and address these limitations by proposing invariants specifically designed to harmonize with the lazy initialization algorithm. We exploit rewrite rules applied within the symbolic executor, to address simplifications of inverse relationships fostered from either program-specific calculations or the logic of the verification tasks. We present a symbolic executor that integrates the two techniques, and validate our approach against the verification of a relevant set of properties of the Tactical Separation Assisted Flight Environment. The empirical data show that the integrated approach can improve the effectiveness of symbolic execution.

Service-oriented applications do not fully benefit from standard APIs yet, and many applications fail to use interchangeably all the services that implement a standard service API. This article presents an approach to develop adaptation strategies that improve service interchangeability for service-oriented applications based on standard APIs. In our approach, an adaptation strategy consists of sets of parametric adaptation plans (called test-and-adapt plans), which execute test cases to reveal the occurrence of interchangeability problems, and activate runtime adaptors according to the test results. Throughout this article, we formalize the structure of the parametric test-and-adapt plans and of their execution semantics, present an algorithm for identifying correct execution orders through sets of test-and-adapt plans, provide empirical evidence of the occurrence of interchangeability problems for sample applications and services, and discuss the effectiveness of the approach in terms of avoided failures, runtime overheads and development costs.

Many modern software systems dynamically discover and integrate third party libraries, components and services that comply with standard APIs. Compliance with standard APIs facilitates dynamic binding, but does not always guarantee full behavioral compatibility. For instance, problems that derive from behavior incompatibility are quite frequent in service-oriented applications that dynamically bind service implementations that match API specifications.

SOQUA 2007 aims to bring together researchers, engineers, and practitioners to discuss and evaluate latest challenges, breakthroughs and experiences in the field of software quality assurance, and to identify open issues and future trends in this area. Among the many quality assurance topics, SOQUA 2007 puts special focus on the role that emerging self adaptive and self-healing solutions can play in quality assurance. The program committee had the difficult task to select 17 papers out of 27 high-quality submissions from all over the world. The selected papers cover 11 countries and 5 continents, and many aspects of software quality assurance, including: self-healing and self-adaptive solutions, testing, quality assurance processes, process modeling, failure analysis and anticipation, quality of requirements, and variability modeling. These papers represent a significant contribution to the state of the art in the field. The workshop program consists of 1 keynote address given by Wilhelm Schäfer, 5 paper sessions hosting the authors' presentations, and 2 discussion sessions on hot-topics in the field.

Autonomic communication and autonomic computing can solve many problems in managing complex network and computer systems, as well as network applications, where computing and networking coexist. Autonomic applications must be able to diagnose and repair their own faults automatically. In particular, they must be able to monitor the execution state, understand the behavior of the application and of the executing environment, and interpret monitored data to identify faults and select a repairing strategy. Assertions have been extensively studied in software engineering for identifying deviations from the expected behaviors and thus signal anomalous outcomes. Unfortunately, classic assertions are defined statically at development time and cannot capture unpredictable changes and evolutions in the execution environment. Thus, they do not easily adapt to autonomic applications. The paper proposes a method for the automatic synthesis and adaptation of assertions from the observed behavior of an application, aimed at achieving adaptive application monitoring. We believe that this represents an important basis to derive autonomic mechanisms that can deal with unpredictable situations.

Estimating software fault-proneness early, i.e., predicting the probability of software modules to be faulty, can help in reducing costs and increasing effectiveness of software analysis and testing. The many available static metrics provide important information, but none of them can be deterministically related to software fault-proneness. Fault-proneness models seem to be an interesting alternative, but the work on these is still biased by lack of experimental validation. This paper discusses barriers and problems in using software fault-proneness in industrial environments, proposes a method for building software fault-proneness models based on logistic regression and cross-validation that meets industrial needs, and provides some experimental evidence of the validity of the proposed approach.

Planning and allocating resources for testing is difficult and it is usually done on empirical basis, often leading to unsatisfactory results. The possibility of early estimating the potential faultiness of software could be of great help for planning and executing testing activities. Most research concentrates on the study of different techniques for computing multivariate models and evaluating their statistical validity, but we still lack experimental data about the validity of such models across different software applications.This paper reports an empirical study of the validity of multivariate models for predicting software fault-proneness across different applications. It shows that suitably selected multivariate models can predict fault-proneness of modules of different software packages.

Modern Web applications are mainly distributed systems that exploit the Internet as communication means and the Web as neutral interface to access services and data. The addition of services to Web applications poses problems that are usually tackled at the technology level, but that should be addressed during design to deliver quality Web applications. A typical example of these problems is the Amazon bug, an annoying problem that the user could encounter if after adding products to his shopping cart, he rolls back to a page with a previous version of the cart and tries to buy it. This would make the user buy the last version of the cart's contents, which in some subtle cases could be different from what expected.In this paper, we do not want to discuss all design aspects, but only how provided services/operations should jointly be designed with the rest of the system. We propose a new reference model for Web applications: Operations require a more complex model where they are not simply appended to information and navigation elements, but they can cooperate with them. Besides the reference model, the paper proposes the use of assertions to constraint the behavior of designed operations. Assertions do not only predicate on how data should be modified, but must also take into account how presentation and navigation could be affected by the execution of the operation.

The effectiveness of the software testing process is a key issue for meeting the increasing demand of quality without augmenting the overall costs of software development. The estimation of software fault-proneness is important for assessing costs and quality and thus better planning and tuning the testing process. Unfortunately, no general techniques are available for estimating software fault-proneness and the distribution of faults to identify the correct level of test for the required quality. Although software complexity and testing thoroughness are intuitively related to the costs of quality assurance and the quality of the final product, single software metrics and coverage criteria provide limited help in planning the testing process and assuring the required quality.By using logistic regression, this paper shows how models can be built that relate software measures and software fault-proneness for classes of homogeneous software products. It also proposes the use of cross-validation for selecting valid models even for small data sets.The early results show that it is possible to build statistical models based on historical data for estimating fault-proneness of software modules before testing, and thus better planning and monitoring the testing activities.

Safety critical systems require to be highly reliable and thus special care is taken when verifying them in order to increase the confidence in their behavior. This paper addresses the problem of formal verification of safety critical systems by providing empirical evidence of the practical applicability of symbolic execution and of its usefulness for checking safety-related properties. In this paper, symbolic execution is used for building an operational model of the software on which safety properties, expressed by means of a Path Description Language (PDL), can be assessed.

A study is carried out to investigate whether a correlation exists between the fault-proneness of the software and the measurable attributes of the code and of the testing. A suitable variety of case studies is selected to investigate a methodology applicable to classes of homogeneous products.