BIB-VERSION:: CS-TR-v2.0
          ID:: STAN//CS-TR-84-1005
       ENTRY:: May 27, 1995
ORGANIZATION:: Stanford University, Department of Computer Science
       TITLE:: Adequate proof principles for invariance and liveness
               properties of concurrent programs
        TYPE:: Technical Report
      AUTHOR:: Manna, Zohar
      AUTHOR:: Pnueli, Amir
        DATE:: May 1984
       PAGES:: 38
    ABSTRACT:: This paper presents proof principles for establishing
               invariance and liveness properties of concurrent programs.
               Invariance properties are established by systematically
               checking that they are preserved by every atomic instruction
               in the program. The methods for establishing liveness
               properties are based on 'well-founded asserations' and are
               applicable to both "just" and "fair" computations. These
               methods do not assume a decrease of the rank at each
               computation step. It is sufficient that there exists one
               process which decreases the rank when activated. Fairness
               then ensures that the program will eventually attain its
               goal. In the finite state case such proofs can be represented
               by diagrams. Several examples are given.
       NOTES:: [Adminitrivia V1/Prg/19950527]
         END:: STAN//CS-TR-84-1005