Verifying Temporal Properties without Using Temporal Logic

摘要

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 discharged 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)