Abstract
Debugging is one of the most time-consuming and expensive tasks in softwaredevelopment. Several formula-based fault localization (FBFL) methods have beenproposed, but they fail to guarantee a set of diagnoses across all failingtests or may produce redundant diagnoses that are not subset-minimal,particularly for programs with multiple faults. This paper introduces a novel fault localization approach for C programs withmultiple faults. CFaults leverages Model-Based Diagnosis (MBD) with multipleobservations and aggregates all failing test cases into a unified MaxSATformula. Consequently, our method guarantees consistency across observationsand simplifies the fault localization procedure. Experimental results on twobenchmark sets of C programs, TCAS and C-Pack-IPAs, show that CFaults is fasterthan other FBFL approaches like BugAssist and SNIPER. Moreover, CFaults onlygenerates subset-minimal diagnoses of faulty statements, whereas the otherapproaches tend to enumerate redundant diagnoses.