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.

CACM July, 1976

King, J. C.

symbolic execution, program testing, program debugging,
program proving, program verification, 
symbolic interpretation

4.13 5.21 5.24

CA760703 JB January 4, 1978  12:59 PM

2850	5	2850
2850	5	2850
2850	5	2850
3080	5	2850
210	6	2850
2850	6	2850