| 1. |
- Torkar, Richard, 1971, et al.
(författare)
-
A Method to Assess and Argue for Practical Significance in Software Engineering
- 2022
-
Ingår i: IEEE Transactions on Software Engineering. - : IEEE Computer Society. - 0098-5589 .- 1939-3520. ; 48:6, s. 2053-2065
-
Tidskriftsartikel (refereegranskat)abstract
- 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 (Afzal et 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.
|
|
| 2. |
- Aichernig, Bernhard Klaus, et al.
(författare)
-
Preface
- 2016
-
Ingår i: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). - Cham : Springer International Publishing. - 1611-3349 .- 0302-9743. ; 9762
-
Tidskriftsartikel (övrigt vetenskapligt/konstnärligt)
|
|
| 3. |
- Ameri, M., et al.
(författare)
-
Why Just Boogie? Translating Between Intermediate Verification Languages
- 2016
-
Ingår i: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). - Cham : Springer International Publishing. - 1611-3349 .- 0302-9743. - 9783319336930 ; 9681, s. 79-95
-
Konferensbidrag (refereegranskat)abstract
- The verification systems Boogie and Why3 use their respective intermediate languages to generate verification conditions from high-level programs. Since the two systems support different back-end provers (such as Z3 and Alt-Ergo) and are used to encode different high-level languages (such as C# and Java), being able to translate between their intermediate languages would provide a way to reuse one system's features to verify programs meant for the other. This paper describes a translation of Boogie into WhyML (Why3's intermediate language) that preserves semantics, verifiability, and program structure to a large degree. We implemented the translation as a tool and applied it to 194 Boogie-verified programs of various sources and sizes; Why3 verified 83% of the translated programs with the same outcome as Boogie. These results indicate that the translation is often effective and practically applicable.
|
|
| 4. |
- Chen, Liushan, et al.
(författare)
-
Contract-Based Program Repair without The Contracts: An Extended Study
- 2021
-
Ingår i: IEEE Transactions on Software Engineering. - 0098-5589 .- 1939-3520. ; 47:12, s. 2841-2857
-
Tidskriftsartikel (refereegranskat)abstract
- 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 on JAID, 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 on JAID with a comprehensive experimental evaluation involving 693 bugs in three different benchmark suites. The evaluation shows, among other things, that: 1) JAID is effective: it produced correct fixes for over 15% of all bugs, with a precision of nearly 60%; 2) JAID is reasonably efficient: on average, it took less than 30 minutes to output a correct fix; 3) JAID is 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) JAID is 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.
|
|
| 5. |
- Chen, L. S., et al.
(författare)
-
Contract-Based Program Repair without the Contracts
- 2017
-
Ingår i: Proceedings of the 2017 32nd IEEE/ACM International Conference on Automated Software Engineering. - 1527-1366. ; , s. 637-647
-
Konferensbidrag (refereegranskat)abstract
- 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.
|
|
| 6. |
- Chen, Yu-Ting, 1992, et al.
(författare)
-
Robustness Testing of Intermediate Verifiers
- 2018
-
Ingår i: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). - Cham : Springer International Publishing. - 1611-3349 .- 0302-9743. ; 11138 LNCS, s. 91-108
-
Konferensbidrag (refereegranskat)abstract
- Program verifiers are not exempt from the bugs that affectnearly every piece of software. In addition, they often exhibit brittle behavior: their performance changes considerably with details of how the input program is expressed—details that should be irrelevant, such as the order of independent declarations. Such a lack of robustness frustrates users who have to spend considerable time figuring out a tool’s idiosyncrasies before they can use it effectively. This paper introduces a technique to detect lack of robustness of program verifiers; the technique is lightweight and fully automated, as it is based on testing methods (such as mutation testing and metamorphic testing). The key idea is to generate many simple variants of a program that initially passes verification. All variants are, by construction, equivalent to the original program; thus, any variant that fails verification indicates lack of robustness in the verifier. We implemented our technique in a tool called μ gie, which operates on programs written in the popular Boogie language for verification—used as intermediate representation in numerous program verifiers. Experiments targeting 135 Boogie programs indicate that brittle behavior occurs fairly frequently (16 programs) and is not hard to trigger. Based on these results, the paper discusses the main sources of brittle behavior and suggests means of improving robustness.
|
|
| 7. |
- Furia, Carlo A, 1979, et al.
(författare)
-
Applying Bayesian Analysis Guidelines to Empirical Software Engineering Data: The Case of Programming Languages and Code Quality
- 2022
-
Ingår i: ACM Transactions on Software Engineering and Methodology. - : Association for Computing Machinery (ACM). - 1049-331X .- 1557-7392. ; 31:3
-
Tidskriftsartikel (refereegranskat)abstract
- 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.
|
|
| 8. |
- Furia, Carlo A, 1979, et al.
(författare)
-
AutoProof: auto-active functional verification of object-oriented programs
- 2017
-
Ingår i: International Journal on Software Tools for Technology Transfer. - : Springer Science and Business Media LLC. - 1433-2779 .- 1433-2787. ; 19:6, s. 697-716
-
Tidskriftsartikel (refereegranskat)abstract
- Auto-active verifiers provide a level of automation intermediate between fully automatic and interactive: users supply code with annotations as input while benefiting from a high level of automation in the back-end. This paper presents AutoProof, a state-of-the-art auto-active verifier for object-oriented sequential programs with complex functional specifications. AutoProof fully supports advanced object-oriented features and a powerful methodology for framing and class invariants, which make it applicable in practice to idiomatic object-oriented patterns. The paper focuses on describing AutoProof ’s interface, design, and implementation features, and demonstrates AutoProof ’s performance on a rich collection of benchmark problems. The results attest AutoProof ’s competitiveness among tools in its league on cutting-edge functional verification of object-oriented programs.
|
|
| 9. |
- Furia, Carlo A, 1979, et al.
(författare)
-
Bayesian Data Analysis in Empirical Software Engineering Research
- 2021
-
Ingår i: IEEE Transactions on Software Engineering. - 0098-5589 .- 1939-3520. ; 47:9, s. 1786-1810
-
Tidskriftsartikel (refereegranskat)abstract
- IEEE 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, respectively. 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.
|
|
| 10. |
- Furia, Carlo A, 1979, et al.
(författare)
-
Bounded variability of metric temporal logic
- 2017
-
Ingår i: Annals of Mathematics and Artificial Intelligence. - : Springer Science and Business Media LLC. - 1573-7470 .- 1012-2443. ; 80:3-4, s. 283-316
-
Tidskriftsartikel (refereegranskat)abstract
- Deciding validity of Metric Temporal Logic (MTL) formulas is generally very complex and even undecidable over dense time domains; bounded variability is one of the several restrictions that have been proposed to bring decidability back. A temporal model has bounded variability if no more than v events occur over any time interval of length V, for constant parameters v and V. Previous work has shown that MTL validity over models with bounded variability is less complex—and often decidable—than MTL validity over unconstrained models. This paper studies the related problem of deciding whether an MTL formula has intrinsic bounded variability, that is whether it is satisfied only by models with bounded variability. The results of the paper are mainly negative: over dense time domains, the problem is mostly undecidable (even if with an undecidability degree that is typically lower than deciding validity); over discrete time domains, it is decidable with the same complexity as deciding validity. As a partial complement to these negative results, the paper also identifies MTL fragments where deciding bounded variability is simpler than validity, which may provide for a reduction in complexity in some practical cases.
|
|
| 11. |
- Furia, Carlo A, 1979, et al.
(författare)
-
Towards causal analysis of empirical software engineering data: The impact of programming languages on coding competitions
- 2024
-
Ingår i: ACM Transactions on Software Engineering and Methodology. - 1049-331X .- 1557-7392. ; 33:1, s. 1-35
-
Tidskriftsartikel (refereegranskat)abstract
- 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 paper 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 program- ming 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.
|
|
| 12. |
- Furia, Carlo A, 1979
(författare)
-
What good is Bayesian data analysis for software engineering?
- 2017
-
Ingår i: 39th IEEE/ACM International Conference on Software Engineering Companion, ICSE-C 2017, Buenos Aires, Argentina, 20-28 May 2017. ; , s. 374-376
-
Konferensbidrag (refereegranskat)abstract
- This abstract outlines the problems with classical statistical hypothesis testing, and recommends using alternative techniques based on Bayesian statistics, which are largely immune to the shortcomings of statistical hypothesis testing, and support a robust induction process.
|
|
| 13. |
- Gomes, Francisco, 1987, et al.
(författare)
-
Evolution of statistical analysis in empirical software engineering research : Current state and steps forward
- 2019
-
Ingår i: Journal of Systems and Software. - : Elsevier Inc.. - 0164-1212 .- 1873-1228. ; 156, s. 246-267
-
Tidskriftsartikel (refereegranskat)abstract
- Software engineering research is evolving and papers are increasingly based on empirical data from a multitude of sources, using statistical tests to determine if and to what degree empirical evidence supports their hypotheses. To investigate the practices and trends of statistical analysis in empirical software engineering (ESE), this paper presents a review of a large pool of papers from top-ranked software engineering journals. First, we manually reviewed 161 papers and in the second phase of our method, we conducted a more extensive semi-automatic classification of papers spanning the years 2001–2015 and 5196 papers. Results from both review steps was used to: i) identify and analyse the predominant practices in ESE (e.g., using t-test or ANOVA), as well as relevant trends in usage of specific statistical methods (e.g., nonparametric tests and effect size measures) and, ii) develop a conceptual model for a statistical analysis workflow with suggestions on how to apply different statistical methods as well as guidelines to avoid pitfalls. Lastly, we confirm existing claims that current ESE practices lack a standard to report practical significance of results. We illustrate how practical significance can be discussed in terms of both the statistical analysis and in the practitioner's context. © 2019 Elsevier Inc.
|
|
| 14. |
- Polikarpova, Nadia, et al.
(författare)
-
A fully verified container library
- 2018
-
Ingår i: Formal Aspects of Computing. - : Association for Computing Machinery (ACM). - 0934-5043 .- 1433-299X. ; 30:5, s. 495-523
-
Tidskriftsartikel (refereegranskat)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).
|
|
| 15. |
- Torkar, Richard, 1971, et al.
(författare)
-
Bayesian Data Analysis for Software Engineering
- 2021
-
Ingår i: Proceedings - International Conference on Software Engineering. - 0270-5257. ; , s. 328-329
-
Konferensbidrag (refereegranskat)abstract
- Slowly but surely, statistical practices in the empirical sciences are undergoing a complete makeover. Researchers in empirical software engineering, where too statistics is an essential tool, must become familiar with these new practices to ensure rigor of their research methods and soundness of their research results.
|
|
| 16. |
- Yuting, Chen, 1992, et al.
(författare)
-
Triggerless happy: Intermediate verification with a first-order prover
- 2017
-
Ingår i: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). - Cham : Springer International Publishing. - 1611-3349 .- 0302-9743. ; 10510, s. 295-311
-
Konferensbidrag (refereegranskat)abstract
- SMT solvers have become de rigueur in deductive verification to automatically prove the validity of verification conditions. While these solvers provide an effective support for theories—such as arithmetic—that feature strongly in program verification, they tend to be more limited in dealing with first-order quantification, for which they have to rely on special annotations—known as triggers—to guide the instantiation of quantifiers. Writing effective triggers is necessary to achieve satisfactory performance with SMT solvers, but remains a tricky endeavor—beyond the purview of non-highly trained experts. In this paper, we experiment with the idea of using first-order provers instead of SMT solvers to prove the validity of verification conditions. First-order provers offer a native support for unrestricted quantification, but have been traditionally limited in theory reasoning. By leveraging some recent extensions to narrow this gap in the Vampire first-order prover, we describe a first-order encoding of verification conditions of programs written in the Boogie intermediate verification language. Experiments with a prototype implementation on a variety of Boogie programs suggest that first-order provers can help achieve more flexible and robust performance in program verification, while avoiding the pitfalls of having to manually guide instantiations by means of triggers.
|
|
