Verifying Properties of Parallel Programs: An Axiomatic Approach

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.

CACM May, 1976

Owicki, S.
Gries, D.

structured multiprogramming correctness proofs, program
verification, concurrent processes, synchronization, 
mutual exclusion, deadlock

4.32 4.35 5.21 5.24

CA760506 JB January 4, 1978  3:23 PM

2021	4	2865
2222	4	2865
2227	4	2865
2315	4	2865
2326	4	2865
2470	4	2865
2732	4	2865
2865	4	2865
2865	4	2865
2866	4	2865
2896	4	2865
2898	4	2865
2943	4	2865
2972	4	2865
3014	4	2865
3043	4	2865
3068	4	2865
3077	4	2865
3128	4	2865
3143	4	2865
3144	4	2865
1834	5	2865
2597	5	2865
2865	5	2865
2865	5	2865
2865	5	2865
3128	5	2865
3148	5	2865
1860	6	2865
2150	6	2865
2376	6	2865
2436	6	2865
2597	6	2865
2817	6	2865
2865	6	2865
2865	6	2865
2866	6	2865
2870	6	2865
2912	6	2865
2939	6	2865
3073	6	2865
3082	6	2865