Institution: Stanford University, Department of Computer Science

Title: Verification of concurrent programs: a temporal proof system

Author: Manna, Z ohar

Author: Pnueli, Amir

Date: June 1983

Abstract: A proof system based on temporal logic is presented for proving properties of concurrent programs based on the shared-variables computation model. The system consists of three parts: the general uninterpreted part, the domain dependent part and the program dependent part. In the general part we give a complete proof system for first-order temporal logic with detailed proofs of useful theorems. This logic enables reasoning about general time sequences. The domain dependent part characterizes the special properties of the domain over which the program operates. The program dependent part introduces program axioms which restrict the time sequences considered to be execution sequences of a given program. The utility of the full system is demonstrated by proving invariance, liveness and precedence properties of several concurrent programs. Derived proof principles for these classes of properties are obtained and lead to a compact representation of proofs.

http://i.stanford.edu/pub/cstr/reports/cs/tr/83/967/CS-TR-83-967.pdf