Symbolic execution and program testing
The work
| Authors | James C. King |
|---|---|
| Editors | |
| Type | article |
| Year | 1976 |
| Citekey | king1976symbolic |
Where it appeared
| Published in | Communications of the ACM |
|---|---|
| Publisher | Association for Computing Machinery (ACM) |
| Volume | 19 |
| Issue | 7 |
| Pages | 385--394 |
Identifiers
| DOI | 10.1145/360248.360252 |
|---|---|
| ISSN | 0001-0782 |
Access
| Landing page | https://doi.org/10.1145/360248.360252 |
|---|
From crossref.
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.
How it got here
| How it got here | agent via crossref |
|---|---|
| Added | 2026-10-26 05:42 UTC |
| Not denied by | a person 2026-10-29 17:12 UTC |
Filed under
Cite it as
@article{king1976symbolic,
title = {Symbolic execution and program testing},
author = {James C. King},
year = {1976},
journal = {Communications of the ACM},
publisher = {Association for Computing Machinery (ACM)},
volume = {19},
number = {7},
pages = {385--394},
issn = {0001-0782},
doi = {10.1145/360248.360252},
}
This record lives at https://refs.drheap.org/king1976symbolic/ and will keep doing so.