James C. King
Abstract
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.
- 1 Boyer, R.S., Elspas, B., Levitt, K.N. SELECT-A formal system for testing and debugging programs by symbolic execution. 1975 Int. Conf. on Reliable Software, April 1975, pp. 234-245. Google Scholar
Digital Library
- 2 Clarke, L. A system to generate test data and symbolically execute programs. Rep. No. CU-CS-060-75, Dep. of Computer Sci., U. of Colorado, Feb. 1975.Google Scholar
- 3 Darlington, J. A semantic approach to automatic program improvement. Ph.D. Th., U. of Edinburgh, 1972.Google Scholar
- 4 Deutsch, L.P. An interactive program verifier. Ph.D. Th., Dep. of Computer Sci., U. of California, Berkeley, May 1973.Google Scholar
- 5 Elspas, B., et al. An assessment of techniques for proving program correctness. Computing Surveys 4, 2 (June 1972), 97-147. Google ScholarDigital Library
- 6 Floyd, R.W. Assigning meanings to programs, Proc. Symp. Appl. Math. Vol. 19, Amer. Math. Soc., Provincetown, R.I., 1967, pp. 19-32.Google ScholarCross Ref
- 7 King, J.C. Proving programs to be correct. IEEE Trans. on Comp. C-20, 11 (Nov. 1971), 1331-1336.Google ScholarDigital Library
- 8 King, J.C. A program verifier. Proc. IFIP Cong. 71, North- Holland, Amsterdam, 1971, pp. 235-249.Google Scholar
- 9 King, J.C. and Floyd, R.W. An interpretation oriented theorem prover over integers, J. Computer Syst. Sci. 6, 4(Aug. 1972), 305-323.Google ScholarDigital Library
- 10 King, J.C. A new approach to program testing. 1975 Int. Conf. on Reliable Software, April 1975, pp. 228-233. Google ScholarDigital Library
- 11 Krause, K.W., et al. Optimal software test planning through Automated network analysis. IEEE Symp. on Computer Software Reliability, April 1973, pp. 18-22.Google Scholar
- 12 Manna, Z. Mathematical Theory of Computation. McGraw- Hill, New York, 1974, Ch. 4. Google ScholarDigital Library
- 13 Paterson, M.S. Equivalence problems in a model of computation. Ph.D. Th., U. of Cambridge, England, Aug. 1967. Also published as A.I. Tech. Memo No. 1 (Memo No. 211), MIT, Nov. 1970.Google Scholar
- 14 Sites, R.L. Algol W Reference Manual. Rep. CS-230 (Clearinghouse No. PB 203601), Computer Sci. Dep., Stanford LI., Feb. 1972. Google ScholarDigital Library
- 15 Topor, R.W., and Burstall, R.M. Verification of programs by symbolic execution-progress report. Unpublished report, Dep. of Machine Intelligence, U. of Edinburgh, Scotland, Dec. 1972.Google Scholar
- 16 Urschler, G. Complete redundant expression elimination in flow diagrams. Rep. RC4965, IBM Research, Yorktown Heights, N.Y., Aug. 1974.Google Scholar
Index Terms
- Symbolic execution and program testing
Recommendations
Compiler testing via symbolic interpretation
ACM '76: Proceedings of the 1976 annual conferenceA method for compiler testing using symbolic interpretation is presented. This method is a cross between program proving and program testing. It is useful in demonstrating that programs are correctly translated from a high level language to a low level ...
Formal Program Verification Using Symbolic Execution
Symbolic execution provides a mechanism for formally proving programs correct. A notation is introduced which allows a concise presentation of rules of inference based on symbolic execution. Using this notation, rules of inference are developed to ...
A new approach to program testing
International Conference on Reliable SoftwareThe current approach for testing a program is, in principle, quite primitive. Some small sample of the data that a program is expected to handle is presented to the program. If the program produces correct results for the sample, it is assumed to be ...
Comments