%0 Journal Article %1 susan1976axiomatic %A Owicki, Susan %A Gries, David %D 1976 %J Acta Informatica %K concurrent verification %N 4 %P 319--340 %T An axiomatic proof technique for parallel programs I %U http://dx.doi.org/10.1007/BF00268134 %V 6 %X A language for parallel programming, with a primitive construct for synchronization and mutual exclusion, is presented. Hoare's deductive system for proving partial correctness of sequential programs is extended to include the parallelism described by the language. The proof method lends insight into how one should understand and present parallel programs. Examples are given using several of the standard problems in the literature. Methods for proving termination and the absence of deadlock are also given. ER -

@article{susan1976axiomatic, abstract = {A language for parallel programming, with a primitive construct for synchronization and mutual exclusion, is presented. Hoare's deductive system for proving partial correctness of sequential programs is extended to include the parallelism described by the language. The proof method lends insight into how one should understand and present parallel programs. Examples are given using several of the standard problems in the literature. Methods for proving termination and the absence of deadlock are also given. ER -}, added-at = {2010-01-28T17:03:34.000+0100}, author = {Owicki, Susan and Gries, David}, biburl = {https://www.bibsonomy.org/bibtex/25447c652aca55c9d4aedcf2befdb98a8/giuliano.losa}, description = {An axiomatic proof technique for parallel programs}, interhash = {24bd942eeaeecb96e503546a9b64674d}, intrahash = {5447c652aca55c9d4aedcf2befdb98a8}, journal = {Acta Informatica}, keywords = {concurrent verification}, month = dec, number = 4, pages = {319--340}, timestamp = {2010-01-28T17:03:34.000+0100}, title = {An axiomatic proof technique for parallel programs I}, url = {http://dx.doi.org/10.1007/BF00268134}, volume = 6, year = 1976 }