# Incremental Formula-Based Fix Localization
## 4 Evaluation Setup
### Benchmarks  
For our evaluation, we use several buggy programs selected from three different benchmarks. The first benchmark consist of a set of example programs provided by [PERSON] [28]. The size of these program ranges from 17 to 130 lines of code. Each program contains one to three faults that were specifically injected to evaluate fault localization techniques. The second benchmark contains 41 faulty versions of a real traffic collision avoidance system (TCAS) from Siemens [29], which is popularly used in software testing and fault localization researches. The third benchmark we selected is real-world buggy programs in the Defects4][30]. We selected the programs in the first and second benchmark for two main reasons. First, these programs are small, so they allow us to find all minimal angelic fix candidates for the programs. This is generally impossible for large and more complex programs. By finding all minimal angelic fix candidates for the programs, we can precisely compare the efficiency of the techniques in term of complexity reduction and compare the effectiveness of the techniques in terms of success rates. Second, the TCAS programs are commonly used to evaluate state-of-the-art formula-based fault localization techniques, includingBugAssist, Sniper, and LocFaults. Thus, we can directly compare our results with those techniques since the program in the first and the second benchmarks are small size and contains only artificial faults. The third benchmark contains non-trivial open-source programs with real bugs. We obtained Java versions of the TCAS programs from the SIR website. Each faulty version of the TCAS program has a size of 180 lines and contains one to three artificially-injected faults. These programs also come with a total of 1576 test inputs and a fault-free version. For each buggy version, we manually compare it with the fault-free version and consider the set of different statements to be the actual faulty statements. To obtain failing test cases for each buggy version, we ran all test cases using the fault-free version to obtain the expected output of the test cases. Then, for each buggy version, we ran all the test cases and matched the results with the expected output to identify the failing test cases. The third benchmark we considered is several faulty programs in the Defects4J, a benchmark containing real bugs from large and complex open-source projects. We randomly select several buggy versions of open-source projects in the Defects4J. These programs include JFreeChart, Commons-Codec, Commons-Compress, Common-CSV, Common-Lang, Common-Math, and Mockito. In this experiment, we use the failing test cases that are already provided in the Defects4J as the input for the AgxFaults tool. Study Protocol  
We ran each of four techniques methods implemented in our tool on a buggy program multiple times, each time inputting a different failing test case and outputting a list of minimal angelic fix candidates (MFCs). We examined all MFCs produced for each run, in the generated order, and determined the validity and accuracy of the results. Specifically, a run was considered _successful fault localization_ if its output contained a correct fault location MFC, i.e., all suspicious statements in the MFC were actually faulty statements. A run was considered _successful fix localization_ if its output contained an correct fix location MFC, i.e., an MFC that is both a feasible fix candidate and performs fix at the correct fault location. To evaluate the performance of the techniques, we record the average CPU time of each technique for processing each failing test case and the amount of which consumed by the solvers, the number of MFC each technique generated and the number of which are feasible fix candidates, the number of code lines included in the report, whether the generated report contained the actual fault, and how many lines of code developer will have to examine to identify the actual fault location.