Putting Time Into Proof Outlines.

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 structural operational semantics is outlined in the appendix. Concurrent program verification, Timing properties, Safety properties, Real-time programming, Real-time actions, Proof outlines.

Document Details

Document Type
Technical Report
Publication Date
Mar 10, 1993
Accession Number
ADA262086

Entities

People

  • Bard Bloom
  • Fred B. Schneider
  • Keith Marzullo

Organizations

  • Cornell University

Tags

DTIC Thesaurus Topics

  • Biological Phenomena
  • Cognition
  • Computer Programming
  • Computing-Related Activities
  • Ecological And Environmental Phenomena
  • Environment
  • Linguistics
  • Mental Processes
  • Psychological Phenomena And Processes
  • Reasoning
  • Semantics
  • Social Sciences
  • Verification

Fields of Study

  • Computer science

Readers

  • Business Analytics
  • Mathematical Modeling and Probability Theory.