The rely-guarantee method for verifying shared variable concurrent programs Export

@article{citeulike:4069238, abstract = {Compositional proof systems for shared variable concurrent programs can be devised by including the interference information in the specifications. The formalism falls into a category calledrely-guarantee (orassumption-commitment), in which a specification is explicitly (syntactically) split into two corresponding parts. This paper summarises existing work on the rely-guarantee method and gives a systematic presentation. A proof system for partial correctness is given first, thereafter it is demonstrated how the relevant rules can be adapted to verify deadlock freedom and convergence. Soundness and completeness, of which the completeness proof is new, are studied with respect to an operational model. We observe that the rely-guarantee method is in a sense a reformulation of the classical non-compositional Owicki \& Gries method, and we discuss throughout the paper the connection between these two methods.}, author = {Xu, Qiwen and de Roever, Willem and He, Jifeng}, citeulike-article-id = {4069238}, citeulike-linkout-0 = {http://dx.doi.org/10.1007/BF01211617}, citeulike-linkout-1 = {http://www.springerlink.com/content/pw138twh343x5466}, day = {1}, doi = {10.1007/BF01211617}, journal = {Formal Aspects of Computing}, keywords = {concurrent, guarantee, rely, verification}, month = {March}, number = {2}, pages = {149--174}, posted-at = {2009-02-19 01:46:21}, priority = {0}, title = {The rely-guarantee method for verifying shared variable concurrent programs}, url = {http://dx.doi.org/10.1007/BF01211617}, volume = {9}, year = {1997} }

TY - JOUR ID - citeulike:4069238 L3 - citeulike-article-id:4069238 N2 - Compositional proof systems for shared variable concurrent programs can be devised by including the interference information in the specifications. The formalism falls into a category calledrely-guarantee (orassumption-commitment), in which a specification is explicitly (syntactically) split into two corresponding parts. This paper summarises existing work on the rely-guarantee method and gives a systematic presentation. A proof system for partial correctness is given first, thereafter it is demonstrated how the relevant rules can be adapted to verify deadlock freedom and convergence. Soundness and completeness, of which the completeness proof is new, are studied with respect to an operational model. We observe that the rely-guarantee method is in a sense a reformulation of the classical non-compositional Owicki & Gries method, and we discuss throughout the paper the connection between these two methods. IS - 2 JF - Formal Aspects of Computing EP - 174 TI - The rely-guarantee method for verifying shared variable concurrent programs VL - 9 SP - 149 KW - concurrent KW - guarantee KW - rely KW - verification AU - Xu, Qiwen AU - de Roever, Willem AU - He, Jifeng PY - 1997/03/01/ UR - http://dx.doi.org/10.1007/BF01211617 ER -