On Program Synthesis and Program Verification

Abstract

Certain similarities between program verification and program synthesis are pointed out. The analogy is illustrated using a "bubble-sort" program. Recent work has shewn that automatic deductive methods may be applied to the problems of program verification [1] and program synthesis [2]. As it turns out, these techniques are closely related. We demonstrate this relation using a particular program.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Nov 01, 1970
Accession Number
ADA638145

Entities

People

  • Richard J. Waldinger
  • Zohar Manna

Organizations

  • Stanford University

Tags

Communities of Interest

  • Space

DTIC Thesaurus Topics

  • Abstracts
  • Air Force
  • Artificial Intelligence
  • Computer Science
  • Computers
  • Contracts
  • Department Of Defense
  • Information Operations
  • Numbers
  • Real Numbers
  • Sequences
  • Systems Science
  • Universities
  • Verification

Fields of Study

  • Computer science

Readers

  • Computer Science.
  • Mathematical Modeling and Probability Theory.