Abstract
Among various automatic fault localization methods, two of them are specifically noticed, coverage-based and formula-based. While the coverage-based method relies on statistical measures, the formula-based approach is an algorithmic method being 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 improves the efficiency of computing the potential root causes by using the push & pop mechanism of the Yices solver. The technique is particularly useful for programs with multiple faults. We implemented the method in a tool, SNIPER, which was applied to the TCAS benchmark. All single and multiple faults were successfully identified and discriminated by using the original test cases of the TCAS.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Binkley, D., Gold, N., Harman, M.: An Empirical Study of Static Program Slice Size. ACM TOSEM 16(2), Article 8 (April 2007)
Christ, J., Ermis, E., Schäf, M., Wies, T.: Flow-Sensitive Fault Localization. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) VMCAI 2013. LNCS, vol. 7737, pp. 189–208. Springer, Heidelberg (2013)
Clarke, E., Kroning, D., Lerda, F.: A Tool for Checking ANSI-C Programs. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 168–176. Springer, Heidelberg (2004)
DiGiuseppe, N., Jones, J.A.: On the Influence of Multiple Faults on Coverage-based Fault Localization. In: Proc. ISSTA 2011, pp. 210–220 (2011)
Dutertre, B., de Moura, L.: The Yices SMT Solver, http://yices.csl.sri.com
Griesmayer, A., Staber, S., Bloem, R.: Fault Localization using a Model Checker. In: STVR, pp. 149–173 (2010)
Groce, A., Chaki, S., Kroening, D., Strichman, O.: Error Explanation with Distance Metrics. STTT 8(3), 229–247 (2006)
Jones, J.A., Harrold, M.J.: Empirical Evaluation of the Tarantula Automatic Fault-Localization Technique. In: Proc. ASE 2005, pp. 273–282 (2005)
Jose, M., Majumdar, R.: Cause Clue Clauses: Error Localization using Maximum Satisfiability. In: Proc. PLDI 2011, pp. 437–446 (2011)
Kusumoto, S., Nishimatsu, A., Nishie, K., Inoue, K.: Experimental Evaluation of Program Slicing for Fault Localization. Empirical Software Engineering 7(1), 49–76 (2002)
Lattner, C., Adve, V.: LLVM: A Compilation Framework for Lifelong Program Analysis & Transformation. In: Proc. CGO 2004, pp. 75–86 (2004)
Liffiton, M.H., Sakallah, K.A.: Algorithms for Computing Minimal Unsatisfiable Subsets of Constraints. Automated Reasoning 40(1), 1–33 (2008)
Merz, F., Falke, S., Sinz, C.: LLBMC: Bounded Model Checking of C and C++ Programs Using a Compiler IR. In: Joshi, R., Müller, P., Podelski, A. (eds.) VSTTE 2012. LNCS, vol. 7152, pp. 146–161. Springer, Heidelberg (2012)
Morgado, A., Liffiton, M., Marques-Silva, J.: MaxSAT-Based MCS Enumeration. In: Biere, A., Nahir, A., Vos, T. (eds.) HVC. LNCS, vol. 7857, pp. 86–101. Springer, Heidelberg (2013)
Prasad, M.R., Biere, A., Gupta, A.: A Survey of Recent Advances in SAT-Based Formal Verification. STTT 7(2), 156–173 (2005)
Reiter, R.: A Theory of Diagnosis from First Principles. Artificial Intelligence 32(1), 57–95 (1987)
Safarpour, S., Mangassarian, H., Veneris, A., Liffiton, M.H., Sakallah, K.A.: Improved Design Debugging using Maximum Satisfiability. In: Proc. FMCAD 2007, pp. 13–19 (2007)
Weiser, M.: Programmers Use Slices When Debugging. Comm. ACM 25(7), 446–452 (1982)
Wotawa, F.: On the Relationship between Model-based Debugging and Program Slicing. Artificial Intelligence 135(1), 125–143 (2002)
Wotawa, F., Nica, M., Moraru, I.: Automated Debugging based on a Constraint Model of the Program and a Test Case. Logic and Algebraic Programming 81(4), 390–407 (2012)
Zeller, A., Hildebrandt, R.: Simplifying and Isolating Failure-Inducing Input. IEEE Trans. Softw. Eng. 28(2), 183–200 (2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Lamraoui, SM., Nakajima, S. (2014). A Formula-Based Approach for Automatic Fault Localization of Imperative Programs. In: Merz, S., Pang, J. (eds) Formal Methods and Software Engineering. ICFEM 2014. Lecture Notes in Computer Science, vol 8829. Springer, Cham. https://doi.org/10.1007/978-3-319-11737-9_17
Download citation
DOI: https://doi.org/10.1007/978-3-319-11737-9_17
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-11736-2
Online ISBN: 978-3-319-11737-9
eBook Packages: Computer ScienceComputer Science (R0)