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

This is the implementation of CFaults: Model-Based Diagnosis for Fault Localization in C with Multiple Test Cases [1] accepted at Formal Methods (FM) 2024.

CFaults introduces a novel formula-based fault localization technique for C programs capable of addressing any number of faults. Leveraging Model-Based Diagnosis (MBD) with multiple observations, CFaults consolidates all failing test cases into a unified MaxSAT formula, ensuring consistency in the fault localization process. In our paper, we show that CFaults only generates minimal diagnoses of faulty statements, while other formula-based fault localization methods tend to produce redundant diagnoses.

REQUIREMENTS

All requirements are installed in the Docker image available on Zenodo. Nevertheless, the script config.sh executes the commands to install all requirements.

MOTIVATING EXAMPLE

To run the motivating example from our paper: (Each FBFL tool should take less than one minute to process the motivating example) NOTE: Do not use the "enum_all" flag. This computes all possible diagnoses, not only the minimal ones.

CFaults

./CFaults.sh -i examples/fm2024_example.c -o motivating_example_CFaults -nu 3 -e lab02/ex01 -v -hw

CFaults-Refined

./CFaults.sh -i examples/fm2024_example.c -o motivating_example_CFaults-Refined -nu 3 -e lab02/ex01 -ss -v -hw

BugAssist

./BugAssist.sh -i examples/fm2024_example.c -o motivating_example_BugAssist -nu 3 -e lab02/ex01 -v -hw

SNIPER

./SNIPER.sh -i examples/fm2024_example.c -o motivating_example_SNIPER -nu 3 -e lab02/ex01 -v -hw

FM 2024 Reproducibility Instructions

See the FM 2024 reproducibility instructions for the full list of experiments and step-by-step guidance to reproduce all results from our paper.

Maintenance, Support && Collaborations

CFaults is actively maintained and used in ongoing research. We continue to develop the tool and build upon it, and we are open to collaborations.

If you run into a problem, please open an issue on this repository and/or (optionally) email us so we do not miss it.

Citation

If you use CFaults in your research, please cite the following paper:

@inproceedings{DBLP:conf/fm/OrvalhoJM24,
  author       = {Pedro Orvalho and
                  Mikol{\'{a}}s Janota and
                  Vasco M. Manquinho},
  title        = {{CFaults: Model-Based Diagnosis for Fault Localization in {C} with
                  Multiple Test Cases}},
  booktitle    = {Formal Methods - 26th International Symposium, {FM} 2024},
  series       = {Lecture Notes in Computer Science},
  volume       = {14933},
  pages        = {463--481},
  publisher    = {Springer},
  year         = {2024},
  doi          = {10.1007/978-3-031-71162-6\_24},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

REFERENCES

[1] P. Orvalho, M. Janota, and V. Manquinho. CFaults: Model-Based Diagnosis for Fault Localization in C with Multiple Test Cases. The 26th International Symposium on Formal Methods, FM 2024. PDF.

VERSIONS

• v3 : FM2024-v3 — minor update. Added flags to toggle: (1) hierarchical weights (-hw) across all FBFL methods; and (2) maximum coverage (-mc), which maps each statement S to every other statement that would be executed if S is executed. Note: enabling -mc may compromise the minimality of the reported diagnoses. This flag is useful when evaluating localisation methods on finding the injected bugs in TCAS rather than on finding minimal bugs.
• v2 : FM2024-v2 - minor fix on localizing bugs on uninitialized global variables, and fixed CFaults' enum_all flag (legacy, this flag should not be used).
• v1 : FM2024.