BIB-VERSION:: CS-TR-v2.0
          ID:: STAN//CS-TR-90-1321
       ENTRY:: September 14, 1994
ORGANIZATION:: Stanford University, Department of Computer Science
       TITLE:: Tools and rules for the practicing verifier
        TYPE:: Technical Report
      AUTHOR:: Manna, Zohar
      AUTHOR:: Pnueli, Amir
        DATE:: July 1990
       PAGES:: 35
    ABSTRACT:: The paper presents a minimal proof theory which is adequate
               for proving the main important temporal properties of
               reactive programs. The properties we consider consist of the
               classes of invariance, response, and precedence properties.
               For each of these classes we present a small set of rules
               that is complete for verifying properties belonging to this
               class. We illustrate the application of these rules by
               analyzing and verifying the properties of a new algorithm for
               mutual exclusion.
       NOTES:: [Adminitrivia V1/RAM/19940914]
         END:: STAN//CS-TR-90-1321