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

Empty on purpose

copy

Related

Distinct fromowicki1975axiomatic
Distinct fromowicki1976verifying
Distinct frompnueli1977temporal

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 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.