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

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)

Open PDF

Document Details

Document Type
Technical Report
Publication Date
May 01, 1982
Accession Number
ADA132416

Entities

People

  • Amir Pnueli
  • Zohar Manna

Organizations

  • Stanford University

Tags

Communities of Interest

  • Materials and Manufacturing Processes

DTIC Thesaurus Topics

  • Air Force
  • Applied Mathematics
  • Binomials
  • Computations
  • Computer Science
  • Computers
  • Consumers
  • Contracts
  • Convergence
  • Guarantees
  • Instructions
  • Invariance
  • Mathematics
  • Reasoning
  • Sequences
  • Terminals
  • Transitions

Fields of Study

  • Computer science

Readers

  • Artificial Intelligence
  • Regression Analysis.
  • Software Engineering.