Towards A Case-Optimal Symbolic Execution Algorithm for Analyzing Strong Properties of Object-Oriented Programs
Third IEEE International Conference on Software Engineering and Formal Methods (SEFM'05) (2007)
Sept. 10, 2007 to Sept. 14, 2007
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/SEFM.2007.43
Xianghua Deng , Kansas State University
Robby , Kansas State University
John Hatcliff , Kansas State University
Recent work has demonstrated that symbolic execution techniques can serve as a basis for formal analysis capable of automatically checking heap-manipulating software components against strong interface specifications. In this paper, we present an enhancement to existing symbolic execution algorithms for object-oriented programs that significantly improves upon the algorithms currently implemented in Bogor/Kiasan and JPF. To motivate and justify the new strategy for handling heap data in our enhanced approach, we present a significant empirical study of the performance of related algorithms and an interesting case counting analysis of the heap shapes that can appear in several widely used Java data structure packages.
X. Deng, J. Hatcliff and Robby, "Towards A Case-Optimal Symbolic Execution Algorithm for Analyzing Strong Properties of Object-Oriented Programs," 2007 IEEE International Conference on Software Engineering and Formal Methods(SEFM), London, 2007, pp. 273-282.