Verifying Temporal Properties without Using Temporal Logic,

Abstract

A new approach for proving temporal properties of concurrent programs is presented. The approach does not use temporal logic. To show that a program satisfies a given temporal property, the property is first decomposed into proof obligations. These obligations are then discharge by devising suitable invariant assertions and variant functions for the program. The approach is quite general - it handles a superset of the properties that can be expressed in linear-time temporal logic. Keywords: Computer program verification. (Author)

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Dec 01, 1985
Accession Number
ADA164820

Entities

People

  • Bowen Alpern
  • Fred B. Schneider

Organizations

  • Cornell University

Tags

Communities of Interest

  • C4I
  • Materials and Manufacturing Processes

DTIC Thesaurus Topics

  • Automata
  • Carbonate Esters
  • Classification
  • Computer Program Verification
  • Computer Programming
  • Computer Programs
  • Computer Science
  • Computers
  • Construction
  • Language
  • Length
  • Military Research
  • Nutrition Disorders
  • Security
  • Simulations
  • Universities
  • Verification

Fields of Study

  • Computer science

Readers

  • Adaptive Control and Estimation with Uncertainty in Dynamic Systems.
  • Coastal Oceanography
  • Computational Linguistics