Report Number: CS-TR-90-1321
Institution: Stanford University, Department of Computer Science
Title: Tools and rules for the practicing verifier
Author: Manna, Z ohar
Author: Pnueli, Amir
Date: July 1990
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.
http://i.stanford.edu/pub/cstr/reports/cs/tr/90/1321/CS-TR-90-1321.pdf