Technical Report CS0633

Authors: Snmuel Katz and Doron Peled
Abstract: We present a formal proof method based on a partial order semantics for parallel and distributed programs. In this view, a program's semantics is given by a collection of partial orders of the events which can occur during execution. Rather than using the partial orders directly, the basis of the method assumes the sets of interleaving sequences with global states that are consistent with each partial order (each such set is called an interleaving set). The proof rules allow concluding the correctness of certain classes of properties for all interleaving sequences, even though the property is only demonstrated directly for a subset of the sequences. The subset used must include a representative sequence from each interleaving set, and the proof rules guarantee that this is the case when they may be applied. The method employs proof lattices, and is expressed using the temporal logic ISTL*. By choosing a subset with appropriate sequences, simpler intennediate assertions can be used than in previous fonnal approaches.
CopyrightThe above paper is copyright by the Technion, Author(s), or others. Please contact the author(s) for more information

Remark: Any link to this technical report should be to this page (, rather than to the URL of the PDF files directly. The latter URLs may change without notice.

To the list of the CS technical reports of 1990
To the main CS technical reports page

Computer science department, Technion