# Incremental Formula-Based Fix Localization
## 1 Introduction  
Debugging is an essential and yet the most expensive task in software development [1, 2]. It includes a labor-intensive process of locating and fixing faulty code in a buggy program. This process consumes about 50% of the total software development costs, of which the majority is spent on fault localization [1]. Automatic techniques that reduce manual effort in debugging can significantly impact software costs and productivity [3]. Many automatic techniques have been proposed for supporting developers in various debugging activities (e.g., Reference [4, 5, 6, 7]). Most fault localization approaches (e.g., spectrum-based or mutation-based methods [8, 9]) focus on computing a statistical measurement of suspicious to rank program statements by their likelihood of being faulty. However, to be useful, these methods require a test suite containing many passing and failing executions with high code coverage [10, 11]. Such a high-quality test suite is often not available in practice. Moreover, these methods provide a ranked list of suspicious statements solely without any explanation; thus, developers still need high inspection efforts to examine these statements for localizing and fixing faults [3]. Formula-based fault localization (FFL) is particularly a promising approach as it not only logically identifies possible fault locations but also provides additional information that helps to explain and fix the faults [5]. Consider a buggy program and a failing test case that, in its execution trace, called error trace, demonstrate an error. FFL techniques work by constructing an unsatisfiable logical formula called _error trace formula_, that is a symbolic representation of the error trace, and using an automatic solver to find the causesof this formula unsatisfiability. Based on the solution obtained from the solver, possible faulty statements in the program can be logically identified. Existing FFL techniques differ in how they construct the error trace formula and how they use the automatic solver to manipulate the formula for locating the fault. In Reference [12; 13; 14; 15], a static analysis technique was performed to construct a logical formula called _program-formula_ that semantically equal to the input program (with regard to a certain unwinding bound). Specifically, every satisfiable assignment to the program-formula corresponds to a feasible execution in the program, and vice versa every program execution (with regard to a certain bound) corresponds to a satisfiable assignment of the formula. This program-formula is then extended in conjunction with clauses encoding the input values and the assertions of a failing test case to form an unsatisfiable formula. They then feed the extended formula into a pMaxSAT solver, which finds an assignment to the formula's variables that maximize the number of satisfied clauses. The set of unsatisfied clauses, called a minimal correction subset (MCS) of the formula, indicates a corresponding minimal set of program statements that can be modified to correct the considered error execution. In addition, the obtained variable assignments correspond to a feasible correct execution in the angelically fixed program, which replaces all statements in the MCS with suitable angelic values. As a result, they can provide developers with potential minimal fix location, together with a successful angelic execution, as an explanation. A key limitation of these methods is that they are extremely computationally expensive and has scalability issue even with small programs. This is because they represent all possible execution paths in a program into a formula. It may easily lead to a very large and complex formula that cannot be handled or is difficult to handle by recent solvers. [PERSON] [16] proposed an on-demand formula computation (OFC) technique to construct a smaller formula that encodes only program parts relevant to a given test case.