Report Number: CS-TR-84-1005
Institution: Stanford University, Department of Computer Science
Title: Adequate proof principles for invariance and liveness properties of concurrent programs
Author: Manna, Z ohar
Author: Pnueli, Amir
Date: May 1984
Abstract: This paper presents proof principles for establishing invariance and liveness properties of concurrent programs. Invariance properties are established by systematically checking that they are preserved by every atomic instruction in the program. The methods for establishing liveness properties are based on 'well-founded asserations' and are applicable to both "just" and "fair" computations. These methods do not assume a decrease 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. In the finite state case such proofs can be represented by diagrams. Several examples are given.
http://i.stanford.edu/pub/cstr/reports/cs/tr/84/1005/CS-TR-84-1005.pdf