sion debugging methods of Banerjee
et al. 3 and Qi et al. 22 localized the error to within 10 lines of code in fewer
than 10 minutes.
Among the techniques covered
here, the regression-debugging
methods3, 22 have shown the greatest scalability, with the other techniques being employed on small-to-moderate-scale programs. Moreover,
the scalability of symbolic analysis-based debugging methods crucially
depends on the scalability of SMT
constraint solving. 8 Compared to statistical fault-localization techniques,
which are easily implemented, symbolic execution-based debugging
methods still involve more implementation effort, as well as greater
execution time overheads. While we
see much promise due to the growth
in SMT solver technology, as partly
evidenced by the scalability of the
more research is needed in symbolic
analysis and SMT constraint solving
to enhance the scalability and applicability of these methods.
Note for all of the presented debugging methods, professional
programmers need user studies to
measure programmer productivity
gain that might be realized through
these methods. Parnin and Orso21
highlighted the importance of user
studies in evaluating debugging
methods. The need for user studies
may be even more acute for methods
like BugAssist that provide an iterative exploration of the possible error
causes, instead of providing a final
set of diagnostic information capturing the lines likely to be the causes of
errors. Finally, for the interpolant-based debugging method, the issue
of choosing suitable interpolants
needs further study, a topic being investigated today (such as by Albarghouthi and McMillan2).
Other directions. Related to our
topic of using symbolic execution for
software debugging, we wish to say
symbolic execution can also be useful
for “bug reproduction,” as shown by
Jin and Orso. 11 The bug-reproduction
problem is different from both test
generation and test explanation. Here,
some hints may be reported about the
failing execution by on-the-field users
in the form of a crash report, and these
(Paris, France, Aug. 27–31). Springer, 2012.
10. GNU Core Utilities; http://www.gnu.org/software/
11. Jin, W. and Orso, A. BugRedux: Reproducing field
failures for in-house debugging. In Proceedings of the
34th International Conference on Software Engineering
(Zürich, Switzerland, June 2–9). IEEE, 2012.
12. Jones, J.A., Harrold, M.J., and Stasko, J. T.
Visualization of test information to assist fault
localization. In Proceedings of the 24th International
Conference on Software Engineering (Orlando, FL, May
19–25). ACM Press, New York, 2002.
13. Jose, M. and Majumdar, R. Cause clue clauses:
Error localization using maximum satisfiability. In
Proceedings of the 32nd International Conference on
Programming Language Design and Implementation
(San Jose, CA, June 4–8). ACM Press, New York, 2011,
14. King, J.C. Symbolic execution and program testing.
Commun. ACM 19, 7 (July 1976) 385–394.
15. Liblit, B., Naik, M., Zheng, A.X., Aiken, A., and Jordan,
M.I. Scalable statistical bug isolation. In Proceedings
of the ACM SIGPLAN Conference on Programming
Language Design and Implementation (Chicago, IL,
June 12–15). ACM Press, New York, 2005, 15–26.
16. McMillan, K. L. An interpolating theorem prover.
Theoretical Computer Science 345, 1 (Nov. 2005),
17. Mechtaev, S., Yi, J., and Roychoudhury, A. DirectFix:
Looking for simple program repairs. In Proceedings
of the 37th IEEE/ACM International Conference on
Software Engineering (Firenze, Italy, May 16–24).
IEEE, 2015, 448–458.
18. Mechtaev, S., Yi, J., and Roychoudhury, A. Angelix:
Scalable multiline program patch synthesis via
symbolic analysis. In Proceedings of the 38th
International Conference on Soft ware Engineering
(Austin, TX, May 14–22) ACM Press, New York, 2016.
19. Morgado, A., Heras, F., Liffiton, M., Planes, J., and
Marques-Silva, J. Iterative and core-guided MaxSAT
solving: A survey and assessment. Constraints 18, 4
20. Nguyen, H.D. T., Qi, D., Roychoudhury, A., and Chandra,
S. SemFix: Program repair via semantic analysis. In
Proceedings of the 35th International Conference on
Software Engineering (San Francisco, CA, May 18–26).
IEEE/ACM, 2013, 772–781.
21. Parnin, C. and Orso, A. Are automated debugging
techniques actually helping programmers? In
Proceedings of the 20th International Symposium on
Software Testing and Analysis (Toronto, ON, Canada,
July 17–21) ACM Press, New York, 2011, 199–209.
22. Qi, D., Roychoudhury, A., Liang, Z., and Vaswani,
K. DAR WIN: An approach for debugging evolving
programs. ACM Transactions on Software Engineering
and Methodology 21, 3 (2012).
23. Weiser, M. Program slicing. IEEE Transactions on
Software Engineering 10, 4 (1984), 352–357.
24. Zeller, A. Yesterday my program worked. Today it fails.
Why? In Proceedings of the Seventh Joint Meeting of
European Software Engineering Conference and ACM
SIGSOF T Symposium on Foundations of Software
Engineering, Lecture Notes in Computer Science
(Toulouse, France, Sept. 1999). Springer, 1999, 253–267.
25. Zeller, A. Why Programs Fail: A Guide to Systematic
Debugging. Elsevier, 2006.
Abhik Roychoudhury ( firstname.lastname@example.org) is a
professor of computer science in the School of Computing
at the National University of Singapore and an ACM
Distinguished Speaker and leads the TSUNAMI center, a
software-security research effort funded by the Singapore
National Research Foundation.
Satish Chandra ( email@example.com) leads the advanced
programming tools research team at Samsung Research
America, Mountain View, CA, and is an ACM Distinguished
© 2016 ACM 0001-0782/16/07 $15.00
hints can be combined through symbolic execution to construct a failing
Finally, the software-engineering community has shown much
interest in building semiautomat-ed methods for program repair. It
would be interesting to see how symbolic execution-based debugging
methods can help develop program-repair techniques. The research
community is already witnessing development of novel program-repair
methods based on symbolic execution and program synthesis. 17, 18, 20
We would like to acknowledge many
discussions with our co-authors in Banerjee et al., 3 Chandra et al., 5 and Qi et
al. 22 We also acknowledge discussions
with researchers in a Dagstuhl seminar on fault localization (February
2013) and a Dagstuhl seminar on symbolic execution and constraint solving
(October 2014). We further acknowledge a grant from the National Research Foundation, Prime Minister’s
Office, Singapore, under its National
Cybersecurity R&D Program (Award
No. NRF2014NCR-NCR001-21) and administered by the National Cybersecurity R&D Directorate.
1. Agrawal, H. and Horgan, J. Dynamic program slicing.
In Proceedings of the ACM SIGPLAN Conference on
Programming Language Design and Implementation
(White Plains, NY, June 20–22). ACM Press, New
2. Albarghouthi, A. and McMillan, K.L. Beautiful
interpolants. In Proceedings of the 25th International
Conference on Computer-Aided Verification, Lecture
Notes in Computer Science 8044 (Saint Petersburg,
Russia, July 13–19). Springer, 2013.
3. Banerjee, A., Roychoudhury, A., Harlie, J.A., and Liang,
Z. Golden implementation-driven software debugging.
In Proceedings of the 18th International Symposium
on Foundations of Software Engineering (Santa Fe, NM,
Nov. 7–11). ACM Press, New York, 2010, 177–186.
4. Cadar, C. and Sen, K. Symbolic execution for software
testing: Three decades later. Commun. ACM 56, 1
(Jan. 2013), 82–90.
5. Chandra, S., Torlak, E., Barman, S., and Bodik, R.
Angelic debugging. In Proceedings of the 33rd
International Conference on Software Engineering
(Honolulu, HI, May 21–28). ACM Press, New York,
6. Christ, J., Ermis, E., Schaff, M., and Wies, T. Flow
sensitive fault localization. In Proceedings of the
14th International Conference on Verification Model
Checking and Abstract Interpretation (Rome, Italy,
Jan. 20–22). Springer, 2013.
7. Cleve, H. and Zeller, A. Locating causes of program
failures. In Proceedings of the 27th International
Conference on Software Engineering (St. Louis, MO,
May 15–21). ACM Press, New York, 2005.
8. de Moura, L. and Björner, N. Satisfiability modulo
theories: Introduction and applications. Commun.
ACM 54, 9 (Sept. 2011), 69–77.
9. Ermis, E., Schaff, M., and Wies, T. Error invariants. In
Proceedings of the 18th International Symposium on
Formal Methods, Lecture Notes in Computer Science