Satisfiability modulo theory solvers can
help automate the search for the root cause
of observable software errors.
BY ABHIK ROYCHOUDHURY AND SATISH CHANDRA
PROGRAMMING, THOUGH A creative activity, poses
strict demands on its human practitioners in terms
of precision, and even talented programmers make
mistakes. The effect of a mistake can manifest in
several ways—as a program crash, data corruption, or
unexpected output. Debugging is the task of locating the
root cause of an error from its observable manifestation.
It is a challenge because the manifestation of an error
might become observable in a program’s execution
much later than the point at which the error infected
the program state in the first place. Stories abound of
heroic efforts required to fix problems that cropped up
unexpectedly in software that was previously considered
to be working and dependable.
Given the importance of efficient debugging in overall
software productivity, computer-assisted techniques
for debugging are an active topic of
research. The premise of such tech-
niques is to employ plentiful com-
pute cycles to automatically narrow
the scope of where in the source code
the root cause is likely to be, thereby
reducing the amount of time a pro-
grammer must spend on debugging.
Such computer-assisted debugging
techniques, as discussed in this ar-
ticle, do not promise to pinpoint the
mistake in a program but only to nar-
row the scope of where the mistake
might lurk. Such techniques are also
sometimes called “fault localization”
in the software-engineering literature.
We now proceed to review the major advances in computer-assisted debugging and describe one of the major challenges in debugging—lack of
specifications capturing the intended
behavior of the program; that is, if the
intended behavior of the program is
not available, how can a debugging
method infer where the program went
“wrong”? We next present a motivating
example extracted from Address Resolution Protocol (ARP) implementation
from GNU Coreutils10 that serves as a
running example in the article.
We then discuss at a high level
how symbolic techniques can help in
this direction by extracting candidate
specifications. These techniques utilize some form of symbolic execution,
first introduced by King. 14 We later describe debugging techniques that use
some form of symbolic techniques to
recover specifications. Table 1 outlines
˽ The lack of explicit formal specifications
of correct program behavior has long held
back progress in automated debugging.
˽ To overcome this lack of formal
specifications, a debugging system can
use logical formula solving to attempt to
find the change in a program that would
make the failed test pass.
˽ Because the failure of a test in a program
can also be seen as an unsatisfiable
logical formula, debugging—the task
of explaining failures—can thus benefit
from advances in formula solving or