Sciweavers

Share
ENTCS
2007

Automated Fault Localization for C Programs

11 years 8 months ago
Automated Fault Localization for C Programs
If a program does not fulfill a given specification, a model checker delivers a counterexample, a run which demonstrates the wrong behavior. Even with a counterexample, locating the actual fault in the source code is often a difficult task for the verification engineer. We present an automatic approach for fault localization in C programs. The method is based on model checking and reports only components that can be changed such that the difference between actual and intended behavior of the example is removed. To identify these components, we use the bounded model checker CBMC on an instrumented version of the program. We present experimental data that supports the applicability of our approach.
Andreas Griesmayer, Stefan Staber, Roderick Bloem
Added 13 Dec 2010
Updated 13 Dec 2010
Type Journal
Year 2007
Where ENTCS
Authors Andreas Griesmayer, Stefan Staber, Roderick Bloem
Comments (0)
books