
Accession Number : ADA131501
Title : Verification of Concurrent Programs: A Temporal Proof System,
Corporate Author : STANFORD UNIV CA DEPT OF COMPUTER SCIENCE
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 sharedvariables 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 firstorder 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