As autonomous coding agents increasingly integrate into software development workflows, understanding their testing practices is essential. We study how well tests in a pull request (PR) exercise the code changed by that PR, and whether those tests contain meaningful assertions. Using AIDev dataset v2, we compare three authorship types: AI-Only (all commits authored by agents), Coauthor (mixed human-AI commits), and Human (baseline PRs from the same repository). Analyzing 2,314 Python PRs that modify tests, we measure diff-coverage: the percentage of modified non-test source lines executed by the PR’s tests. AI-Only PRs achieve higher mean diff-coverage (19.96%) than Coauthor (17.35%) and Human PRs (13.09%). Moreover, 80.4% of AI-Only PRs have non-zero diff-coverage, compared to 62.3% for Coauthor and 66.2% for Human. To assess oracle strength, we manually classify assertions in 255 diffs using a four-level taxonomy (L1–L4) with three independent evaluators. Functional assertions (L3) are dominant, regardless of authorship type: 66.7% AI-Only, 80.0% Coauthor, and 69.9% Human. High-quality assertions (L3+L4) appear in over 90% of test files across all groups, with no statistically significant pairwise differences (Fisher’s exact, p > 0.05). Overall, within PRs that include test changes, AI-authored submissions tend to achieve higher coverage of changed code without evidence of weaker assertions, providing empirical evidence to inform strategies for integrating AI-assisted development into software projects.

Configurable software systems offer user-selectable features to tailor them to the target hardware and user requirements. It is almost a rule that, as the number of features increases over time, unintended and inadvertent feature interactions arise. Despite numerous definitions of feature interactions and methods for detecting them, there is no procedure for determining whether the effect of a feature interaction could be, in principle, observed from an external perspective. In this paper, we devise a decision procedure to verify whether the effect of a given feature or potential feature interaction could be isolated by blackbox observations of a set of system configurations. For this purpose, we introduce the notion of blackbox observability, which is based on recent work on counterfactual reasoning on configuration decisions. Direct observability requires a single reference configuration to isolate the effect in question, while the broader notion of general observability relaxes this precondition and suffices with a set of reference configurations. We report on a series of experiments on community benchmarks as well as real-world configuration spaces and models. We found that (1) deciding observability is indeed tractable in real-world settings, (2) constraints in real-world configuration spaces frequently limit observability, and (3) blackbox performance models often include effects that are de facto not observable.

Variability permeates software development to satisfy ever-changing requirements and mass-customization needs. A prime example is the Linux kernel, which employs the C preprocessor to specify a set of related but distinct kernel variants. To study, analyze, and verify variational software, several formal languages have been proposed. For example, the choice calculus has been successfully applied for type checking and symbolic execution of configurable software, while other formalisms have been used for variational model checking, change impact analysis, among other use cases. Yet, these languages have not been formally compared, hence, little is known about their relationships. Crucially, it is unclear to what extent one language subsumes another, how research results from one language can be applied to other languages, and which language is suitable for which purpose or domain. In this paper, we propose a formal framework to compare the expressive power of languages for static (i.e. compile-time) variability. By establishing a common semantic domain to capture a widely used intuition of explicit variability, we can formulate the basic, yet to date neglected, properties of soundness, completeness, and expressiveness for variability languages. We then prove the (un)soundness and (in)completeness of a range of existing languages, and relate their ability to express the same variational systems. We implement our framework as an extensible open source Agda library in which proofs act as correct compilers between languages or differencing algorithms. We find different levels of expressiveness as well as complete and incomplete languages w.r.t. our unified semantic domain, with the choice calculus being among the most expressive languages.

Abstract A product line is an approach for systematically managing configuration options of customizable systems, usually by means of features. Products are generated for configurations consisting of selected features. Product-line evolution can lead to unintended changes to product behavior. We illustrate that updating configurations after product-line evolution requires decisions of both, domain engineers responsible for product-line evolution as well as application engineers responsible for configurations. The challenge is that domain and application engineers might not be able to interact with each other. We propose a formal foundation and a methodology that enables domain engineers to guide application engineers through configuration evolution by sharing knowledge on product-line evolution and by defining automatic update operations for configurations. As an effect, we enable knowledge transfer between those engineers without the need for interactions. We evaluate our methodology on four large-scale industrial product lines. The results of the qualitative evaluation indicate that our method is flexible enough for real-world product-line evolution. The quantitative evaluation indicates that we detect product behavior changes for up to $$55.3\%$$ 55.3 % of the configurations which would not have been detected using existing methods.

Runtime Verification (RV) is a technique to monitor formally-specified properties of the software during its execution. RV has shown to be very effective for bug finding. Unfortunately, RV typically relies on formal specification languages and learning those languages be costly for developers. This paper reports on a study to assess the challenges to specify API properties for the purpose of RV. To that end, we wrote SIESTA, a minimalist specification language, extending Java with two features (the ability to catch calls to specified methods and the ability to access the event history of a given object), and asked inexperienced developers (students) to write specifications in that language for certain parts of the Java API. Among our findings, we observed that 40% of the specifications written by the students matched the ground truth perfectly. The main messages of this work are that 1) it is feasible to use a simple imperative language for specifying properties without significant loss of generality; and that 2) developers are capable of writing specifications in the (programming) language they feel comfortable.

A test case that intermittently passes or fails when performed under the same version of source code and test code is said to be flaky. The presence of flaky tests wastes testing time and effort. The most popular approach in industry to detect flakiness is ReRun. The idea behind ReRun is very simple: failing test cases are re-executed many times looking for inconsistencies in the output. Despite its simplicity, the ReRun strategy is very expensive both in terms of time and in terms of computational resources. This is particularly true for contexts where thousands of test cases are performed on a daily basis. Reducing the rerunning overhead is, thus, of utmost importance. This paper presents SHAKER, an open-source tool for detecting flakiness in time-constrained tests by adding noise in the execution environment. The main idea behind SHAKER is to add stressing tasks that compete with the test execution for the use of resources (CPU or memory). SHAKER is available as a GitHub Actions workflow that can be seamlessly integrated with any GitHub project. Alternatively, SHAKER can also be used via its provided Command Line Interface. In our evaluation, SHAKER was able to discover more flaky tests than ReRun and in a faster way (less re-executions); besides, our approach revealed tens of new flaky tests that went undetected by ReRun even after 50 re-executions. Thanks to its flexibility and ease of use, we believe that SHAKER can be useful for both practitioners and researchers.Demo video: https://youtu.be/7-aiQwOb4rAShaker website: https://star-rg.github.io/shaker

A number of product-line analysis approaches lift analyses such as type checking, model checking, and theorem proving from the level of single programs to the level of product lines. These approaches share concepts and mechanisms that suggest an unexplored potential for reuse of key analysis steps and properties, implementation, and verification efforts. Despite the availability of taxonomies synthesizing such approaches, there still remains the underlying problem of not being able to describe product-line analyses and their properties precisely and uniformly. We propose a formal framework that models product-line analyses in a compositional manner, providing an overall understanding of the space of family-based, feature-based, and product-based analysis strategies. It defines precisely how the different types of product-line analyses compose and inter-relate. To ensure soundness, we formalize the framework, providing mechanized specification and proofs of key concepts and properties of the individual analyses. The formalization provides unambiguous definitions of domain terminology and assumptions as well as solid evidence of key properties based on rigorous formal proofs. To qualitatively assess the generality of the framework, we discuss to what extent it describes five representative product-line analyses targeting the following properties: safety, performance, dataflow facts, security, and functional program properties.

A test is said to be flaky when it non-deterministically passes or fails. Test flakiness negatively affects the effectiveness of regression testing and, consequently, impacts software evolution. Detecting test flakiness is an important and challenging problem. ReRun is the most popular approach in industry to detect test flakiness. It re-executes a test suite on a fixed code version multiple times, looking for inconsistent outputs across executions. Unfortunately, ReRun is costly and unreliable. This paper proposes SHAKER, a lightweight technique to improve the ability of ReRun to detect flaky tests. SHAKER adds noise in the execution environment (e.g., it adds stressor tasks to compete for the CPU or memory). It builds on the observations that concurrency is an important source of flakiness and that adding noise in the environment can interfere in the ordering of events and, consequently, influence on the test outputs. We conducted experiments on a data set with 11 Android apps. Results are very encouraging. SHAKER discovered many more flaky tests than ReRun (95% and 37.5% of the total, respectively) and discovered these flaky tests much faster. In addition, SHAKER was able to reveal 61 new flaky tests that went undetected in 50 re-executions with ReRun.

In 2017, Google announced Kotlin as one of the officially supported languages for Android development. Among the reasons for choosing Kotlin, Google mentioned it is “concise, expressive, and designed to be type and null-safe”. Another important reason is that Kotlin is a language fully interoperable with Java and runs on the JVM. Despite Kotlin's rapid rise in the industry, very little has been done in academia to understand how developers are dealing with the adoption of Kotlin. The goal of this study is to understand how developers are dealing with the recent adoption of Kotlin as an official language for Android development, their perception about the advantages and disadvantages related to its usage, and the most common problems faced by them. This research was conducted using the concurrent triangulation strategy, which is a mixed-method approach. We performed a thorough analysis of 9,405 questions related to Kotlin development for the Android platform on Stack Overflow. Concurrently, we also conducted a basic qualitative research interviewing seven Android developers that use Kotlin to confirm and cross-validate our findings. Our study reveals that developers do seem to find the language easy to understand and to adopt it. This perception begins to change when the functional paradigm becomes more evident. Accordingly to the developers, the readability and legibility are compromised if developers overuse the functional flexibility that the language provides. The developers also consider that Kotlin increases the quality of the produced code mainly due to its null-safety guarantees, but it can also become a challenge when interoperating with Java, despite the interoperability being considered as an advantage. While adopting Kotlin requires some care from developers, its benefits seem to bring many advantages to the platform according to the developers, especially in the aspect of adopting a more modern language while maintaining the consolidated Java-based development environment.

Refactoring engines may have overly strong preconditions preventing developers from applying useful transformations. We find that 32 percent of the Eclipse and JRRT test suites are concerned with detecting overly strong preconditions. In general, developers manually write test cases, which is costly and error prone. Our previous technique detects overly strong preconditions using differential testing. However, it needs at least two refactoring engines. In this work, we propose a technique to detect overly strong preconditions in refactoring engines without needing reference implementations. We automatically generate programs and attempt to refactor them. For each rejected transformation, we attempt to apply it again after disabling the preconditions that lead the refactoring engine to reject the transformation. If it applies a behavior preserving transformation, we consider the disabled preconditions overly strong. We evaluate 10 refactorings of Eclipse and JRRT by generating 154,040 programs. We find 15 overly strong preconditions in Eclipse and 15 in JRRT. Our technique detects 11 bugs that our previous technique cannot detect while missing 5 bugs. We evaluate the technique by replacing the programs generated by JDolly with the input programs of Eclipse and JRRT test suites. Our technique detects 14 overly strong preconditions in Eclipse and 4 in JRRT.

Configurable systems typically use #ifdefs to denote variability. Generating and compiling all configurations may be time-consuming. An alternative consists of using variability-aware parsers, such as TypeChef. However, they may not scale. In practice, compiling the complete systems may be costly. Therefore, developers can use sampling strategies to compile only a subset of the configurations. We propose a change-centric approach to compile configurable systems with #ifdefs by analyzing only configurations impacted by a code change (transformation). We implement it in a tool called CHECKCONFIGMX, which reports the new compilation errors introduced by the transformation. We perform an empirical study to evaluate 3,913 transformations applied to the 14 largest files of BusyBox, Apache HTTPD, and Expat configurable systems. CHECKCONFIGMX finds 595 compilation errors of 20 types introduced by 41 developers in 214 commits (5.46% of the analyzed transformations). In our study, it reduces by at least 50% (an average of 99%) the effort of evaluating the analyzed transformations by comparing with the exhaustive approach without considering a feature model. CHECKCONFIGMX may help developers to reduce compilation effort to evaluate fine-grained transformations applied to configurable systems with #ifdefs.

A key challenge developers might face when evolving a product line is not to inadvertently affect users of existing products. In refactoring and conservative extension scenarios, we can avoid this problem by checking for behavior preservation, either by testing the generated products or by using formal theories. Product line refinement theories support that by requiring behavior preservation for all existing products. However, in many evolution scenarios, such as bug fixing, there is a high chance that only some of the products are refined. To support developers in these and other non full-refinement situations, we define a theory of partial product line refinement that helps to precisely understand which products should not be affected by an evolution scenario. This provides a kind of impact analysis that could, for example, reduce test effort, since products not affected do not need to be tested. Additionally, we formally derive a catalog of eight partial refinement templates that capture evolution scenarios, and associated preconditions, not covered before. Finally, by analyzing 79218 commits from the Linux repository, we find evidence that the proposed templates could cover a number of practical evolution scenarios.

The variability of configurable systems may lead to configuration-related issues (i.e., faults and warnings) that appear only when we select certain configuration options. Previous studies found that issues related to configurability are harder to detect than issues that appear in all configurations, because variability increases the complexity. However, little effort has been put into understanding configuration-related faults (e.g., undeclared functions and variables) and warnings (e.g., unused functions and variables). To better understand the peculiarities of configuration-related undeclared/unused variables and functions, in this paper we perform an empirical study of 15 systems to answer research questions related to how developers introduce these issues, the number of configuration options involved, and the time that these issues remain in source files. To make the analysis of several projects feasible, we propose a strategy that minimizes the initial setup problems of variability-aware tools. We detect and confirm 2 undeclared variables, 14 undeclared functions, 16 unused variables, and 7 unused functions related to configurability. We submit 30 patches to fix issues not fixed by developers. Our findings support the effectiveness of sampling (i.e., analysis of only a subset of valid configurations) because most issues involve two or less configuration options. Nevertheless, by analyzing the version history of the projects, we observe that a number of issues remain in the code for several years. Furthermore, the corpus of undeclared/unused variables and functions gathered is a valuable source to study these issues, compare sampling algorithms, and test and improve variability-aware tools.

A product line refinement theory formalizes safe evolution in terms of a refinement notion, which does not rely on particular languages for the elements that constitute a product line. Based on this theory, we can derive refinement templates to support safe evolution scenarios. To do so, we need to provide formalizations for particular languages, to specify and prove the templates. Without a systematic approach, this leads to many similar templates and thus repetitive verification tasks. We investigate and explore similarities between these concrete languages, which ultimately results in a product line of theories, where different languages correspond to features, and products correspond to theory instantiations. This also leads to specifying refinement templates at a higher abstraction level, which, in the long run, reduces the specification and proof effort, and also provides the benefits of reusing such templates for additional languages plugged into the theory. We use the Prototype Verification System to encode and prove soundness of the theories and their instantiations. Moreover, we also use the refinement theory to reason about safe evolution of the proposed product line of theories.

A product line is often developed in the context of a set of related product lines. When supporting separate feature development, we might have product populations, with product line versions being simultaneously developed in different branches. Multi product lines involve a number of product lines that depend on each other. A product line refinement notion formalizes safe evolution, but this is not sufficient for reasoning over sets of product lines. We propose refinement notions and compositionality properties that help to explain how we can support modular development in these contexts. Thus, we formally define the foundations for safe and modular evolution of product populations and multi product lines, enabling developers to perform changes in a systematic manner.

Variability-aware systems are subject to the coevolution of variability models and related artifacts. Surprisingly, little knowledge exists to understand such coevolution in practice. This shortage is directly reflected in existing approaches and tools for variability management, as they fail to provide effective support for such a coevolution. To understand how variability models and related artifacts coevolve in a large and complex real-world variability-aware system, we inspect over 500 Linux kernel commits spanning almost four years of development. We collect a catalog of evolution patterns, capturing the coevolution of the Linux kernel variability model, Makefiles, and C source code. Further, we extract general findings to guide further research and tool development.

The adoption of a product line strategy can bring significant productivity and time to market improvements. However, evolving a product line is risky because it might impact many products and their users. So when evolving a product line to introduce new features or to improve its design, it is important to make sure that the behavior of existing products is not affected. In fact, to preserve the behavior of existing products one usually has to analyze different artifacts, like feature models, configuration knowledge and the product line core assets. To better understand this process, in this paper we discover and analyze concrete product line evolution scenarios and, based on the results of this study, we describe a number of safe evolution templates that developers can use when working with product lines. For each template, we show examples of their use in existing product lines. We evaluate the templates by also analyzing the evolution history of two different product lines and demonstrating that they can express the corresponding modifications and then help to avoid the mistakes that we identified during our analysis.