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