Verifying properties of parallel programs: An axiomatic approach
The work
| Authors | Susan Owicki; David Gries |
|---|---|
| Editors | |
| Type | article |
| Year | 1976 |
| Citekey | owicki1976verifying |
Where it appeared
| Published in | Communications of the ACM |
|---|---|
| Publisher | Association for Computing Machinery (ACM) |
| Volume | 19 |
| Issue | 5 |
| Pages | 279--285 |
Identifiers
| DOI | 10.1145/360051.360224 |
|---|---|
| OpenAlex | W1965662337 |
Access
| Landing page | https://doi.org/10.1145/360051.360224 |
|---|---|
| Free full text | https://dl.acm.org/doi/pdf/10.1145/360051.360224 |
Related
| Distinct from | owicki1975axiomatic |
|---|---|
| Distinct from | owicki1976axiomatic |
Abstract
An axiomatic method for proving a number of properties of parallel programs is presented. Hoare has given a set of axioms for partial correctness, but they are not strong enough in most cases. This paper defines a more powerful deductive system which is in some sense complete for partial correctness. A crucial axiom provides for the use of auxiliary variables, which are added to a parallel program as an aid to proving it correct. The information in a partial correctness proof can be used to prove such properties as mutual exclusion, freedom from deadlock, and program termination. Techniques for verifying these properties are presented and illustrated by application to the dining philosophers problem.
A copy is held
pdf, 655.6 kB. Not published — it may be under copyright. The facts and links here are.
How it got here
| How it got here | agent via bibtex |
|---|---|
| Added | 2026-08-05 00:00 UTC |
| Approved by | a person 2026-08-23 14:12 UTC |
Filed under
cacm gries owicki relatively-complete what-a-process-may-share
Cite it as
@article{owicki1976verifying,
title = {Verifying properties of parallel programs: An axiomatic approach},
author = {Susan Owicki and David Gries},
year = {1976},
journal = {Communications of the ACM},
publisher = {Association for Computing Machinery (ACM)},
volume = {19},
number = {5},
pages = {279--285},
doi = {10.1145/360051.360224},
}
This record lives at https://refs.drheap.org/owicki1976verifying/ and will keep doing so.