Omitted variable bias occurs when a statistical model leaves out variables that are relevant determinants of the studied effects. This results in the model attributing the missing variables’ effect to some of the included variables—hence over- or under-estimating the latter’s true effect. Omitted variable bias presents a significant threat to the validity of empirical research, particularly in non-experimental studies such as those common in empirical software engineering. This paper illustrates the impact of omitted variable bias on two illustrative examples in the software engineering domain, and uses them to present methods to investigate the possible presence of omitted variable bias, to estimate its impact, and to mitigate its drawbacks. The analysis techniques we present are based on causal structural models of the variables of interest, which provide a practical, intuitive summary of the key relations among variables. This paper demonstrates a sequence of analysis steps that inform the design and execution of similar empirical studies in software engineering. An important observation is that it pays off to invest effort investigating omitted variable bias before actually executing an empirical study, because this effort can lead to a more solid study design, and to a reduction in its threats to validity.

Automated program repair (APR) techniques have achieved conspicuous progress, and are now capable of producing genuinely correct fixes in scenarios that were well beyond their capabilities only a few years ago. Nevertheless, even when an APR technique can find a correct fix for a bug, it still runs the risk of ranking the fix lower than other patches that are plausible (they pass all available tests) but incorrect. This can seriously hurt the technique’s practical effectiveness, as the user will have to peruse a larger number of patches before finding the correct one. This paper presents PrevaRank , a technique that ranks plausible patches produced by any APR technique according to their feature similarity with historic programmer-written fixes for similar bugs. PrevaRank implements simple heuristics, which help make it scalable and applicable to any APR tool that produces plausible patches. In our experimental evaluation, after training PrevaRank on the fix history of 81 open-source Java projects, we used it to rank patches produced by 8 Java APR tools on 168 Defects4J bugs. PrevaRank consistently improved the ranking of correct fixes: for example, it ranked a correct fix within the top-3 positions in 27% more cases than the original tools did. Other experimental results indicate that PrevaRank works robustly with a variety of APR tools and bugs, with negligible overhead. • Ranks APR patches via category-conditioned syntactic frequency patterns. • Improves top-3 correct-patch placement by ＋27% over tools’ native order. • Evaluated on 168 Defects4J bugs, 8 tools, 23,032 plausible patches.

International audience

Abstract Subtyping in object-oriented languages is widely based on Liskov’s substitution principle, which offers static correctness guarantees of type safety while abstracting implementation details. Unfortunately, the type systems of languages like Java cannot statically enforce full behavioral substitutability, and in fact there are numerous examples of libraries some of whose components are related by inheritance but not substitutable (for example, because they do not implement “optional” operations). In this paper, we present a novel approach to precisely specify and reason about substitutability in JVM languages. A distinctive feature of our approach is that it targets JVM bytecode, as opposed to a program’s source code, as it is based on the ByteBack deductive verifier. To support reasoning about substitutability, we extended ByteBack with ghost specifications, a (restricted) form of class invariants, and substitutability-preserving specification inheritance (precondition weakening and postcondition strengthening). Equipped with these features, ByteBack can now reason precisely about behavioral substitutability violations in a way that is applicable to realistic examples (such as with optional operations of Java’s interface). Our experiments also demonstrate that ByteBack can analyze substitutability in programs written in a combination of JVM languages, including multi-language code where Scala or Kotlin code interacts with Java libraries.

A program’s exceptional behavior can substantially complicate its control flow, and hence accurately reasoning about the program’s correctness. On the other hand, formally verifying realistic programs is likely to involve exceptions—a ubiquitous feature in modern programming languages. In this article, we present a novel approach to verify the exceptional behavior of Java programs, which extends our previous work on ByteBack . ByteBack works on a program’s bytecode, while providing means to specify the intended behavior at the source-code level; this approach sets ByteBack apart from most state-of-the-art verifiers that target source code. To explicitly model a program’s exceptional behavior in a way that is amenable to formal reasoning, we introduce Vimp: a high-level bytecode representation that extends the Soot framework’s Jimple with verification-oriented features, thus serving as an intermediate layer between bytecode and the Boogie intermediate verification language. Working on bytecode through this intermediate layer brings flexibility and adaptability to new language versions and variants: as our experiments demonstrate, ByteBack can verify programs involving exceptional behavior in all versions of Java, as well as in Scala and Kotlin (two other popular JVM languages).

Abstract Android’s intents provide a form of inter-app communication with implicit, capability-based matching of senders and receivers. Such kind of implicit addressing provides some much-needed flexibility but also increases the risk of introducing information flow security bugs and vulnerabilities—as there is no standard way to specify what permissions are required to access the data sent through intents, so that it is handled properly. To mitigate such risks of intent-based communication, this paper introduces IntentRepair, an automated technique to detect such information flow security leaks and to automatically repair them. IntentRepair first finds sender and receiver modules that may communicate via intents, and such that the sender sends sensitive information that the receiver forwards to a public channel. To prevent this flow, IntentRepair patches the sender so that it also includes information about the permissions needed to access the data; and the receiver so that it will only disclose the sensitive information if it possesses the required permissions. We evaluated a prototype implementation of IntentRepair on 869 Android open-source apps, showing that it is effective in automatically detecting and repairing information flow security bugs that originate in implicit intent-based communication, introducing only a modest overhead in terms of patch size.

Abstract As research in automatically detecting bugs grows and produces new techniques, having suitable collections of programs with known bugs becomes crucial to reliably and meaningfully compare the effectiveness of these techniques. Most of the existing approaches rely on benchmarks collecting manually curated real-world bugs, or synthetic bugs seeded into real-world programs. Using real-world programs entails that extending the existing benchmarks or creating new ones remains a complex time-consuming task. In this paper, we propose a complementary approach that automatically generates programs with seeded bugs. Our technique, called HyperPUT, builds C programs from a “seed” bug by incrementally applying program transformations (introducing programming constructs such as conditionals, loops, etc.) until a program of the desired size is generated. In our experimental evaluation, we demonstrate how HyperPUT can generate buggy programs that can challenge in different ways the capabilities of modern bug-finding tools, and some of whose characteristics are comparable to those of bugs in existing benchmarks. These results suggest that HyperPUT can be a useful tool to support further research in bug-finding techniques—in particular their empirical evaluation.

-is a crucial element of the method's documentation that clients should know to properly use it. Unfortunately, exceptional behavior is often poorly documented, and sensitive to changes in a project's implementation details that can be onerous to keep synchronized with the documentation. We present wit, an automated technique that extracts the exception preconditions of Java methods and constructors. wit uses static analysis to analyze the paths in a method's implementation that lead to throwing an exception. wit's analysis is precise, in that it only reports exception preconditions that are correct and correspond to feasible exceptional behavior. It is also lightweight: it only needs the source code of the class (or classes) to be analyzed- without building or running the whole project. To this end, its design uses heuristics that give up some completeness (wit cannot infer all exception preconditions) in exchange for precision and ease of applicability. We ran wit on the JDK and 46 Java projects, where it discovered 30 487 exception preconditions in 24 461 methods, taking less than two seconds per analyzed public method on average. A manual analysis of a significant sample of these exception preconditions confirmed that wit is 100% precise, and demonstrated that it can document the exceptional behavior of Java methods.

Abstract Despite its massive popularity as a programming language, especially in novel domains like data science programs, there is comparatively little research about fault localization that targets Python. Even though it is plausible that several findings about programming languages like C/C++ and Java—the most common choices for fault localization research—carry over to other languages, whether the dynamic nature of Python and how the language is used in practice affect the capabilities of classic fault localization approaches remain open questions to investigate. This paper is the first multi-family large-scale empirical study of fault localization on real-world Python programs and faults. Using Zou et al.’s recent large-scale empirical study of fault localization in Java (Zou et al. 2021) as the basis of our study, we investigated the effectiveness (i.e., localization accuracy), efficiency (i.e., runtime performance), and other features (e.g., different entity granularities) of seven well-known fault-localization techniques in four families (spectrum-based, mutation-based, predicate switching, and stack-trace based) on 135 faults from 13 open-source Python projects from the BugsInPy curated collection (Widyasari et al. 2020). The results replicate for Python several results known about Java, and shed light on whether Python’s peculiarities affect the capabilities of fault localization. The replication package that accompanies this paper includes detailed data about our experiments, as well as the tool FauxPy that we implemented to conduct the study.

There is abundant observational data in the software engineering domain, whereas running large-scale controlled experiments is often practically impossible. Thus, most empirical studies can only report statistical correlations —instead of potentially more insightful and robust causal relations. To support analyzing purely observational data for causal relations and to assess any differences between purely predictive and causal models of the same data, this article discusses some novel techniques based on structural causal models (such as directed acyclic graphs of causal Bayesian networks). Using these techniques, one can rigorously express, and partially validate, causal hypotheses and then use the causal information to guide the construction of a statistical model that captures genuine causal relations—such that correlation does imply causation. We apply these ideas to analyzing public data about programmer performance in Code Jam, a large world-wide coding contest organized by Google every year. Specifically, we look at the impact of different programming languages on a participant’s performance in the contest. While the overall effect associated with programming languages is weak compared to other variables—regardless of whether we consider correlational or causal links—we found considerable differences between a purely associational and a causal analysis of the very same data. The takeaway message is that even an imperfect causal analysis of observational data can help answer the salient research questions more precisely and more robustly than with just purely predictive techniques—where genuine causal effects may be confounded.

Modern software development heavily relies on reusing third-party libraries; this makes developers more productive, but may also lead to misuses or other kinds of design issues. In this paper, we focus on the exceptional behavior of library methods, and propose to detect client code that may trigger such exceptional behavior. As we demonstrate on several examples of open-source projects, exceptional behavior in clients often naturally suggests improvements to the documentation, tests, runtime checks, and annotations of the clients.In order to automatically detect client calls that may trigger exceptional behavior in library methods, we show how to repurpose existing techniques to extract a method’s exception precondition—the condition under which the method throws an exception. To demonstrate the feasibility of our approach, we applied it to 1,523 open-source Java projects, where it found 4,115 cases of calls to library methods that may result in an exception. We manually analyzed 100 of these cases, confirming that the approach is capable of uncovering several interesting opportunities for code improvements.

Even though neural network (NN) programs are often written in Python, using general-purpose test-generation tools for Python to test them is likely to be ineffective, as these tools do not support the particular input constraints that NN programs often require. To address this challenge, we present aNNoTest: an automated unit-test generation tool for NN programs written in Python. aNNoTest offers a simple annotation language that is suitable to concisely express the usual input constraints of NN programs; it then uses these annotations to precisely generate valid inputs that are capable of revealing bugs. This short paper describes how aNNoTest works in practice, and reports some experiments that demonstrate its effectiveness as a bug-finding tool for NN programs. aNNoTest is available as open source.

As neural networks are increasingly included as core components of safety–critical systems, developing effective testing techniques specialized for them becomes crucial. The bulk of the research has focused on testing neural-network models; but these models are defined by writing programs, and there is growing evidence that these neural-network programs often have bugs too. This paper presents aNNoTest: an approach to generating test inputs for neural-network programs. A fundamental challenge is that the dynamically-typed languages (e.g., Python) commonly used to program neural networks cannot express detailed constraints about valid function inputs (e.g., matrices with certain dimensions). Without knowing these constraints, automated test-case generation is prone to producing invalid inputs, which trigger spurious failures and are useless for identifying real bugs. To address this problem, we introduce a simple annotation language tailored for concisely expressing valid function inputs in neural-network programs. aNNoTest takes as input an annotated program, and uses property-based testing to generate random inputs that satisfy the validity constraints. In the paper, we also outline guidelines that simplify writing aNNoTest annotations. We evaluated aNNoTest on 19 neural-network programs from Islam et al’s survey. Islam et al. (2019), which we manually annotated following our guidelines — producing 6 annotations per tested function on average. aNNoTest automatically generated test inputs that revealed 94 bugs, including 63 bugs that the survey reported for these projects. These results suggest that aNNoTest can be a valuable approach to finding widespread bugs in real-world neural-network programs.

A key challenge in generate-and-validate automated program repair is directing the search for fixes so that it can efficiently find those that are more likely to be correct. To this end, several techniques use machine learning to capture the features of programmer-written fixes. In existing approaches, fitting the model typically takes placebeforefix generation and is independent of it: the fix generation process uses the learned model as one of its inputs. However, the intermediate outcomes of an ongoing fix generation process often provide valuable information about which candidate fixes were “better”; this information could profitably be used to retrain the model, so that each new iteration of the fixing process would also learn from the outcome of previous ones. In this paper, we propose theLianatechnique for automated program repair, which is based on this idea ofrepeatedlylearning the features of generated fixes. To this end,Lianauses a fine-grained model that combines information about fix characteristics, their relations to the fixing context, and the results of test execution. The model is initially trained offline, and then repeatedly updated online as the fix generation process unravels; at any step, the most up-to-date model is used to guide the search for fixes—prioritizing those that are more likely to include the right ingredients. In an experimental evaluation on 732 real-world Java bugs from 3 popular benchmarks,Lianabuilt correct fixes for 134 faults (83 ranked as first in its output)— improving over several other generate-and-validate program repair tools according to various measures.

When a method throws an exception—its exception precondition—is a crucial element of the method’s documentation that clients should know to properly use it. Unfortunately, exceptional behavior is often poorly documented, and sensitive to changes in a project’s implementation details that can be onerous to keep synchronized with the documentation.We present WIT, an automated technique that extracts the exception preconditions of Java methods. WIT uses static analysis to analyze the paths in a method’s implementation that lead to throwing an exception. WIT’s analysis is precise, in that it only reports exception preconditions that are correct and correspond to feasible exceptional behavior. It is also lightweight: it only needs the source code of the class (or classes) to be analyzed— without building or running the whole project. To this end, its design uses heuristics that give up some completeness (WIT cannot infer all exception preconditions) in exchange for precision and ease of applicability.We ran WIT on 46 Java projects, where it discovered 11 875 exception preconditions in 10 234 methods, taking just 1 second per method on average. A manual analysis of a significant sample of these exception preconditions confirmed that WIT is 100% precise, and demonstrated that it can accurately and automatically document the exceptional behavior of Java methods.

Static analyzers have become increasingly popular both as developer tools and as subjects of empirical studies. Whereas static analysis tools exist for disparate programming languages, the bulk of the empirical research has focused on the popular Java programming language. In this paper, we investigate to what extent some known results about using static analyzers for Java change when considering C#-another popular object-oriented language. To this end, we combine two replications of previous Java studies. First, we study which static analysis tools are most widely used among C# developers, and which warnings are more commonly reported by these tools on open-source C# projects. Second, we develop and empirically evaluate EagleRepair: a technique to automatically fix code in response to static analysis warnings; this is a replication of our previous work for Java [20]. Our replication indicates, among other things, that 1) static code analysis is fairly popular among C# developers too; 2) Re-Sharper is the most widely used static analyzer for C#; 3) several static analysis rules are commonly violated in both Java and C# projects; 4) automatically generating fixes to static code analysis warnings with good precision is feasible in C#. The EagleRepair tool developed for this research is available as open source.

Resource leaks – a program does not release resources it previously acquired – are a common kind of bug in Android applications. Even with the help of existing techniques to automatically detect leaks, writing a leak-free program remains tricky. One of the reasons is Android’s event-driven programming model, which complicates the understanding of an application’s overall control flow. In this paper, we present : a technique to automatically detect and fix resource leaks in Android applications. builds a succinct abstraction of an app’s control flow, and uses it to find execution traces that may leak a resource. The information built during detection also enables automatically building a fix – consisting of release operations performed at appropriate locations – that removes the leak and does not otherwise affect the application’s usage of the resource. An empirical evaluation on resource leaks from the curated collection demonstrates that ’s approach is scalable, precise, and produces correct fixes for a variety of resource leak bugs: automatically found and repaired 50 leaks that affect 9 widely used resources of the Android system, including all those collected by for those resources; on average, it took just 2 min to detect and repair a leak. also compares favorably to Relda2/RelFix – the only other fully automated approach to repair Android resource leaks – since it can often detect more leaks with higher precision and producing smaller fixes. These results indicate that can provide valuable support to enhance the quality of Android applications in practice.

Statistical analysis is the tool of choice to turn data into information and then information into empirical knowledge. However, the process that goes from data to knowledge is long, uncertain, and riddled with pitfalls. To be valid, it should be supported by detailed, rigorous guidelines that help ferret out issues with the data or model and lead to qualified results that strike a reasonable balance between generality and practical relevance. Such guidelines are being developed by statisticians to support the latest techniques for Bayesian data analysis. In this article, we frame these guidelines in a way that is apt to empirical research in software engineering. To demonstrate the guidelines in practice, we apply them to reanalyze a GitHub dataset about code quality in different programming languages. The dataset’s original analysis [Ray et al. 55 ] and a critical reanalysis [Berger et al. 6 ] have attracted considerable attention—in no small part because they target a topic (the impact of different programming languages) on which strong opinions abound. The goals of our reanalysis are largely orthogonal to this previous work, as we are concerned with demonstrating, on data in an interesting domain, how to build a principled Bayesian data analysis and to showcase its benefits. In the process, we will also shed light on some critical aspects of the analyzed data and of the relationship between programming languages and code quality—such as the impact of project-specific characteristics other than the used programming language. The high-level conclusions of our exercise will be that Bayesian statistical techniques can be applied to analyze software engineering data in a way that is principled, flexible, and leads to convincing results that inform the state-of-the-art while highlighting the boundaries of its validity. The guidelines can support building solid statistical analyses and connecting their results. Thus, they can help buttress continued progress in empirical software engineering research.

A key goal of empirical research in software engineering is to assess practical significance, which answers the question whether the observed effects of some compared treatments show a relevant difference in practice in realistic scenarios. Even though plenty of standard techniques exist to assess statistical significance, connecting it to practical significance is not straightforward or routinely done; indeed, only a few empirical studies in software engineering assess practical significance in a principled and systematic way. In this paper, we argue that Bayesian data analysis provides suitable tools to assess practical significance rigorously. We demonstrate our claims in a case study comparing different test techniques. The case study's data was previously analyzed (Afzalet al., 2015) using standard techniques focusing on statistical significance. Here, we build a multilevel model of the same data, which we fit and validate using Bayesian techniques. Our method is to apply cumulative prospect theory on top of the statistical model to quantitatively connect our statistical analysis output to a practically meaningful context. This is then the basis both for assessing and arguing for practical significance. Our study demonstrates that Bayesian analysis provides a technically rigorous yet practical framework for empirical software engineering. A substantial side effect is that any uncertainty in the underlying data will be propagated through the statistical model, and its effects on practical significance are made clear. Thus, in combination with cumulative prospect theory, Bayesian analysis supports seamlessly assessing practical significance in an empirical software engineering context, thus potentially clarifying and extending the relevance of research for practitioners.

Fault localization is a crucial step of automated program repair, because accurately identifying program locations that are most closely implicated with a fault greatly affects the effectiveness of the patching process. An ideal fault localization technique would provide precise information while requiring moderate computational resources—to best support an efficient search for correct fixes. In contrast, most automated program repair tools use standard fault localization techniques—which are not tightly integrated with the overall program repair process, and hence deliver only subpar efficiency. In this paper, we presentretrospective fault localization: a novel fault localization technique geared to the requirements of automated program repair. A key idea of retrospective fault localization is to reuse the outcome of failed patch validation to support mutation-based dynamic analysis—providing accurate fault localization information without incurring onerous computational costs. We implemented retrospective fault localization in a tool calledRestore—based on theJaidJava program repair system. Experiments involving faults from theDefects4Jstandard benchmark indicate that retrospective fault localization can boost automated program repair:Restoreefficiently explores a large fix space, delivering state-of-the-art effectiveness (41Defects4Jbugs correctly fixed, 8 of which no other automated repair tool for Java can fix) while simultaneously boosting performance (speedup over 3 compared toJaid). Retrospective fault localization is applicable to any automated program repair techniques that rely on fault localization and dynamic validation of patches.

Exceptions often signal faulty or undesired behavior; hence, high-quality test suites should also target exceptional behavior. This paper is a large-scale study of exceptional tests-which exercise exceptional behavior-in 1 157 open-source Java projects hosted on GitHub. We analyzed JUnit exceptional tests to understand what kinds of exceptions are more frequently tested, what coding patterns are used, and how features of a project, such as its size and number of contributors, correlate to the characteristics of its exceptional tests. We found that exceptional tests are only 13% of all tests, but tend to be larger than other tests on average; unchecked exceptions are tested twice as frequently as checked ones; 42% of all exceptional tests use try/catch blocks and usually are larger than those using other idioms; and bigger projects with more contributors tend to have more exceptional tests written using different styles. The paper also zeroes in on several detailed examples involving some of the largest analyzed projects, which refine the empirical results with qualitative evidence. The study's findings, and the capabilities of the tool we developed to analyze exceptional tests, suggest several implications for the practice of software development and for follow-up empirical studies.

Abstract VerifyThis is a series of program verification competitions that emphasize the human aspect: participants tackle the verification of detailed behavioral properties—something that lies beyond the capabilities of fully automatic verification and requires instead human expertise to suitably encode programs, specifications, and invariants. This paper describes the 8th edition of VerifyThis, which took place at ETAPS 2019 in Prague. Thirteen teams entered the competition, which consisted of three verification challenges and spanned 2 days of work. This report analyzes how the participating teams fared on these challenges, reflects on what makes a verification challenge more or less suitable for the typical VerifyThis participants, and outlines the difficulties of comparing the work of teams using wildly different verification approaches in a competition focused on the human aspect.

Most techniques for automated program repair (APR) use tests to drive the repair process; this makes them prone to generating spurious repairs that overfit the available tests unless additional information about expected program behavior is available. Our previous work onJaid, an APR technique for Java programs, showed that constructing detailed state abstractions—similar to those employed by techniques for programs with contracts—from plain Java code without any special annotations provides valuable additional information, and hence helps mitigate the overfitting problem. This paper extends the work onJaidwith a comprehensive experimental evaluation involving 693 bugs in three different benchmark suites. The evaluation shows, among other things, that: 1)Jaidis effective: it produced correct fixes for over 15 percent of all bugs, with a precision of nearly 60 percent; 2)Jaidis reasonably efficient: on average, it took less than 30 minutes to output a correct fix; 3)Jaidis competitive with the state of the art, as it fixed more bugs than any other technique, and 11 bugs that no other tool can fix; 4)Jaidis robust: its heuristics are complementary and their effectiveness does not depend on the fine-tuning of parameters. The experimental results also indicate the main trade-offs involved in designing an APR technique based on tests, as well as possible directions for further progress in this line of work.

Statistics comes in two main flavors: frequentist and Bayesian. For historical and technical reasons, frequentist statistics have traditionally dominated empirical data analysis, and certainly remain prevalent in empirical software engineering. This situation is unfortunate because frequentist statistics suffer from a number of shortcomings-such as lack of flexibility and results that are unintuitive and hard to interpret-that curtail their effectiveness when dealing with the heterogeneous data that is increasingly available for empirical analysis of software engineering practice. In this paper, we pinpoint these shortcomings, and present Bayesian data analysis techniques that provide tangible benefits-as they can provide clearer results that are simultaneously robust and nuanced. After a short, high-level introduction to the basic tools of Bayesian statistics, we present the reanalysis of two empirical studies on the effectiveness of automatically generated tests and the performance of programming languages. By contrasting the original frequentist analyses with our new Bayesian analyses, we demonstrate the concrete advantages of the latter. To conclude we advocate a more prominent role for Bayesian statistical techniques in empirical software engineering research and practice.

Static code analysis tools such as FindBugs and SonarQube are widely used on open-source and industrial projects to detect a variety of issues that may negatively affect the quality of software. Despite these tools' popularity and high level of automation, several empirical studies report that developers normally fix only a small fraction (typically, less than 10% [1]) of the reported issues-so-called "warnings". If these analysis tools could also automatically provide suggestions on how to fix the issues that trigger some of the warnings, their feedback would become more actionable and more directly useful to developers. In this work, we investigate whether it is feasible to automatically generate fix suggestions for common warnings issued by static code analysis tools, and to what extent developers are willing to accept such suggestions into the codebases they're maintaining. To this end, we implemented a Java program transformation technique that fixes 11 distinct rules checked by two well-known static code analysis tools (SonarQube and SpotBugs). Fix suggestions are generated automatically based on templates, which are instantiated in a way that removes the source of the warnings; templates for some rules are even capable of producing multi-line patches. We submitted 38 pull requests, including 920 fixes generated automatically by our technique for various open-source Java projects, including the Eclipse IDE and both SonarQube and SpotBugs tools. At the time of writing, project maintainers accepted 84% of our fix suggestions (95% of them without any modifications). These results indicate that our approach to generating fix suggestions is feasible, and can help increase the applicability of static code analysis tools.

No abstract available.

Abstract The comprehensive functionality and nontrivial design of realistic general-purpose container libraries pose challenges to formal verification that go beyond those of individual benchmark problems mainly targeted by the state of the art. We present our experience verifying the full functional correctness of EiffelBase2: a container library offering all the features customary in modern language frameworks, such as external iterators, and hash tables with generic mutable keys and load balancing. Verification uses the automated deductive verifier AutoProof, which we extended as part of the present work. Our results indicate that verification of a realistic container library (135 public methods, 8400 LOC) is possible with moderate annotation overhead (1.4 lines of specification per LOC) and good performance (0.2 s per method on average).

Automated program repair (APR) is a promising approach to automatically fixing software bugs. Most APR techniques use tests to drive the repair process; this makes them readily applicable to realistic code bases, but also brings the risk of generating spurious repairs that overfit the available tests. Some techniques addressed the overfitting problem by targeting code using contracts (such as pre- and postconditions), which provide additional information helpful to characterize the states of correct and faulty computations; unfortunately, mainstream programming languages do not normally include contract annotations, which severely limits the applicability of such contract-based techniques. This paper presents JAID, a novel APR technique for Java programs, which is capable of constructing detailed state abstractions-similar to those employed by contract-based techniques-that are derived from regular Java code without any special annotations. Grounding the repair generation and validation processes on rich state abstractions mitigates the overfitting problem, and helps extend APR's applicability: in experiments with the DEFECTS4J benchmark, a prototype implementation of JAID produced genuinely correct repairs, equivalent to those written by programmers, for 25 bugs-improving over the state of the art of comparable Java APR techniques in the number and kinds of correct fixes.

We present the integration of the AutoFix automated program repair technique into the EiffelStudio Development Environment. AutoFix presents itself like a recommendation system capable of automatically finding bugs and suggesting fixes in the form of source-code patches. Its performance suggests usage scenarios where it runs in the background or during work interruptions, displaying fix suggestions as they become available. This is a contribution towards the vision of semantic Integrated Development Environments, which offer powerful automated functionality within interfaces familiar to developers. A screencast highlighting the main features of AutoFix can be found at: http://youtu.be/Ff2ULiyL-80.

Sometimes debates on programming languages are more religious than scientific. Questions about which language is more succinct or efficient, or makes developers more productive are discussed with fervor, and their answers are too often based on anecdotes and unsubstantiated beliefs. In this study, we use the largely untapped research potential of Rosetta Code, a code repository of solutions to common programming tasks in various languages, which offers a large data set for analysis. Our study is based on 7'087 solution programs corresponding to 745 tasks in 8 widely used languages representing the major programming paradigms (procedural: C and Go, object-oriented: C# and Java, functional: F# and Haskell, scripting: Python and Ruby). Our statistical analysis reveals, most notably, that: functional and scripting languages are more concise than procedural and object-oriented languages, C is hard to beat when it comes to raw speed on large inputs, but performance differences over inputs of moderate size are less pronounced and allow even interpreted languages to be competitive, compiled strongly-typed languages, where more defects can be caught at compile time, are less prone to runtime failures than interpreted or weakly-typed languages. We discuss implications of these results for developers, language designers, and educators.

Verifiers that can prove programs correct against their full functional specification require, for programs with loops, additional annotations in the form of loop invariants-properties that hold for every iteration of a loop. We show that significant loop invariant candidates can be generated by systematically mutating postconditions; then, dynamic checking (based on automatically generated tests) weeds out invalid candidates, and static checking selects provably valid ones. We present a framework that automatically applies these techniques to support a program prover, paving the way for fully automatic verification without manually written loop invariants: Applied to 28 methods (including 39 different loops) from various java.util classes (occasionally modified to avoid using Java features not fully supported by the static checker), our DYNAMATE prototype automatically discharged 97 percent of all proof obligations, resulting in automatic complete correctness proofs of 25 out of the 28 methods-outperforming several state-of-the-art tools for fully automatic verification.

Collaborative software development requires programmers to coordinate their work and merge individual contributions into a consistent shared code base. Traditionally, coordination follows a series of update-modify-commit" cycles, where merge conflicts arise upon committing if individual modifications have diverged and must be explicitly reconciled. Researchers have been suggesting that providing timely awareness information about "who's changing what" may not only help deal with conflicts but, more generally, improve the effectiveness of collaboration. This paper investigates the impact of awareness information in the context of globally distributed software development. Based on an analysis of data from 105 student developers constituting 12 development teams located in different countries, we analyze, among other things: 1) the frequency of merge conflicts and insufficient awareness, 2) the impact of distribution on team awareness, 3) the perceived impact of conflicts and lack of awareness on productivity, motivation, and project punctuality. Our findings include: 1) lack of awareness occurs more frequently than merge conflicts, 2) information about remote team members is missing roughly as often as information about colocated ones, 3) insufficient awareness information affects more negatively programmer's performance than merge conflicts.

Previous work has shown that reasoning with real-time temporal logics is often simpler when restricted to models with bounded variability-where no more than v events may occur every V time units, for given v, V. When reasoning about formulas with intrinsic bounded variability, one can employ the simpler techniques that rely on bounded variability, without any loss of generality. What is then the complexity of algorithmically deciding which formulas have intrinsic bounded variability? In this paper, we study the problem with reference to Metric Temporal Logic (MTL). We prove that deciding bounded variability of MTL formulas is undecidable over dense-time models, but with a undecidability degree lower than generic dense-time MTL satisfiability. Over discrete-time models, instead, deciding MTL bounded variability has the same exponential-space complexity as satisfiability. To complement these negative results, we also briefly discuss small fragments of MTL that are more amenable to reasoning about bounded variability.

This paper describes AutoFix, an automatic debugging technique that can fix faults in general-purpose software. To provide high-quality fix suggestions and to enable automation of the whole debugging process, AutoFix relies on the presence of simple specification elements in the form of contracts (such as pre- and postconditions). Using contracts enhances the precision of dynamic analysis techniques for fault detection and localization, and for validating fixes. The only required user input to the AutoFix supporting tool is then a faulty program annotated with contracts; the tool produces a collection of validated fixes for the fault ranked according to an estimate of their suitability. In an extensive experimental evaluation, we applied AutoFix to over 200 faults in four code bases of different maturity and quality (of implementation and of contracts). AutoFix successfully fixed 42 percent of the faults, producing, in the majority of cases, corrections of quality comparable to those competent programmers would write; the used computational resources were modest, with an average time per fix below 20 minutes on commodity hardware. These figures compare favorably to the state of the art in automated program fixing, and demonstrate that the AutoFix approach is successfully applicable to reduce the debugging burden in real-world scenarios.

Modern software development extensively involves reusing library components accessed through their Application Programming Interfaces (APIs). Usability is therefore a fundamental goal of API design, but rigorous empirical studies of API usability are still relatively uncommon. In this paper, we present the design of an API usability study which combines interview questions based on the cognitive dimensions framework, with systematic observations of programmer behavior while solving programming tasks based on ``tokens''. We also discuss the implementation of the study to assess the usability of a persistence library API (offering functionalities such as storing objects into relational databases). The study involved 25 programmers (including students, researchers, and professionals), and provided additional evidence to some critical features evidenced by related studies, such as the difficulty of finding good names for API features and of discovering relations between API types. It also discovered new issues relevant to API design, such as the impact of flexibility, and confirmed the crucial importance of accurate documentation for usability.

Debugging - the process of finding and correcting programming mistakes - faces too the challenges of distributed and collaborative development. The debugging tools commonly used by programmers are integrated into traditional development environments such as Eclipse or Visual Studio, and hence do not offer specific features for collaboration or remote shared usage. In this paper, we describe CDB, a debugging technique and integrated tool specifically designed to support effective collaboration among developers during shared debugging sessions. We also discuss the design and results of an empirical study aimed at identifying features that can ameliorate the effectiveness of collaborative debugging processes, and at evaluating the usefulness of our CDB collaborative debugging approach. The study suggests that CDB's collaboration features are often perceived as important for effective debugging, and can improve the overall debugging experience in collaborative settings.

Experience with lightweight formal methods suggests that programmers are willing to write specification if it brings tangible benefits to their usual development activities. This paper considers stronger specifications and studies whether they can be deployed as an incremental practice that brings additional benefits without being unacceptably expensive. We introduce a methodology that extends Design by Contract to write strong specifications of functional properties in the form of preconditions, postconditions, and invariants. The methodology aims at being palatable to developers who are not fluent in formal techniques but are comfortable with writing simple specifications. We evaluate the cost and the benefits of using strong specifications by applying the methodology to testing data structure implementations written in Eiffel and C#. In our extensive experiments, testing against strong specifications detects twice as many bugs as standard contracts, with a reasonable overhead in terms of annotation burden and run-time performance while testing. In the wide spectrum of formal techniques for software quality, testing against strong specifications lies in a “sweet spot” with a favorable benefit to effort ratio.

This panel will discuss what characterizes the publication process in the software engineering community and debate how it serves the needs of the community, whether it is fair - e.g. valuable work gets published and mediocre work rejected - and highlight the obstacles for young scientists. The panel will conclude with a discussion on suggested next steps.

This paper presents a case study on the impact of development processes on the success of globally distributed software projects. The study compares agile (Scrum, XP, etc.) vs. structured (RUP, waterfall) processes to determine if the choice of process impacts: the overall success and economic savings of distributed projects; the importance customers attribute to projects; the motivation of the development teams; and the amount of real-time or asynchronous communication required during project development. The case study includes data from 66 projects developed in Europe, Asia, and the Americas. The results show no significant difference between the outcome of projects following agile processes and structured processes, suggesting that agile and structured processes can be equally effective for globally distributed development. The paper also discusses several qualitative aspects of distributed software development such as the advantages of near shore vs. offshore, the preferred communication patterns, and some common critical aspects.

A model has variability bounded by v/k when the state changes at most v times over any linear interval containing k time instants. When interpreted over models with bounded variability, specification formulae that contain redundant metric information -- through the usage of next operators -- can be simplified without affecting their validity. This paper shows how to harness this simplification in practice: we present a translation of LTL into Büchi automata that removes redundant metric information, hence makes for more efficient verification over models with bounded variability. To show the feasibility of the approach, we also implement a proof-of-concept translation in ProMeLa and verify it using the Spin off-the-shelf model-checker.

Considerable progress has been made towards automatic support for one of the principal techniques available to enhance program reliability: equipping programs with extensive contracts. The results of current contract inference tools are still often unsatisfactory in practice, especially for programmers who already apply some kind of basic Design by Contract discipline, since the inferred contracts tend to be simple assertions - the very ones that programmers find easy to write. We present new, completely automatic inference techniques and a supporting tool, which take advantage of the presence of simple programmer-written contracts in the code to infer sophisticated assertions, involving for example implication and universal quantification.

Initial research in automated program fixing has generally limited itself to specific areas, such as data structure classes with carefully designed interfaces, and relied on simple approaches. To provide high-quality fix suggestions in a broad area of applicability, the present work relies on the presence of contracts in the code, and on the availability of static and dynamic analyses to gather evidence on the values taken by expressions derived from the code. The ideas have been built into the AutoFix-E2 automatic fix generator. Applications of AutoFix-E2 to general-purpose software, such as a library to manipulate documents, show that the approach provides an improvement over previous techniques, in particular purely model-based approaches.

Automated random testing has shown to be an effective approach to finding faults but still faces a major unsolved issue: how to generate test inputs diverse enough to find many faults and find them quickly. Stateful testing, the automated testing technique introduced in this article, generates new test cases that improve an existing test suite. The generated test cases are designed to violate the dynamically inferred contracts (invariants) characterizing the existing test suite. As a consequence, they are in a good position to detect new faults, and also to improve the accuracy of the inferred contracts by discovering those that are unsound. Experiments on 13 data structure classes totalling over 28,000 lines of code demonstrate the effectiveness of stateful testing in improving over the results of long sessions of random testing: stateful testing found 68.4% new faults and improved the accuracy of automatically inferred contracts to over 99%, with just a 7% time overhead.

Metric LTL formulas rely on the next operator to encode time distances, whereas qualitative LTL formulas use only the until operator. This paper shows how to transform any metric LTL formula M into a qualitative formula Q, such that Q is satisfiable if and only if M is satisfiable over words with variability bounded with respect to the largest distances used in M (i.e., occurrences of next), but the size of Q is independent of such distances. Besides the theoretical interest, this result can help simplify the verification of systems with time-granularity heterogeneity, where large distances are required to express the coarse-grain dynamics in terms of fine-grain time units.

When dependability of systems with a large number of components is a concern, being able to model and analyze their properties, especially non-functional ones, in a formal and automated way becomes essential. Often, however, the application of formal methods and automated reasoning is seen by practitioners as complex and time consuming. Compositional techniques can help modify this belief. In this paper we show how a compositional modeling and verification technique can be applied to the analysis of distributed systems with numerous interacting nodes. We automate the proof by exploiting a SAT-based tool. We demonstrate the validity of the resulting approach by applying it to an autonomic service-based system that manages, in a coordinated peer-to-peer manner, electricity consumption in a geographical area. In particular, we show that in this case the time needed for performing the proof is remarkably shorter than in the case in which we adopt a non-compositional approach.

This paper presents a novel approach to the design of self-adaptive service-oriented applications based on a new model called service tiles. The approach allows designers to develop a service-oriented system by building an assembly of component services that accomplishes the given goal. The assembly is computed automatically starting from the specification of a subset of the whole system, a few constraints, and the goals the application should fulfill. An application designed according to the service-tile model can also dynamically self-adapt by replacing, in part or entirely, services in the assembly whenever they fail or the application context changes. The service-tile design technique has been implemented in a prototype and some experiments with several examples demonstrate the feasibility of the approach and its practical efficiency.

In program debugging, finding a failing run is only the first step; what about correcting the fault? Can we automate the second task as well as the first? The AutoFix-E tool automatically generates and validates fixes for software faults. The key insights behind AutoFix-E are to rely on contracts present in the software to ensure that the proposed fixes are semantically sound, and on state diagrams using an abstract notion of state based on the boolean queries of a class. Out of 42 faults found by an automatic testing tool in two widely used Eiffel libraries, AutoFix-E proposes successful fixes for 16 faults. Submitting some of these faults to experts shows that several of the proposed fixes are identical or close to fixes proposed by humans.

This article revisits the classical notion of sampling in the setting of real-time temporal logics for the modeling and analysis of systems. The relationship between the satisfiability of metric temporal logic (MTL) formulas over continuous-time models and over discrete-time models is studied. It is shown to what extent discrete-time sequences obtained by sampling continuous-time signals capture the semantics of MTL formulas over the two time domains. The main results apply to “flat” formulas that do not nest temporal operators and can be applied to the problem of reducing the verification problem for MTL over continuous-time models to the same problem over discrete time, resulting in an automated partial practically efficient discretization technique.

A core problem in formal methods is the transition from informal requirements to formal specifications. Especially when specifying reactive systems, many formalisms require the user to either understand a complex mathematical theory and notation or to derive details not given in the requirements, such as the state space of the problem. While formalizing a real-world requirements document, we developed a technique where not states but signal patterns are the main elements. We argue that it supports a formalization that is often closer to the informal requirements and thus provides a smoother transition to formal methods. As only tables of regular expressions are used for notation, the technique can easily be understood by non-mathematicians. Many properties, such as consistency, can be checked automatically on these specifications. Besides the formal foundation of our approach, this paper presents prototypical tool support and first results from an industrial case study.

In this paper we argue that the modeling activity in the development of software-intensive systems should formalize as much as possible of the environment in which the application being developed operates. We also show that a rich formal model of the environment helps developers clearly state requirements that might typically be considered intrinsically informal (or non- formalizable in general). To illustrate this point, we show how a requirement for "orderly safe traffic" in a traffic system can be modeled, and we briefly discuss the benefits thereof.

The paper "An Interval Logic for Real-Time System Specification" (Mattolini and Nesi, IEEE Trans. Software Eng., vol. 27, no. 3, pp. 208-227, Mar. 2001) presents the TILCO specification language and compares it to other existing similar languages. In this comment, we show that several of the logic formulas used for the comparison are flawed and/or overly complicated and we explain why, in this respect, the comparison is moot