Welcome to the new version of CaltechAUTHORS. Login is currently restricted to library staff. If you notice any issues, please email coda@library.caltech.edu
Published April 25, 2001 | Submitted
Report Open

Properties of Concurrent Programs

Abstract

A program property is a predicate on programs. In this paper we explore program properties of the form U -> V where U and V are either predicates on states of a program or program properties, and -> satisfies three rules that are also used in reasoning about sequential programs and safety properties of parallel programs. We show how such properties can be used to reason about concurrent programs.

Additional Information

© 1993 California Institute of Technology June 15, 1993. This paper was completely rewritten based on constructive criticism form J. Misra, E.W. Dijkstra and B. Sanders. Thanks to suggestions from Rustan Leino and many at Caltech. Finally, many thanks to Cliff Jones and David Gries for careful reading and key insights. Supported in part by AFOSR 91-0070.

Attached Files

Submitted - 93-24.pdf

Submitted - postscript.ps

Files

93-24.pdf
Files (565.1 kB)
Name Size Download all
md5:b9515736196d2ff576677c2b96cf5a46
172.0 kB Download
md5:01258c64845c8dd116fa147ecfe14951
393.1 kB Preview Download

Additional details

Created:
August 20, 2023
Modified:
January 13, 2024