Patch overfitting is a well-known open challenge for automated program repair (APR), which results from having insufficient or incomplete specifications to validate the generated patches. We argue that part of the patch overfitting challenge is caused by not properly taking termination issues into account during patch validation. As such, our goal here is to improve APR process by proposing a new approach that is dedicated to more complete patch correctness validation for APR.

The paper is divided into two parts: In the first part, we study the correlation between the APR problem and the program termination problem, demonstrating how a variety of program defects (e.g., violation of liveness properties, which causes the program to run indefinitely, and memory safety properties, which lead the program to crash) can be handled by fixing the termination of the program. In the second part, we present a novel patch validation approach that extends the standard test-based validation strategy by verifying two additional oracles: (i) oracles for checking the absence of the erroneous behavior caused by the bug being fixed, and (ii) oracles for checking the successful or normal termination of the patched program. We demonstrate how to validate the two oracles using contemporary termination provers and program verifiers. We also demonstrate how to effectively use the new validation oracles while taking into account the type of bug being repaired and the structure of the defected program.