Symbolic execution
In computer science, symbolic execution (also symbolic evaluation) refers to the analysis of programs by tracking symbolic rather than actual values, a case of abstract interpretation. The field of symbolic simulation applies the same concept to hardware. Symbolic computation applies the concept to the analysis of mathematical expressions.
Symbolic execution is used to reason about all the inputs that take the same path through a program.
Contents |
[edit] Example
Consider the program below, which reads in a value and fails if the input is 6. If this program is symbolically executed, a special symbolic variable (as distinct from the program's variables) is associated with the values returned from the read function. These symbolic variables, and expressions of them are tracked in a special symbolic state. The symbolic variable, which we call s, is assigned to y in the symbolic state, later when y is multiplied by two, y is updated to contain the expression 2 * s.
At any control transfer instructions, such as the y ==12, a Path Constraint is updated to track which branch was taken. In this example assuming the condition is true, the Path Constraint is updated, from being empty, to contain: 2 * s ==12.
y = read() y = 2 * y if (y == 12) fails() print("OK")
By negating some of the conditions in the Path Constraint, and by using a constraint solver to obtain satisfying assignments to the modified Path Constraint it is possible to generate inputs that explore new parts of the program.
[edit] Testing
Symbolic execution is useful for software testing because it can analyse if and when errors in the code may occur. It can be used to predict what code statements do to specified inputs and outputs. It is also important for considering path traversal.
[edit] Limitations
Symbolic execution is used to reason about a program path-by-path. This may be superior to reasoning about a program, like Dynamic program analysis does, input-by-input. But if few inputs take the same path through the program, there is no saving over testing each of the inputs separately.
Addressing the path explosion of symbolic execution is a research problem [1] .
[edit] History
The concept of symbolic execution was introduced academically with descriptions of: the Select system ,[2] the EFFIGY system ,[3] the DISSECT system [4] , and Clarke's system .[5] See a bibliography of more technical papers published on symbolic execution.
[edit] References
- ^ Trevor Hansen, Peter Schachte, Harald Sondergaard, State Joining and Splitting for the symbolic execution of binaries, RV09 [1]
- ^ Robert S. Boyer and Bernard Elspas and Karl N. Levitt SELECT--a formal system for testing and debugging programs by symbolic execution, Proceedings of the International Conference on Reliable Software, 1975,page 234--245, Los Angeles, California
- ^ James C. King,Symbolic execution and program testing, Communications of the ACM, volume 19, number 7, 1976, 385--394
- ^ William E. Howden, Experiments with a symbolic evaluation system, Proceedings, National Computer Conference, 1976.
- ^ Lori A. Clarke, A program testing system, ACM 76: Proceedings of the Annual Conference, 1976, pages 488-491, Houston, Texas, United States
