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.