# Incremental Formula-Based Fix Localization
## 6 Related Work
### Formula-Based Fault Localization  
[PERSON] [12; 22], [PERSON] [14; 33], and [PERSON] [13] construct a formula that semantically represents all possible executions in a buggy program (unwinding to a given bound) and extend this formula in conjunction with clauses encoding input and expected output of a failing test case to form an unsatisfiable error trace formula. [PERSON] [12; 22] and [PERSON] [14; 33] treat this error trace formula as an instance of a partial MaxSAT problem, in which the clauses encoding test input and expected output is marked \"hard-clause\", and the clauses encoding program statements are marked \"soft-clause\". They use a pMaxSAT solver to obtain the MCS and report the program statements that correspond to clauses in the MCS as possible faults. To reduce the formula solving time, [PERSON] et al. [15] determine correct basic blocks (CB), which are basic blocks that do not participate in any failing executions, and set all clauses related to statements in these CBs as hard-clause. Instead of using MaxSAT solver to obtain MCS directly, [PERSON] [13] derives the MCS by computing irreducible infeasible subsets (minimal hitting set) of the error trace formula. Our approach is similar to these MaxSAT-based approaches in finding minimal sets of program locations where an angelic fix may exist. However, our approach differs from these approaches in several aspects. First, while these approaches are based on a static error trace formula, which may lead to over-complex or insufficient for reasoning, our approach is based on a formula that is constructed dynamically on-demand in order to gain the trade-off between efficiency and complexity. Second, instead of using a MaxSAT solver, we adapt the core-guided maxsat algorithm to manipulate and solve the formula incrementally. [PERSON] [17], [PERSON] [18], [PERSON] [34], and [PERSON] [19] work on error trace formulas that represent a sequence of program statements in which execution produced an error; however, we referred as single-path formula. [PERSON] [17] and [PERSON] [34] leverage Craig Interpolation to find Error Invariants for every point in the error trace, where an error invariant for a position in a trace is a condition that the error will occur if the program is continued from that position. Based on Error Invariants, they can semantically remove all irrelevant statements from the error trace, thus resulting in a shorter error trace which is easier to localize bugs. Compared to our approach, both approaches can output a reduced error trace which contains error-relevant statements only (in our approach, the reduced error trace can be reconstructed by sort all statements in MCS by the executed order); in addition, our approach also provides a suggestion about how to fix these bugs. Moreover, while our approach uses incremental SMT solving, which is commonly supported by recent SMT solvers, these error invariant approaches require an interpolation solver, which is not popular. [PERSON] et al. [19] encode assignment statements on a given error path into an error trace formula. They used a MaxSAT solver to compute the MCS of this formula and reported the corresponding statements as possible faults. An attempt is made to divert at most k conditional branch decisions on the error path to find alternative corrected paths. For each corrected path found, diverted conditional branches and also the MCS of the trace formula constructed on the path that reached the first diverted condition are reported as possibly faulty. Similar to this approach, we also diverted the counterexample path to find corrected executions. However, there are several difference between our approach and that of [PERSON] et al. [19]. First, our approach finds corrected paths by diverting not only branch decisions but also assignment statements.