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.

翻译：调试是软件开发中最耗时且成本最高的任务之一。已有多种基于公式的故障定位方法被提出，但这些方法无法保证在所有失败测试中生成一致的诊断集合，或可能产生非子集最小化的冗余诊断，尤其对于存在多故障的程序。本文针对含多故障的C程序提出一种新颖的故障定位方法。CFaults采用基于模型诊断框架整合多观测数据，将所有失败测试用例聚合为统一的MaxSAT公式。该方法确保了跨观测结果的一致性，并简化了故障定位流程。在TCAS和C-Pack-IPAs两个C程序基准集上的实验表明，CFaults相较于BugAssist、SNIPER等其他基于公式的故障定位方法具有更快的执行速度。此外，CFaults仅生成故障语句的子集最小化诊断，而其他方法往往枚举出冗余诊断。