  Symbolic execution is at the core of many techniques for program analysis and
test generation. Traditional symbolic execution of programs with numeric inputs
enjoys the property of forking as many analysis traces as the number of
analyzed program paths, a property that in this paper we refer to as path
optimality. On the contrary, current approaches for symbolic execution of
heap-manipulating programs fail to satisfy this property, thereby incurring
heavy path explosion effects that crucially penalize the efficiency of the
analysis. This paper introduces POSE, path-optimal symbolic execution, a
symbolic execution algorithm that originally accomplishes path optimality
against heap-manipulating programs. We formalize the POSE algorithm for a tiny,
but representative object-oriented programming language, and implement the
formalization into a prototype symbolic executor to experiment the algorithm
against a benchmark of sample programs that take data structures as inputs. Our
experiments provide initial empirical evidence of the potential of POSE for
improving on the state of the art of symbolic execution of heap-manipulating
programs.
