Publisher's Synopsis
A logic for reasoning about timing properties of concurrent programs is presented. The logic is based on Hoare-style proof outlines and can handle maximal parallelism as well as certain resource-constrained execution environments. The correctness proof for a mutual exclusion protocol that uses execution timings in a subtle way illustrates the logic in action. A soundness proof using structural operational semantics is outlined in the appendix. Schneider, Fred B. and Bloom, Bard and Marzullo, Keith Unspecified Center N00014-91-J-1219; NSF CCR-87-01103; NSF CCR-90-14363; NAG2-593...
