Title: Towards A Case-Optimal Symbolic Execution Algorithm for Analyzing
       Strong Properties of Object-Oriented Programs

Authors: Xianghua Deng and  Robby and John Hatcliff

Recent work has demonstrated that symbolic execution 
techniques can serve as a basis for formal analysis capa- 
ble of automatically checking heap-manipulating software 
components against strong interface specifications. In this 
paper, we present an enhancement to existing symbolic exe- 
cution algorithms for object-oriented programs that signifi- 
cantly 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 anal- 
ysis of the heap shapes that can appear in several widely 
used Java data structure packages.