On the Nature of Symbolic Execution

In the symbolic execution of a program real values are replaced by so-called symbolic values. Consequently, programming expressions cannot be evaluated, and thus the state, i.e., the assignment of values to program variables, in a symbolic execution is replaced by a substitution which assigns to each program variable an expression. The goal of symbolic execution is to generate a path condition that specifies concrete input values for which the actual execution of the program follows the same path (as generated by the symbolic execution). In the full version of this abstract we provide a formal definition of symbolic execution in terms of a symbolic transition system and prove its correctness with respect to an operational semantics which models the execution on concrete values. Our approach is modular, starting with a formal model for a basic programming language with a statically fixed number of programming variables. This model is extended to a programming language with recursive procedures which are called by a call-by-value parameter mechanism. Finally, we show how to extend this latter model of symbolic execution to arrays and object-oriented languages which feature dynamically allocated variables.