Paper Info
Title
Bug-Assist: assisting fault localization in ANSI-C programs
Abstract
Several verification tools exist for checking safety properties of programs and reporting errors. However, a large part of the program development cycle is spend in analyzing the error trace to isolate locations in the code that are potential causes of the bug. Currently, this is usually performed manually, by stepping through the error trace in a debugger. We describe Bug-Assist, a tool that assists programmers localize error causes to a few lines of code. Bug-Assist takes as input an ANSIC program annotated with assertions, performs bounded model checking to find potential assertion violations, and for each error trace returned by the model checker, returns a set of lines of code which can be changed to eliminate the error trace. Bug-Assist formulates error localization as a MAX-SAT problem and uses scalable MAX-SAT solvers. In experiments on a set of C benchmarks, Bug-Assist was able to reduce error traces to only a few lines of code. Bug-Assist is available as an Eclipse plug-in, enabling its easy deployment in the code development phase.
Year
DOI
Venue
2011
10.1007/978-3-642-22110-1_40
CAV
Keywords
Field
DocType
potential cause,max-sat problem,ansic program,code development phase,error localization,error trace,model checker,ansi-c program,potential assertion violation,bounded model checking,fault localization,programmers localize error
Programming language,Model checking,ANSI C,Debugger,Computer science,Assertion,Algorithm,Theoretical computer science,Software development process,True quantified Boolean formula,Source lines of code,Scalability
Conference
Volume
Citations 
PageRank 
6806
12
0.62
References 
Authors
10
4
Name
Order
Citations
PageRank
Manu Jose11194.08
Rupak Majumdar23401220.08
Ganesh Gopalakrishnan31619130.11
Shaz Qadeer43257239.11