Accession Number : AD0764272

Title :   A Heuristic Approach to Program Verification.

Descriptive Note : Technical rept.,

Corporate Author : STANFORD UNIV CALIF DEPT OF COMPUTER SCIENCE

Personal Author(s) : Katz,Shmuel M. ; Manna,Zohar

Report Date : MAR 1973

Pagination or Media Count : 43

Abstract : The authors present various heuristic techniques for use in proving the correctness of computer programs. The techniques are designed to obtain automatically the inductive assertions attached to the loops of the program which previously required human understanding of the program performance. The authors distinguish between two general approaches: one in which the inductive assertion is obtained by analyzing predicates which are known to be true at the entrances and exits of the loop (top-down approach), and another in which we generate the inductive assertion directly from the statements of the loop (bottom-up approach). (Author)

Descriptors :   (*COMPUTER PROGRAMMING, MATHEMATICAL LOGIC), SET THEORY, INEQUALITIES, CORRECTIONS, ACCURACY

Subject Categories : Computer Programming and Software

Distribution Statement : APPROVED FOR PUBLIC RELEASE