|
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)
| Pages: |
27 |
| Report Date: |
MAY 1982 |
| Contract Number: |
N00014-76-C-0687, AFOSR-81-001 |
| Report Number: |
A614231 |
Report Unavailable |
| This title is unavailable from Storming Media. We do not know when it might be available, if at all. We list the report on our site for bibliographic completeness, to help our users know what other work has been performed in this field. Please note that as with all titles on this site, we do not have contact information for any of the authors. Nor can we give any suggestions on how one might obtain this report. |
|
|
|
|
|
Keywords relating to this report:
Email This Abstract
