Putting Time into Proof Outlines

Abstract

A logic for reasoning about timing properties of concurrent programs is presented. The logic is based on proof outlines and can handle maximal parallelism as well as 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.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Sep 01, 1991
Accession Number
ADA242522

Entities

People

  • Bard Bloom
  • Fred B. Schneider
  • Keith Marzullo

Organizations

  • Cornell University

Tags

Communities of Interest

  • Materials and Manufacturing Processes

DTIC Thesaurus Topics

  • Abstracts
  • Classification
  • Computer Programming
  • Computer Science
  • Computers
  • Control Systems
  • Environment
  • Invariance
  • Language
  • Military Research
  • New York
  • Programming Languages
  • Reasoning
  • Security
  • Sequences
  • Test And Evaluation
  • Universities

Fields of Study

  • Computer science

Readers

  • Applied Combinatorial Optimization and Logic Circuit Design.
  • Parallel and Distributed Computing.
  • Theoretical Analysis.