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.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Mar 01, 1993
Accession Number
ADA264183

Entities

People

  • Bard Bloom
  • Fred B. Schneider
  • Keith Marzullo

Organizations

  • Cornell University

Tags

DTIC Thesaurus Topics

  • Abstracts
  • Computer Programming
  • Computer Science
  • Computers
  • Consistency
  • Intervals
  • Invariance
  • Language
  • Military Research
  • Programming Languages
  • Reasoning
  • Semantics
  • Sequences
  • Standards
  • Test And Evaluation
  • Time Intervals
  • Transitions

Fields of Study

  • Computer science

Readers

  • Computer Science.
  • Mathematical Modeling and Probability Theory.