Chidanand Apté, Fred Damerau, et al.
ACM Transactions on Information Systems (TOIS)
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. © 1976, ACM. All rights reserved.
Chidanand Apté, Fred Damerau, et al.
ACM Transactions on Information Systems (TOIS)
Liat Ein-Dor, Y. Goldschmidt, et al.
IBM J. Res. Dev
Maurice Hanan, Peter K. Wolff, et al.
DAC 1976
Qing Li, Zhigang Deng, et al.
IEEE T-MI