Properties of Concurrent Programs

1 December 1994

journal article
Published by Association for Computing Machinery (ACM) in Formal Aspects of Computing

Vol. 6 (6), 607-619
https://doi.org/10.1007/bf03259388

Abstract

A program property is a predicate on programs. In this paper we explore program properties for safety, progress and parallel composition, 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 enjoyed by implication. We show how such properties can be used to reason about concurrent programs. Our motivation is to explore methods of reasoning based on a very small number of widely-known rules.

Keywords

PROGRAM PROPERTY
FORM U
CONCURRENT PROGRAMS
CONCURRENCY
SAFETY
PROGRESS
TEMPORAL LOGIC
UNITY THEORY
FAIRNESS
HOARE TRIPLES

This publication has 2 references indexed in Scilit:

Predicate Calculus and Program Semantics
Published by Springer Nature ,1990
An axiomatic basis for computer programming
Communications of the ACM, 1969

Cited by 1 article