JavaScript is disabled for your browser. Some features of this site may not work without it.
Proving Temporal Properties of Concurrent Programs: A Non-Temporal Approach

Author
Alpern, Bowen
Abstract
This thesis develops a new method for proving properties of concurrent programs and gives formal definitions for safety and liveness. A property is specified by a property recognizer - a finite-state machine that accepts the sequences of program states in the property it specifies. A property recognizer can be constructed for any temporal logic formula. (ABRIDGED ABSTRACT)
Date Issued
1986-02Publisher
Cornell University
Subject
computer science; technical report
Previously Published As
http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR86-732
Type
technical report