Accession Number:

ADA164820

Title:

Verifying Temporal Properties without Using Temporal Logic,

Descriptive Note:

Corporate Author:

CORNELL UNIV ITHACA NY DEPT OF COMPUTER SCIENCE

Personal Author(s):

Report Date:

1985-12-01

Pagination or Media Count:

43.0

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

Subject Categories:

  • Computer Programming and Software

Distribution Statement:

APPROVED FOR PUBLIC RELEASE