BIB-VERSION:: CS-TR-v2.0
          ID:: STAN//CS-TR-73-341
       ENTRY:: September 25, 1995
ORGANIZATION:: Stanford University, Department of Computer Science
       TITLE:: A heuristic approach to program verification.
        TYPE:: Technical Report
      AUTHOR:: Katz, Shmuel M.
      AUTHOR:: Manna, Zohar
        DATE:: March 1973
       PAGES:: 42
    ABSTRACT:: We 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's performance.
               We distinguish between two general approaches: one in which
               we obtain the inductive assertion by analyzing predicates
               which are known to be true at the entrances and exits of the
               loop ($underline{top-down}$ approach), and another in which
               we generate the inductive assertion directly from the
               statements of the loop ($underline{bottom-up}$ approach).
       NOTES:: [Adminitrivia V1/Prg/19950925]
         END:: STAN//CS-TR-73-341