An axiomatic proof technique for parallel programs I

The work

AuthorsSusan Owicki; David Gries
Editors
Typearticle
Year1976
Citekeyowicki1976axiomatic

Where it appeared

Published inActa Informatica
PublisherSpringer
Volume6
Issue4
Pages319--340

Identifiers

DOI10.1007/bf00268134
OpenAlexW1964727056

Access

Landing pagehttps://doi.org/10.1007/bf00268134

Settled

CopyClosed at Springer, verified rather than assumed. A note on this record already recorded that `fetchable.py` has no route to it; the finding was never written into the field, so the queue went on offering a fetch. OpenAlex answers for `10.1007/bf00268134`: `is_oa: false`, `oa_status: closed`, `oa_url: null`, `any_repository_has_fulltext: false`, and one location -- the Acta Informatica landing page at doi.org. So there is nothing for a person to click through to either, which is what makes this settleable where `fischer1983impossibility` and `boer2025footprint` are not; those are open articles that a host refuses to this account, and they carry a click-through URL instead of a settle. **The corpus is not without the Owicki-Gries method.** A note on this record already sets out the practical position: the thesis `owicki1975axiomatic` is held but its scan carries about 210 characters of text layer, so it must be rendered to be read, and `owicki1976verifying` -- the CACM paper -- is held with a full text layer and is the way in. This settle closes the acquisition question for the Acta Informatica paper; it does not leave a reader without the material.

Related

Distinct fromowicki1975axiomatic The 1975 record is a technical report with no container; the 1976 is the Acta Informatica paper of nearly the same title. That has the shape of a report later published, which would make it a version relation rather than two independent works -- unverified here, and flagged for the same reason as the Butler surveys in routing-attacks. Note also that the Acta paper is titled '... I', and the corpus holds no part II.
Distinct fromowicki1975axiomatic
Distinct fromowicki1976verifying

Abstract

A language for parallel programming, with a primitive construct for synchronization and mutual exclusion, is presented. Hoare's deductive system for proving partial correctness of sequential programs is extended to include the parallelism described by the language. The proof method lends insight into how one should understand and present parallel programs. Examples are given using several of the standard problems in the literature. Methods for proving termination and the absence of deadlock are also given.

How it got here

How it got hereagent via openalex
Added2026-08-04 00:00 UTC
Approved bya person 2026-08-24 07:29 UTC

Filed under

gries owicki relatively-complete what-a-process-may-share

Cite it as

@article{owicki1976axiomatic,
  title        = {An axiomatic proof technique for parallel programs I},
  author       = {Susan Owicki and David Gries},
  year         = {1976},
  journal      = {Acta Informatica},
  publisher    = {Springer},
  volume       = {6},
  number       = {4},
  pages        = {319--340},
  doi          = {10.1007/bf00268134},
}

This record lives at https://refs.drheap.org/owicki1976axiomatic/ and will keep doing so.