A Formula-Based Approach for Automatic Fault Localization of Imperative Programs

摘要

Among various automatic fault localization methods, two of them are specifically noticed, coverage-based and formula-based. While the coverage-based method relies on statistical measures, the formula-based approach is an algorithmic method being able to provide finegrained information account for identified root causes. The method combines the SAT-based formal verification techniques with the Reiter's model-based diagnosis theory. This paper adapts the formula-based fault localization method, and improves the efficiency of computing the potential root causes by using the push & pop mechanism of the Yices solver. The technique is particularly useful for programs with multiple faults. We implemented the method in a tool, SNIPER, which was applied to the TCAS benchmark. All single and multiple faults were successfully identified and discriminated by using the original test cases of the TCAS.