@TECHREPORT{AICPub1464:1970, AUTHOR={Manna, Zohar, and Waldinger, Richard J.}, TITLE={On Program Synthesis and Program Verification}, ADDRESS={333 Ravenswood Ave, Menlo Park, CA 94025}, INSTITUTION={AI Center, SRI International}, MONTH={Nov}, NUMBER={52}, YEAR={1970}, KEYWORDS={Program Synthesis, Deductive Methods}, ABSTRACT={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.}, 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. } }
