A proof technique for parallel programs. (English) Zbl 0543.68010

Summary: In this paper we present a set of axioms and rules of inference for a parallel programming language with shared variables and synchronization statements. The important difference between our approach and that of S. Owicki and D. Gries [Commun. ACM 19, 279-285 (1976; Zbl 0322.68010)] is that our semantics does not contain anything similar to their ’inference freedom’ check, resulting in a much greater isolation of the proofs of the individual processes than is possible in their system. We illustrate our proof technique with some simple examples.


68Q60 Specification and verification (program logics, model checking, etc.)
68N25 Theory of operating systems


Zbl 0322.68010
Full Text: DOI


[1] Hoarc, C.A.R., Communicating sequential processes, Comm. ACM, 21, 666-667, (1978) · Zbl 0383.68028
[2] Owicki, S.S.; Gries, D., An axiomatic proof technique for parallel programs, Acta. inform., 6, 319-340, (1976) · Zbl 0312.68011
[3] Owicki, S.S.; Gries, D., Verifying properties of parallel programs: an axiomatic approach, Comm. ACM, 19, 279-285, (1976) · Zbl 0322.68010
[4] Rosen, B.K., Correctness of parallel programs: the church-rosser approach, IBM res. rept. RC5107, (1974)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.