Formula-based software debugging

Abstract

Satisfiability modulo theory solvers can help automate the search for the root cause of observable software errors.

References

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 York, 1990.
2. Albarghouthi, A. and McMillan, K.L. Beautiful interpolants. In Proceedings of the 25^th 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 18^th 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 33^rd International Conference on Software Engineering (Honolulu, HI, May 21-28). ACM Press, New York, 2011, 121--130.
6. Christ, J., Ermis, E., Schaff, M., and Wies, T. Flow sensitive fault localization. In Proceedings of the 14^th 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 27^th 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 18^th International Symposium on Formal Methods, Lecture Notes in Computer Science (Paris, France, Aug. 27-31). Springer, 2012.
10. GNU Core Utilities; http://www.gnu.org/software/coreutils/coreutils.html
11. Jin, W. and Orso, A. BugRedux: Reproducing field failures for in-house debugging. In Proceedings of the 34^th 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 24^th 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 32^nd International Conference on Programming Language Design and Implementation (San Jose, CA, June 4-8). ACM Press, New York, 2011, 437--446.
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), 101--121.
17. Mechtaev, S., Yi, J., and Roychoudhury, A. DirectFix: Looking for simple program repairs. In Proceedings of the 37^th 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 38^th International Conference on Software 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 (2013), 478--534.
20. Nguyen, H.D.T., Qi, D., Roychoudhury, A., and Chandra, S. SemFix: Program repair via semantic analysis. In Proceedings of the 35^th 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 20^th 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. DARWIN: 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 SIGSOFT 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.

Index Terms

• Software and its engineering

  • Software creation and management

    • Software post-development issues