2026-03-06T00:00:51Z https://ipsj.ixsq.nii.ac.jp/oai

oai:ipsj.ixsq.nii.ac.jp:00147454 2025-01-20T06:54:42Z 581:8417:8418

A Formula-based Approach for Automatic Fault Localization of Multi-fault Programs A Formula-based Approach for Automatic Fault Localization of Multi-fault Programs Si-Mohamed, Lamraoui Shin, Nakajima Si-Mohamed, Lamraoui Shin, Nakajima [一般論文] model-based diagnosis theory, multiple faults, partial maximum satisfiability, LLVM, Yices Formula-based fault localization approach is an algorithmic method that is able to provide fine-grained information account for identified root causes. The method combines the SAT-based formal verification techniques with the Reiter's model-based diagnosis theory. This paper adapts the formula-based fault localization method, and introduces a new program encoding, called full flow-sensitive trace formula. This encoding is particularly useful for programs with multiple faults. Furthermore, we improve the efficiency of computing the potential root causes by using the push & pop mechanism of the Yices solver. We implemented the method in a tool, SNIPER, which was applied to some benchmarks. All single and multiple faults were successfully identified and discriminated. \n------------------------------ This is a preprint of an article intended for publication Journal of Information Processing(JIP). This preprint should not be cited. This article should be cited as: Journal of Information Processing Vol.24(2016) No.1 (online) DOI　http://dx.doi.org/10.2197/ipsjjip.24.88 ------------------------------ Formula-based fault localization approach is an algorithmic method that is able to provide fine-grained information account for identified root causes. The method combines the SAT-based formal verification techniques with the Reiter's model-based diagnosis theory. This paper adapts the formula-based fault localization method, and introduces a new program encoding, called full flow-sensitive trace formula. This encoding is particularly useful for programs with multiple faults. Furthermore, we improve the efficiency of computing the potential root causes by using the push & pop mechanism of the Yices solver. We implemented the method in a tool, SNIPER, which was applied to some benchmarks. All single and multiple faults were successfully identified and discriminated. \n------------------------------ This is a preprint of an article intended for publication Journal of Information Processing(JIP). This preprint should not be cited. This article should be cited as: Journal of Information Processing Vol.24(2016) No.1 (online) DOI　http://dx.doi.org/10.2197/ipsjjip.24.88 ------------------------------ journal article 2016-01-15 application/pdf 情報処理学会論文誌 1 57 1882-7764 AN00116647 https://ipsj.ixsq.nii.ac.jp/record/147454/files/IPSJ-JNL5701039.pdf eng