CFaults: Model-Based Diagnosis for Fault Localization in C Programs with Multiple Test Cases
This work addresses the time-consuming and expensive task of debugging for software developers, offering an incremental improvement by ensuring consistency and minimal diagnoses in fault localization.
The paper tackles the problem of fault localization in C programs with multiple faults by introducing CFaults, a model-based diagnosis approach that aggregates failing test cases into a unified MaxSAT formula, resulting in faster performance and generation of only subset-minimal diagnoses compared to existing methods like BugAssist and SNIPER.
Debugging is one of the most time-consuming and expensive tasks in software development. Several formula-based fault localization (FBFL) methods have been proposed, but they fail to guarantee a set of diagnoses across all failing tests 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 with multiple faults. CFaults leverages Model-Based Diagnosis (MBD) with multiple observations and aggregates all failing test cases into a unified MaxSAT formula. Consequently, our method guarantees consistency across observations and simplifies the fault localization procedure. Experimental results on two benchmark sets of C programs, TCAS and C-Pack-IPAs, show that CFaults is faster than other FBFL approaches like BugAssist and SNIPER. Moreover, CFaults only generates subset-minimal diagnoses of faulty statements, whereas the other approaches tend to enumerate redundant diagnoses.