Properties of Concurrent Programs

Chandy, K. Mani (1993) Properties of Concurrent Programs. Computer Science Technical Reports, California Institute of Technology , Pasadena, CA. (Unpublished) https://resolver.caltech.edu/CaltechCSTR:1993.cs-tr-93-24

Preview

Postscript - Submitted Version
See Usage Policy.
172kB

Preview

PDF - Submitted Version
See Usage Policy.
393kB

Use this Persistent URL to link to this item: https://resolver.caltech.edu/CaltechCSTR:1993.cs-tr-93-24

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.

Item Type:

Report or Paper (Technical Report)

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.

Group:

Computer Science Technical Reports

Funders:

Funding Agency	Grant Number
Air Force Office of Scientific Research (AFOSR)	AFOSR-91-0070

Series Name:

Computer Science Technical Reports

DOI:

10.7907/Z9ZS2TJP

Record Number:

CaltechCSTR:1993.cs-tr-93-24

Persistent URL:

https://resolver.caltech.edu/CaltechCSTR:1993.cs-tr-93-24

Usage Policy:

You are granted permission for individual, educational, research and non-commercial reproduction, distribution, display and performance of this work in any format.

ID Code:

26763

Collection:

CaltechCSTR

Deposited By:

Imported from CaltechCSTR

Deposited On:

25 Apr 2001

Last Modified:

03 Oct 2019 03:17

Repository Staff Only: item control page