Program reduction using symbolic execution

ABSTRACT

By "program reduction" we mean making a program simpler according to some measure. For the narrow purposes here, that measure is the number of statements in the program. We are interested in the case when an existing program, assumed to be correct, is too general, too big, for a given situations. A simpler program, consistent with the original, but operating over a smaller domain is desired. We found that a program verifier, based on the symbolic execution methodology, with some minor enhancements could handle this program reduction task. The technique is interesting because it is such a simple, but powerful, application of such a program prover.

REFERENCES

• 1: Allen, F. E.; Carter J. L.; Fabri, J.; Ferrante, J.; Harrison, W. H.; Loewner, P. G.; Trevillyan, L. H. The experimental compiling system. (To appear), IBM Journal of Research and Development, November 1980.
• 2: Cheatham, T. E., Jr.; Holloway, G. H.; and Townley, J. A. Symbolic Evaluation and the Analysis of Programs. IEEE Trans. on Software Eng., vol. 5, no. 4, July 1979, pp 402--417.
• 3: Sidney L. Hantler , James C. King, An Introduction to Proving the Correctness of Programs, ACM Computing Surveys (CSUR), v.8 n.3, p.331-353, Sept. 1976 [doi>10.1145/356674.356677]
• 4: Tamir, M. ADI: Automatic Derivation of Invariants. IEEE Trans. on Software Eng., vol. 6, no. 1, January 1980, pp 40--48.
• 5: Ben Wegbreit, The synthesis of loop predicates, Communications of the ACM, v.17 n.2, p.102-113, Feb. 1974 [doi>10.1145/360827.360850]