On Program Synthesis and Program Verification

Citation

Manna, Z., & Waldinger, R. J. (1970). On program synthesis and program verification. STANFORD UNIV CA DEPT OF COMPUTER SCIENCE.

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.


Read more from SRI