BIB-VERSION:: CS-TR-v2.0
          ID:: STAN//CS-TR-74-473
       ENTRY:: August 23, 1995
ORGANIZATION:: Stanford University, Department of Computer Science
       TITLE:: Automatic program verification II: verifying programs by
               algebraic and logical reduction.
        TYPE:: Technical Report
      AUTHOR:: Suzuki, Norihisa
        DATE:: December 1974
       PAGES:: 30
    ABSTRACT:: Methods for verifying programs written in a higher level
               programming language are devised and implemented. The system
               can verify programs written in a subset of PASCAL, which may
               have data structures and control structures such as WHILE,
               REPEAT, FOR, PROCEDURE, FUNCTION and COROUTINE. The process
               of creation of verification conditions is an extension of the
               work done by Igarashi, London and Luckham which is based on
               the deductive theory by Hoare. Verification conditions are
               proved using specialized simplification and proof techniques,
               which consist of an arithmetic simplifier, equality
               replacement rules, fast algorithm for simplifying formulas
               using propositional truth value evaluation, and a depth first
               proof search process. The basis of deduction mechanism used
               in this prover is Gentzen-type formal system. Several sorting
               programs including Floyd's TREESORT3 and Hoare's FIND are
               verified. It is shown that the resulting array is not only
               well-ordered but also a permutation of the input array.
       NOTES:: [Adminitrivia V1/Prg/19950823]
         END:: STAN//CS-TR-74-473