Automated program repair (APR) tools generally use a test suite to localize bugs and validate patches. These patches may pass the test suite but still be incorrect, which is called overfitting. To better understand the relationship between code coverage and overfitting, we aim to quantify the reduction in overfitting achieved by having more tests to cover branches multiple times, once 100% branch coverage is reached. We also investigate whether having more such tests increases the chances that the generated patch is exact, meaning that the patched program is syntactically the same as the original, high quality correct code in our dataset. Our experiments used three different test suites, each covering all branches in the code: test suites that cover each branch at least 1, 3, or 5 times. We used seven well-known APR tools for Java on a dataset of buggy programs equipped with formal specifications. Using formal methods allows us to reliably and objectively check for overfitting. Our experimental results indicate that enlarging the test suite beyond 100% coverage of branches reduces overfitting. However, beyond a certain threshold, expanding the test suite to cover branches repeatedly does not reduce overfitting.

Testing to detect semantic bugs is essential, especially for critical systems. Coverage-guided fuzzing (CGF) and runtime assertion checking (RAC) are two well-known approaches for detecting semantic bugs. CGF aims to generate test inputs with high code coverage. However, while CGF tools can be equipped with sanitizers to detect a fixed set of semantic bugs, they can otherwise only detect bugs that lead to a crash. Thus, the first problem we address is how to help fuzzers detect previously unknown semantic bugs that do not lead to a crash. Moreover, a CGF tool may not necessarily cover all branches with valid inputs, although invalid inputs are useless for detecting semantic bugs. So, the second problem is how to guide a fuzzer to maximize coverage using only valid inputs. However, RAC monitors the expected behavior of a program dynamically and can only detect a semantic bug when a valid test input shows that the program does not satisfy its specification. Thus, the third problem is how to provide high-quality test inputs for a RAC that can trigger potential bugs. The combination of a CGF tool and RAC solves these problems and can cover branches with valid inputs and detect semantic bugs effectively. Our study uses RAC to guarantee that only valid inputs reach the program under test using the program’s specified preconditions, and it also uses RAC to detect semantic bugs using specified postconditions. A prototype tool was developed for this study, named JMLKelinci+. Our results show that combining a CGF tool with RAC will lead to executing the program under test only with valid inputs and that this technique can effectively detect semantic bugs. Also, this idea improves the feedback given to a CGF tool, enabling it to cover all branches faster in programs with non-trivial preconditions. 1

Formal methods are used for verifying software correctness and reliability, especially for safety- and security-critical systems. After changing or refactoring code, it is often necessary to repair a program’s correctness proof, which can be time-consuming. We describe the problem of automated reasoning repair, provide a public dataset, and suggest some solution directions.

Automated program repair (APR) techniques that use test suites for bug localization and assessing candidate patches have promising results. Studies have shown that generated patches by APR tools that pass its test suite do not always correctly implement the program's expected behavior, known as test overfitting. My research aims to provide fresh insight into the test overfitting problem by using formal methods.

Automated program repair (APR) techniques have shown a promising ability to generate patches that fix program bugs automatically. Typically such APR tools are dynamic in the sense that they find bugs by testing and they validate patches by running a program's test suite. Patches can also be validated manually. However, neither of these methods for validating patches can truly tell whether a patch is correct. Test suites are usually incomplete, and thus APR-generated patches may pass the tests but not be truly correct; in other words, the APR tools may be overfitting to the tests. The possibility of test overfitting leads to manual validation, which is costly, potentially biased, and can also be incomplete. Therefore, we must move past these methods to truly assess APR's overfitting problem.We aim to evaluate the test overfitting problem in dynamic APR tools using ground truth given by a set of programs equipped with formal behavioral specifications. Using these formal specifications and an automated verification tool, we found that there is definitely overfitting in the generated patches of seven well-studied APR tools, although many (about 59%) of the generated patches were indeed correct. Our study further points out two new problems that can affect APR tools: changes to the complexity of programs and numeric problems. An additional contribution is that we introduce the first publicly available data set of formally specified and verified Java programs, their test suites, and buggy variants, each of which has exactly one bug.

Dynamic automated program repair (APR) techniques, which use test suites for bug localization and evaluating candidate patches, have promising results. However, many studies show that machine-generated patches with dynamic APR tools are not always reliable. Recent studies show that enhancing test suites by adding tests will help dynamic APR tools generate more reliable patches. We evaluate the effectiveness of minimally enhancing test suites by adding counterexamples for repaired programs that suffer from test overfitting. We use formal methods as an independent standard for evaluating patches' correctness and for generating counterexamples. Techniques for evaluating patch correctness (both with human reviewers and formal methods) can create false negatives, meaning that the repaired program is correct but is deemed incorrect. A counterexample is a good way to check on reviewer decisions about correctness. Our study evaluated 256 repaired but not verified programs (from the buggy Java+JML dataset); the repairs were generated by seven state-of-the-art dynamic APR tools. Our results show that the counterexample generated by the OpenJML tool could correctly classify all these programs into the categories of “test overfitting” and “false negatives.” After adding tests based on the counterexamples to the test suites, we ran the APR tools on the original buggy programs again and found that: (1) the APR tools were able to generate about 27.3% more correct patches with the enhanced test suite, and (2) the enhanced test suite resulted in the APR tools generating about 83.6% fewer overfitted patches.