Putting Time into Proof Outlines
Scheider, Fred B.; Bard, Bloom; Marzullo, Keith
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 structual operational semantics is outlines in the appendix.
computer science; technical report
Previously Published As