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