Accession Number : ADA132416

Title :   Verification of Concurrent Programs: Proving Eventualities by Well-Founded Ranking,

Corporate Author : STANFORD UNIV CA DEPT OF COMPUTER SCIENCE

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

PDF Url : ADA132416

Report Date : May 1982

Pagination or Media Count : 27

Abstract : In this paper, one of a series on verification of concurrent programs the authors present proof methods for establishing eventuality and until properties. The methods are based on well-founded ranking 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 decrease the rank when activated. Fairness then ensures that the program will eventually attain its goal. In the finite state case the proofs can be represented by diagrams. Several examples are given. (Author)

Descriptors :   *Computer program verification, *Computations, Convergence, Diagrams, Numerical methods and procedures, Ranking

Subject Categories : Numerical Mathematics
      Computer Programming and Software

Distribution Statement : APPROVED FOR PUBLIC RELEASE