Researchers and practitioners alike increasingly often perceive flaky tests as a major challenge in software engineering. They spend a lot of effort trying to detect, repair, and mitigate the negative effects of flaky tests. However, it is yet unclear where and to what extent the costs of flaky tests manifest in industrial Continuous Integration (CI) development processes. In this study, we compile cost factors introduced by flaky tests in CI development from research and practice and derive a cost model that allows gaining insight into the costs incurred. We then instantiate this model in a case study of a large, commercial software project with ~30 developers and ~1M SLoC. We analyze five years of development history, including CI test logs, commits from the Version Control System (VCS), issue tickets, and tracked work time to quantify the cost factors implied by flaky tests. We find that the time spent dealing with flaky tests in the studied project represents at least 2.5% of the productive developer time. This effort is divided into investigating potentially flaky test failures, which accounts for 1.1% of the total time spent, repairing flaky tests adds another 1.3 %, and developing tools to monitor flaky tests adds 0.1 %. Contrary to most other studies, we find the cost for rerunning tests to be negligible and inexpensive. Automatically rerunning a test costs 0.02 cents, while not rerunning and thus letting the pipeline fail results in a manual investigation costing $5.67 in our context. The insights gained from our case study have led to the decision to shift effort from investigation and repair to automatically rerunning tests. Our cost model can help practitioners analyze the cost of flaky tests in their context and make informed decisions. Furthermore, our case study provides a first step to better understand the costs of flaky tests, which can lead researchers to industry-relevant problems.

Android apps can be effectively tested by randomly generating inputs and triggering corresponding events. Most test generators focus on user-triggered events, such as button clicks. However, the state of an app is not only determined by the interactions with a user, but also inputs from the system and other apps, which are called intents in Android. Intent fuzzing, that is, the automated generation of randomized intents as test inputs, has been demonstrated to be an effective means for identifying crashes in apps. However, the behavior of intent handlers is influenced by the state of the app, which may depend on the user’s interactions with the app that triggers corresponding events. Recent test generators have therefore started integrating some of both types of events, leaving open questions about the best way to combine and balance UI inputs and intents. In this paper, we describe a general framework for integrating user events and intents for testing Android apps. We study empirically how to best combine these two types of events, and evaluate the effectiveness of the combination. Our experiments suggest that combining UI inputs and intents reveals substantially higher code coverage as well as more unique crashes (844 on 500 F-Droid apps) than sending only user-events (762) or only intents (511): The combined approach achieves a magnitude higher activity coverage (78.07%) than using only user inputs (70.45%) and sending only intents (58.23%). Furthermore, 121 unique crashes were found only through the combination of UI inputs and intents. Although intent crashes and UI crashes result from similar exception types, they are distinct, which is relevant when comparing test generators.

Programming environments such as Snap, Scratch, and Processing engage learners by allowing them to create programming artifacts such as apps and games, with visual and interactive output. Learning programming with such a media-focused context has been shown to increase retention and success rate. However, assessing these visual, interactive projects requires time and laborious manual effort, and it is therefore difficult to offer automated or real-time feedback to students as they work. In this paper, we introduce SnapCheck, a dynamic testing framework for Snap that enables instructors to author test cases with Condition-Action templates. The goal of SnapCheck is to allow instructors or researchers to author property-based test cases that can automatically assess students' interactive programs with high accuracy. Our evaluation of SnapCheck on 162 code snapshots from a Pong game assignment in an introductory programming course shows that our automated testing framework achieves at least 98% accuracy over all rubric items, showing potentials to use SnapCheck for auto-grading and providing formative feedback to students.

Block-based programming languages like Scratch support learners by providing high-level constructs that hide details and by preventing syntactically incorrect programs. Questions nevertheless frequently arise: Is this program satisfying the given task? Why is my program not working? To support learners and educators, automated program analysis is needed for answering such questions. While adapting existing analyses to process blocks instead of textual statements is straightforward, the domain of programs controlled by block-based languages like Scratch is very different from traditional programs: In Scratch multiple actors, represented as highly concurrent programs, interact on a graphical stage, controlled by user inputs, and while the block-based program statements look playful, they hide complex mathematical operations that determine visual aspects and movement. Analyzing such programs is further hampered by the absence of clearly defined semantics, often resulting from ad-hoc decisions made by the implementers of the programming environment. To enable program analysis, we define the semantics of Scratch using an intermediate language. Based on this intermediate language, we implement the Bastet program analysis framework for Scratch programs, using concepts from abstract interpretation and software model checking. Like Scratch, Bastet is based on Web technologies, written in TypeScript, and can be executed using NodeJS or even directly in a browser. Evaluation on 279 programs written by children suggests that Bastet offers a practical solution for analysis of Scratch programs, thus enabling applications such as automated hint generation, automated evaluation of learner progress, or automated grading.

Block-based programming environments like Scratch foster engagement with computer programming and are used by millions of young learners. Scratch allows learners to quickly create entertaining programs and games, while eliminating syntactical program errors that could interfere with progress. However, functional programming errors may still lead to incorrect programs, and learners and their teachers need to identify and understand these errors. This is currently an entirely manual process. In this paper, we introduce a formal testing framework that describes the problem of Scratch testing in detail. We instantiate this formal framework with the Whisker tool, which provides automated and property-based testing functionality for Scratch programs. Empirical evaluation on real student and teacher programs demonstrates that Whisker can successfully test Scratch programs, and automatically achieves an average of 95.25 % code coverage. Although well-known testing problems such as test flakiness also exist in the scenario of Scratch testing, we show that automated and property-based testing can accurately reproduce and replace the manually and laboriously produced grading efforts of a teacher, and opens up new possibilities to support learners of programming in their struggles.

Major breakthroughs have increased the efficiency and effectiveness of software model checking considerably, such that this technology is now applicable to industrial-scale software. However, verifying the full formal specification of a software system is still considered too complex, and in practice, sets of properties are verified one by one in isolation. We propose an approach that takes the full formal specification as input and first tries to verify all properties simultaneously in one verification run. Our verification algorithm monitors itself and detects situations for which the full set of properties is too complex. In such cases, we perform an automatic decomposition of the full set of properties into smaller sets, and continue the verification seamlessly. To avoid state-space explosion for large sets of properties, we introduce on-the-fly property weaving: properties get weaved into the program's transition system on the fly, during the analysis; which properties to weave and verify is determined dynamically during the verification process. We perform an extensive evaluation based on verification tasks that were derived from 4336 Linux kernel modules, and a set of properties that define the correct usage of the Linux API. Checking several properties simultaneously can lead to a significant performance gain, due to the fact that abstract models share many parts among different properties.

It is commonly understood that a verification tool should provide a counterexample to witness a specification violation. Until recently, software verifiers dumped error witnesses in proprietary formats, which are often neither human- nor machine-readable, and an exchange of witnesses between different verifiers was impossible. To close this gap in software-verification technology, we have defined an exchange format for error witnesses that is easy to write and read by verification tools (for further processing, e.g., witness validation) and that is easy to convert into visualizations that conveniently let developers inspect an error path. To eliminate manual inspection of false alarms, we develop the notion of stepwise testification: in a first step, a verifier finds a problematic program path and, in addition to the verification result FALSE, constructs a witness for this path; in the next step, another verifier re-verifies that the witness indeed violates the specification. This process can have more than two steps, each reducing the state space around the error path, making it easier to validate the witness in a later step. An obvious application for testification is the setting where we have two verifiers: one that is efficient but imprecise and another one that is precise but expensive. We have implemented the technique of error-witness-driven program analysis in two state-of-the-art verification tools, CPAchecker and Ultimate Automizer, and show by experimental evaluation that the approach is applicable to a large set of verification tasks.

Continuous testing during development is a well-established technique for software-quality assurance. Continuous model checking from revision to revision is not yet established as a standard practice, because the enormous resource consumption makes its application impractical. Model checkers compute a large number of verification facts that are necessary for verifying if a given specification holds. We have identified a category of such intermediate results that are easy to store and efficient to reuse: abstraction precisions. The precision of an abstract domain specifies the level of abstraction that the analysis works on. Precisions are thus a precious result of the verification effort and it is a waste of resources to throw them away after each verification run. In particular, precisions are reasonably small and thus easy to store; they are easy to process and have a large impact on resource consumption. We experimentally show the impact of precision reuse on industrial verification problems created from 62 Linux kernel device drivers with 1119 revisions.