Completeness of the Owicki-Gries System for Parameterized Parallel Programs.

Leonor Prensa Nieto

The Owicki-Gries system is extended to allow the verification of parameterized programs of the form "|| S(i,n)" where for each n we obtain a parallel program consisting of n sequential processes. By the completeness of the original Owicki-Gries system, we know that for any valid specification of a parallel program with a fixed number of components there exists a proof in the system. However, we would like to know if there exists a single proof that works for any number of components. In this paper we prove completeness of the extended system, thus giving a positive answer to the question.




  author =	 {Prensa Nieto, Leonor},
  title =	 {Completeness of the {Owicki-Gries} System for Parameterized Parallel Programs},
  booktitle =	 {6th International Workshop on Formal Methods for Parallel Programming: Theory and
                  Applications. Held in conjunction with the 15th International Parallel and Distributed Processing Symposium},
  publisher =	 {IEEE CS Press},
  editor =	 {Michel Charpentier and Beverly Sanders},
  year =	 {2001}
  note =         {Available at \verb{}}