Combining Model Checking and Spectrum-Based Fault Localization with Multiple Counterexamples

In the realm of software debugging, fault localization is a critical and challenging task. Traditional methods, including spectrum-based techniques and model checking, have demonstrated varying degrees of success but are limited by their inherent constraints. In this paper, we present a novel advancement in fault localization accuracy by integrating spectrum-based techniques with model checking, leveraging multiple counterexamples. Our previous work introduced this combined approach using a single counterexample; however, in this study, we show that utilizing multiple counterexamples significantly enhances the accuracy of fault localization. Experimental evaluations on the TCAS benchmark from the Siemens test suite demonstrate an average improvement of 62.80% in fault localization accuracy compared to traditional spectrum-based techniques, with a 20.39% increase when using multiple counterexamples versus a single one. This advancement underscores the potential of leveraging multiple counterexamples to improve the precision of fault localization.