# Incremental Formula-Based Fix Localization
## 1 Introduction
Their experimental evaluation showed that OFC formulas are much simpler than program-formulas but still sufficient to produce the same result as the program-formulas. This method, however, requires to compute all MCS for multiple intermediate formulas before obtaining the final formula. Enumerating all MCS of many formulas might outweigh the benefits of generating a simpler formula. In [PERSON] [17; 18; 19]'s approaches, they work with a formula encoding the semantics of a single execution path, we refer to this formula as _single-path_ trace formula. A single-path trace formula is semantically equal to a straight-line program that contains program statements in which execution produced an error, although these single-path trace formulas are simple and, thus, easy to solve. However, because the formula does not contain information related to the control dependence among statements in the original program, the MCS obtained from these formulas may not correctly correspond to an angelic fix in the original program. As a result, these methods may fail to identify some angelic fix location, and they may also report invalid angelic fix candidates. In this paper, we present AgxFaults, an incremental formula-based fault localization method to overcome the above limitations. Our method is based on two main components. First, instead of based on a static formula that encodes the entire program (like program-formula) or just encodes a single execution path (like single-path formula), AgxFaults is based on an error formula that is constructed and extended dynamically and effectively in an on-demand manner. This formula, called angelic error trace formula, encodes only program parts that relevant to a specific failing test case, and it over-abstracts all unrelated program parts by angelic non-deterministic executions. This encoding results in compact error trace formulas that are easier to solve but that are still sufficient to identify both data and control-related faults. Second, because the angelic formula is incremented dynamically, instead of multiple calls to a MaxSMT solver to solve multiple formulas separately (like OFC approach), we adapt the incremental core-guide MaxSMT algorithm [20] to manipulate the formula and compute the MCS incrementally. We implemented our method in a tool named AgxFaults by extending the Java Path Finder (a NASA model checking tool) for localizing faults in Java programs. The input of AgxFaults is a buggy program and failing test cases (can be given as a jUnit test case, or a pair of input and expected post-condition in a configuration file). AgxFaults outputs a set of minimal angelic fix candidates (MFC), and each MFC is a pair consisting of a minimal fix location set and an angelic execution path to show that modifying these statements can make the given failing test case pass. We evaluated our methods using various programs of different kinds and sizes. These programs include several sample programs provided by Bekkouche [19], 41 faulty versions of a commercial traffic collision avoidance system (TCAS), and several large and complex real-world programs in the Defects4J benchmarks. The experimental results showed that AgxFaults succeeded in reporting actual fault localization for all bugs in both the Bekkouche and the TCAS benchmarks. AgxFaults outperformed single-path formula approaches both in terms of the success rate and the accuracy of fault localization. AgxFaults provided similar results compared to the program-formula approach with better efficiency and scalability. Specifically, AgxFaults has a 28% faster formula solving time and 45% faster running time than the program-formula approach when applied to the TCAS programs. Furthermore, when the complexity of the program increased (e.g., loop unwinding bound increased), the formula solving time of the program-formula-based method increased exponentially, while that of AgxFaults increased significantly slower.