2850	 Symbolic Execution and Program Testing	 This paper describes the symbolic execution of programs. Instead of supplying the normal inputs to a program e.g. numbers one supplies symbols representing arbitrary values. The execution proceeds as in a normal execution except that values may be symbolic formulas over the input symbols. The difficult yet interesting issues arise during the symbolic execution of conditional branch type statements. A particular system called EFFIGY which provides symbolic execution for program testing and debugging is also described. It interpretively executes programs written in a simple PL I style programming language. It includes many standard debugging features the ability to manage and to prove things about symbolic expressions a simple program testing manager and a program verifier. A brief discussion of the relationship between symbolic execution and program proving is also included. symbolic execution program testing program debugging program proving program verification symbolic interpretation
