Test Overfitting in Automated Program Repair: Measurements and Approaches Using Formal Methods

Bugs exist in software systems; unfortunately, manually finding bugs and repairing them is complex, time-consuming, and expensive. Automated Program Repair (APR) techniques have promising results to make the debugging process automatic and dramatically decreasing the cost of developing a software system. Almost all developed APR tools use test suites to bug localization and evaluate generated candidate patches\u27 correctness; thus, it is named dynamic APR. Test overfitting is one of the main challenges of dynamic APR tools, which is evident from several recent studies. Test overfitting means the repaired program is not correct based on the program\u27s expected behavior while the repaired program can satisfy its input test suite. In other words, the patch is only good enough to pass the input test suite, but the generated patched program is not correct regarding the program\u27s actual requirements. My dissertation aims to provide fresh insight into the test overfitting problem by using formal methods as a patch correctness assessment, a counterexample generator, and its combination with fuzzers to make dynamic APR tools more reliable. Furthermore, a new dataset with 597 buggy programs has been created for this research that all programs are equipped with full formal behavioral specifications using Java Modeling Language that OpenJML\u27s static verification tool can detect all as buggy programs