Browse Prior Art Database

Applications of Symbolic Execution to Program Testing Disclosure Number: IPCOM000131296D
Original Publication Date: 1978-Apr-01
Included in the Prior Art Database: 2005-Nov-10
Document File: 12 page(s) / 45K

Publishing Venue

Software Patent Institute

Related People

John A. Darringer: AUTHOR [+4]


IBM Thomas J. Watson Research Center

This text was extracted from a PDF file.
This is the abbreviated version, containing approximately 8% of the total text.

Page 1 of 12


This record contains textual material that is copyright ©; 1978 by the Institute of Electrical and Electronics Engineers, Inc. All rights reserved. Contact the IEEE Computer Society (714-821-8380) for copies of the complete work that was the source of this textual material and for all use beyond that as a record from the SPI Database.

Applications of Symbolic Execution to Program Testing

John A. Darringer

James C. King

IBM Thomas J. Watson Research Center

The advanced method of symbolic evaluation can be applied to program testing situations with results close to those of formal correctness proofs -- but without the high cost.

Symbolic execution provides a basis for a program analysis tool that allows one to choose intermediate points in a spectrum ranging between individual test runs and general correctness proofs. One can perform a single "symbolic execution" of a program that is equivalent to a large (possibly unbounded) number of normal test runs. Not only can test results be checked by careful manual inspection, but if a machine interpretable specification is supplied, the results can be checked automatically. Furthermore, by varying the amount of symbolic data and program specification introduced, one can move from a normal execution (no symbolic data) to a symbolic execution that provides a proof of correctness.

The particular contexts for performing the symbolic execution can also be varied -- to produce results useful for estimating the test coverage of a set of particular test cases, to devise specific test data to force the program to follow specific execution paths, and to systematically explore a set of interesting execution paths.

An experimental system for symbolic program execution called Effigy has been developed and described in previous papers.. 2 The next two sections review the particular terminology and notions of symbolic execution developed in the Effigy project. The remainder of the paper describes how symbolic execution can be used to solve a variety of program testing problems. Related work has been done by Boyer et al.,3 Clarke,4 and Howden.5 9 Similar work emphasizing program correctness proofs has been done by Topor and Burstall,73 Deutsch,9 Good,' and Boyer and Moore."

Symbolic execution

The notion of symbolically executing a program follows quite naturally from normal program execution. First assume that there is a given programming language (say, Algol-60) and the normal definition of program execution for that language. One can extend that definition to provide a symbolic execution in the same manner as one extends arithmetic over numbers to symbolic algebraic operations over symbols and numbers. The definition of the symbolic execution is such that trivial cases involving no symbols are equivalent to normal executions, and any information learned in a symbolic execution applies to the corresponding normal ex...