CFaults: Model-Based Diagnosis for Fault Localization in C Programs with Multiple Test Cases

TL;DR

CFaults is a novel model-based diagnosis approach for fault localization in C programs with multiple faults, ensuring minimal diagnoses and improved efficiency over existing formula-based methods.

Contribution

Introduces CFaults, a model-based diagnosis method that guarantees subset-minimal fault diagnoses across multiple test cases in C programs.

Findings

CFaults is faster than BugAssist and SNIPER.

It guarantees subset-minimal diagnoses.

Performs well on benchmark C programs.

Abstract

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.