[Paper] Model-Based Diagnosis with Multiple Observations: A Unified Approach for C Software and Boolean Circuits

Source: arXiv - 2512.02898v1

Overview

Debugging C programs and digital circuits is notoriously costly, especially when multiple faults are involved. The paper presents CFaults, a new fault‑localisation tool that unifies all failing test cases into a single MaxSAT problem, guaranteeing consistent, subset‑minimal diagnoses for both C code and Boolean circuits.

Key Contributions

• Unified MaxSAT formulation for handling multiple observations (i.e., all failing tests) in one go.
• Model‑Based Diagnosis (MBD) engine that works seamlessly on both C software and Boolean circuit descriptions.
• Subset‑minimal diagnoses only – eliminates redundant fault candidates that plague prior FBFL tools.
• Empirical evaluation on three benchmark suites (TCAS, C‑Pack‑IPAs, ISCAS85) showing faster localisation for C programs and competitive performance on circuits.
• Open‑source implementation (CFaults) that can be integrated into existing verification pipelines.

Methodology

1. Program / Circuit Instrumentation – The source (C) or netlist (circuit) is translated into a propositional model where each statement or gate is represented by Boolean variables.
2. Observation Encoding – Every failing test case is expressed as a set of constraints that must be violated. Instead of solving each test separately, CFaults aggregates all constraints into a single MaxSAT formula.
3. Maximum Satisfiability (MaxSAT) Solving – The solver tries to satisfy as many constraints as possible while minimising the number of “faulty” variables set to true. The optimal solution corresponds to a minimal set of statements/gates whose alteration would make all tests pass.
4. Diagnosis Extraction – The resulting assignment is mapped back to the original source, yielding a subset‑minimal list of suspect statements (or gates).
5. Iterative Refinement (optional) – If the developer wants more candidates, CFaults can enumerate the next‑best solutions, each still guaranteed to be subset‑minimal.

The whole pipeline is automated, requiring only the program, its test suite, and a MaxSAT solver (e.g., Open-WBO).

Results & Findings

Key takeaways

• For software, CFaults consistently outperforms state‑of‑the‑art FBFL tools both in speed and in delivering clean, non‑redundant diagnoses.
• On hardware benchmarks, while not the fastest, CFaults remains competitive and still provides high‑quality, minimal diagnoses.
• The unified MaxSAT approach eliminates the need for per‑test solving, reducing overall runtime and simplifying the debugging workflow.

Practical Implications

• Faster bug triage: Developers can pinpoint the exact statements responsible for a suite of failing tests in a single run, cutting down the “search‑and‑replace” cycle.
• Cleaner output: Subset‑minimal diagnoses mean fewer false positives, reducing the cognitive load on engineers who otherwise have to sift through redundant candidates.
• Cross‑domain applicability: Teams working on embedded firmware (C) and hardware verification (Boolean circuits) can adopt the same toolchain, fostering consistency across software‑hardware co‑design projects.
• Integration potential: CFaults can be hooked into CI pipelines—run after each test failure, automatically generate a minimal fault report, and even feed the results into automated program repair tools.
• Scalability: By leveraging modern MaxSAT solvers, the approach scales to medium‑size code bases (hundreds of KLOC) and realistic circuit benchmarks, making it viable for industrial use.

Limitations & Future Work

• Circuit performance: On large Boolean circuit suites, CFaults is marginally slower than specialised hardware‑only tools like HSD; optimisation of the encoding could close this gap.
• Fault model: The current implementation assumes statement‑level faults; extending to finer‑grained (e.g., expression‑level) or higher‑level (e.g., API misuse) faults would broaden applicability.
• Solver dependence: Diagnosis quality and speed hinge on the underlying MaxSAT solver; exploring portfolio or hybrid solving strategies could improve robustness.
• User interaction: Presently, CFaults outputs a static list of suspects. Future work includes interactive debugging assistance (e.g., ranking suspects by execution frequency or integrating with IDEs).

Overall, CFaults marks a significant step toward unified, efficient fault localisation for both software and hardware, offering developers a practical tool that bridges the gap between academic diagnosis theory and real‑world debugging needs.

Authors

• Pedro Orvalho
• Marta Kwiatkowska
• Mikoláš Janota
• Vasco Manquinho

Paper Information

• arXiv ID: 2512.02898v1
• Categories: cs.SE, cs.AI, cs.LO, cs.SC
• Published: December 2, 2025
• PDF: Download PDF