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.
dvi
ps
BibTeX:
@InProceedings{Prensa01,
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{http://computer.org/cspress/CATALOG/pr00990.htm}}
}