Tools and Rules for the Practicing Verifier
Zohar Manna, Amir Pnueli · 1990
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. 1 Introduction In this paper we present a minimal proof theory that is adequate for proving interesting properties of concurrent programs. The simple theory is illustrated on a single example, which is a new and interesting algorithm for mutual exclusion [Szy88]. There are several points we would like to demonstrate in this paper. The first and main point is that a very little general (temporal) theory is required to handle the most important properties of concurrent programs. The types of properties, on w...