Accession Number : ADA131501

Title :   Verification of Concurrent Programs: A Temporal Proof System,


Personal Author(s) : Manna,Zohar ; Pnueli,Amir

PDF Url : ADA131501

Report Date : Jun 1983

Pagination or Media Count : 93

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 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.

Descriptors :   *Computer program verification, *Mathematical logic, Theorems, Sharing, Variables, Mathematical models, Time domain, Reasoning, Time, Sequences, Syntax, Semantics, Invariance

Subject Categories : Theoretical Mathematics
      Computer Programming and Software

Distribution Statement : APPROVED FOR PUBLIC RELEASE