Executive Summary : | Fault localization is a crucial but laborious task in software development, often involving multiple faults. Developers typically start with one fault at a time and fix it, then test the program again to determine if the previous failure passes. This sequential debugging process is time-consuming and requires a set of test cases to identify each fault. However, the presence of multiple faults can hinder the effectiveness of fault localization techniques, as certain faults may mask others. This proposal aims to eliminate the need for test cases and repeated invocation of the fault localization method by proposing model-based fault localization methods that take the correct and faulty programs as inputs. This method would indicate the code segment responsible for fault in the faulty program with respect to the correct program for every fault without requiring user-specified assertions or test cases. The proposed method uses verification techniques to identify the region of fault using the correct and faulty programs as inputs. SMT solvers are used to identify the code segments responsible for faults. This method has potential applications in localizing faults in transformations applied by compilers, as optimizing compilers apply sequences of transformations on input programs to obtain semantically equivalent output programs. Integrating this method into the LLVM compiler tool chain can help identify buggy optimizing transformations and lines of code responsible for errors. The proposal also aims to characterize the transformation sequence responsible for error by analyzing the regions of faults identified by the fault localization method. |