On Program Synthesis and Program Verification
by Manna, Zohar, and Waldinger, Richard J.
Technical Note 52
Institution: AI Center, SRI International
Address: 333 Ravenswood Ave, Menlo Park, CA 94025
Nov 1970.
Note: Paper presented at the 4th Hawaii International Conference on Systems Science, Honolulu, Hawaii, January 12-14, 1971. SRI Projects 8721 and 8550. The research reported herein was sponsored in part by the Air Force Systems Command, USAF, Department of Defense, through the Air Force Cambridge Research Laboratories, Office of Aerospace Research, under Contract F19628-70-C-0246, and by the National Aeronautics and Space Administration under Contract NASV-2086.
Certain similarities between program verification and program synthesis are pointed out. The analogy is illustrated using a "bubble-sort" program. Recent work has shown that automatic deductive methods may be applied to the problems of program verification and program synthesis. As it turns out, these techniques are closely related. We demonstrate this relation using a particular program.
 Adobe PDF |
 BibTeX |
 EndNote |
| Name | Title | ||
|---|---|---|---|
 |
Waldinger, Richard J | Principal Scientist |  |
