Published June 15, 1993
| Version Submitted
Technical Report
Open
Properties of Concurrent Programs
Creators
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
Additional details
Identifiers
- Eprint ID
- 26763
- Resolver ID
- CaltechCSTR:1993.cs-tr-93-24
Funding
- Air Force Office of Scientific Research (AFOSR)
- AFOSR-91-0070
Dates
- Created
-
2001-04-25Created from EPrint's datestamp field
- Updated
-
2019-10-03Created from EPrint's last_modified field
Caltech Custom Metadata
- Caltech groups
- Computer Science Technical Reports
- Series Name
- Computer Science Technical Reports