| Abstract: | Automated program repair is still a highly challenging problem mainly due to the reliance of the current techniques on test cases to validate candidate patches. This leads to the increasing unreliability of the final patches since test cases are partial specifications of the software. In the present paper, an automated program repair method is proposed by integrating genetic programming (GP) and model checking (MC). Due to its capabilities to verify the finite state systems, MC is employed as an appropriate criterion for evolving programs to calculate the fitness in GP. The application of MC for the fitness evaluation, which is novel in the context of program repair, addresses an important gap in the current heuristic approaches to the program repair. Being focused on fault detection based on the desired aspects, it enables the programmers to detect faults according to the definition of properties. Creating a general method, this characteristic can be effectively customized for different domains of application and the corresponding faults. Apart from various types of faults, the proposed method is capable of handling concurrency bugs which are not the case in many general repair methods. To evaluate the proposed method, it was implemented as a tool, named JBF, to repair Java programs. To meet the objectives of the study, some experiments were conducted in which certain programs with known bugs were automatically repaired by the JBF tool. The obtained results are encouraging and remarkably promising. |
