Cornell University
Library
Cornell UniversityLibrary

eCommons

Help
Log In(current)
  1. Home
  2. Cornell Computing and Information Science
  3. Computer Science
  4. Computer Science Technical Reports
  5. Putting Time into Proof Outlines

Putting Time into Proof Outlines

File(s)
93-1333.pdf (2.87 MB)
93-1333.ps (643.34 KB)
Permanent Link(s)
https://hdl.handle.net/1813/6099
Collections
Computer Science Technical Reports
Author
Scheider, Fred B.
Bard, Bloom
Marzullo, Keith
Abstract

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.

Date Issued
1991-09
Publisher
Cornell University
Keywords
computer science
•
technical report
Previously Published as
http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR93-1333
Type
technical report

Site Statistics | Help

About eCommons | Policies | Terms of use | Contact Us

copyright © 2002-2026 Cornell University Library | Privacy | Web Accessibility Assistance