BIB-VERSION:: CS-TR-v2.0
          ID:: STAN//CS-TR-73-365
       ENTRY:: September 25, 1995
ORGANIZATION:: Stanford University, Department of Computer Science
       TITLE:: Automatic program verification I: a logical basis and its
               implementation.
        TYPE:: Technical Report
      AUTHOR:: Igarashi, Shigeru
      AUTHOR:: London, Ralph L.
      AUTHOR:: Luckham, David C.
        DATE:: May 1973
       PAGES:: 27
    ABSTRACT:: Defining the semantics of programming languages by axioms and
               rules of inference yields a deduction system within which
               proofs may be given that programs satisfy specifications. The
               deduction system herein is shown to be consistent and also
               deduction complete with respect to Hoare's system. A
               subgoaler for the deduction system is described whose input
               is a significant subset of Pascal programs plus inductive
               assertions. The output is a set of verification conditions or
               lemmas to be proved. Several non-trivial arithmetic and
               sorting programs have been shown to satisfy specifications by
               using an interactive theorem prover to automatically generate
               proofs of the verification conditions. Additional components
               for a more powerful verification system are under
               construction.
       NOTES:: [Adminitrivia V1/Prg/19950925]
         END:: STAN//CS-TR-73-365