Incremental formula-based fix localization

Automatically fixing bugs in software programs can significantly reduce the cost and improve the productivity of the software. Toward this goal, a critical and challenging problem is automatic fix localization, which identifies program locations where a bug fix can be synthesized. In this paper, we present AgxFaults, a technique that automatically identifies minimal subsets of program statements at which a suitable modification can remove the error. AgxFaults works based on dynamically encoding semantic of program parts that are relevant to an observed error into an unsatisfiable logical formula and then manipulating this formula in an increasingly on-demand manner. We perform various experiments on faulty versions of the traffic collision avoidance system (TCAS) program in the Siemens Suite, programs in Bekkouche’s benchmark, and server real bugs in the Defects4J benchmark. The experimental results show that AgxFaults outperforms single-path-formula approaches in terms of effectiveness in finding fix localization and fault localization. AgxFaults is better than program-formula-based approaches in terms of efficiency and scalability, while providing similar effectiveness. Specifically, the solving time of AgxFaults is 28% faster, and the running time is 45% faster, than the program-formula-based approach, while providing similar fault localization results.