BIB-VERSION:: CS-TR-v2.0
          ID:: STAN//CS-TR-82-915
       ENTRY:: June 01, 1995
ORGANIZATION:: Stanford University, Department of Computer Science
       TITLE:: Verification of concurrent programs: proving eventualities by
               well-founded ranking
        TYPE:: Technical Report
      AUTHOR:: Manna, Zohar
      AUTHOR:: Pnueli, Amir
        DATE:: May 1982
       PAGES:: 28
    ABSTRACT:: In this paper, one of a series on verification of concurrent
               programs, we present proof methods for establishing
               eventuality and until properties. The methods are based on
               well-founded ranking and are applicable to both "just" and
               "fair" computations. These methods do not assume a decrcase
               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.
       NOTES:: [Adminitrivia V1/Prg/19950601]
         END:: STAN//CS-TR-82-915