Abstract
In this talk, I present a formal definition of symbolic execution in
terms of a symbolic transition system. This formal definition allows
for a general definition of the correctness of a symbolic transition
system with respect to a transition system which models the execution
on concrete values. Further, it allows for a general definition of
completeness in terms of a simulation relation between a concrete and
symbolic transition system. I first discuss such a formal model for a
basic programming language with a statically fixed number of
programming variables, and then show how to extend this basic model of
symbolic execution to object-oriented languages which feature
dynamically allocated variables.