{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,15]],"date-time":"2024-09-15T13:31:14Z","timestamp":1726407074477},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540008866"},{"type":"electronic","value":"9783540365754"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/3-540-36575-3_24","type":"book-chapter","created":{"date-parts":[[2007,10,27]],"date-time":"2007-10-27T17:52:15Z","timestamp":1193507535000},"page":"348-362","source":"Crossref","is-referenced-by-count":21,"title":["The Rely-Guarantee Method in Isabelle\/HOL"],"prefix":"10.1007","author":[{"given":"Leonor Prensa","family":"Nieto","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2003,2,28]]},"reference":[{"unstructured":"W.-P. de Roever, F. S. de Boer, U. Hannemann, J. Hooman, Y. Lakhnech, M. Poel, and J. Zwiers. Concurrency Verification: Introduction to Compositional and Noncompositional Methods, volume 54 of Tracts in Theoretical Computer Science. Cambridge University Press, 2001.","key":"24_CR1"},{"doi-asserted-by":"crossref","unstructured":"S. O. Ehmety and L. C. Paulson. Program composition in Isabelle\/UNITY. In M. Charpentier and B. Sanders, editors, Formal Methods for Parallel Programming: Theory and Application, 2002.","key":"24_CR2","DOI":"10.1109\/IPDPS.2002.1016620"},{"key":"24_CR3","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"262","DOI":"10.1007\/3-540-45927-8_19","volume-title":"Thread-modular verification for sharedmemory programs","author":"C. Flanagan","year":"2002","unstructured":"C. Flanagan, S. Freund, and S. Qadeer. Thread-modular verification for sharedmemory programs. In European Symposium on Programming, volume 2305 of LNCS, pages 262\u2013277. Springer-Verlag, 2002."},{"unstructured":"J. Hooman. Developing proof rules for distributed real-time systems with PVS. In Proc. Workshop on Tool Support for System Development and Verification, volume 1 of BISS Monographs, pages 120\u2013139. Shaker Verlag, 1998.","key":"24_CR4"},{"issue":"4","key":"24_CR5","doi-asserted-by":"publisher","first-page":"596","DOI":"10.1145\/69575.69577","volume":"5","author":"C. B. Jones","year":"1983","unstructured":"C. B. Jones. Tentative steps towards a development method for interfering programs. ACM Transactions on Programming Languages and Systems, 5(4):596\u2013619, 1983.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"24_CR6","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"342","DOI":"10.1007\/3-540-48153-2_30","volume-title":"Advances in Hardware Design and Verification Methods: IFIP WG10.5 (CHARME\u201999)","author":"K. L. McMillan","year":"1999","unstructured":"K. L. McMillan. Circular compositional reasoning about liveness. In Advances in Hardware Design and Verification Methods: IFIP WG10.5 (CHARME\u201999), volume 1703 of LNCS, pages 342\u2013345. Springer-Verlag, 1999."},{"key":"24_CR7","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL-A Proof Assistant for Higher-Order Logic","author":"T. Nipkow","year":"2002","unstructured":"T. Nipkow, L. C. Paulson, and M. Wenzel. Isabelle\/HOL-A Proof Assistant for Higher-Order Logic, volume 2283 of LNCS. Springer-Verlag, 2002."},{"key":"24_CR8","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"188","DOI":"10.1007\/978-3-540-49020-3_13","volume-title":"Fundamental Approaches to Software Engineering","author":"T. Nipkow","year":"1999","unstructured":"T. Nipkow and L. Prensa Nieto. Owicki\/Gries in Isabelle\/HOL. In J.-P. Finance, editor, Fundamental Approaches to Software Engineering, volume 1577 of LNCS, pages 188\u2013203. Springer-Verlag, 1999."},{"issue":"6","key":"24_CR9","first-page":"1","volume":"23","author":"L. C. Paulson","year":"2001","unstructured":"L. C. Paulson. Mechanizing a theory of program composition for UNITY. ACM Transactions on Programming Languages and Systems, 23(6):1\u201330, 2001.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"doi-asserted-by":"crossref","unstructured":"L. Prensa Nieto. Completeness of the Owicki-Gries system for parameterized parallel programs. In M. Charpentier and B. Sanders, editors, 6th International Workshop on Formal Methods for Parallel Programming: Theory and Applications. Held in conjunction with the 15th International Parallel and Distributed Processing Symposium. IEEE CS Press, 2001.","key":"24_CR10","DOI":"10.1109\/IPDPS.2001.925138"},{"unstructured":"L. Prensa Nieto. Verification of Parallel Programs with the Owicki-Gries and Rely-Guarantee Methods in Isabelle\/HOL. PhD thesis, Technische Universit\u00e4t M\u00fcnchen, 2002. Available at \n                    http:\/\/tumb1.biblio.tu-muenchen.de\/publ\/diss\/allgemein.html\n                    \n                  .","key":"24_CR11"},{"unstructured":"J. Rushby. Formal verification of McMillan\u2019s compositional assume-guarantee rule. Technical report, Sept. 2001.","key":"24_CR12"},{"key":"24_CR13","doi-asserted-by":"publisher","first-page":"347","DOI":"10.1016\/0304-3975(88)90033-3","volume":"58","author":"C. Stirling","year":"1988","unstructured":"C. Stirling. A generalization of Owicki-Gries\u2019s Hoare logic for a concurrent while language. Theoretical Computer Science, 58:347\u2013359, 1988.","journal-title":"Theoretical Computer Science"},{"unstructured":"Q. Xu, W.-P. de Roever, and J. He. Rely-guarantee method for verifying shared variable concurrent programs. Technical Report 9502, Christian-Albrechts-Universit\u00e4t Kiel, March 1995.","key":"24_CR14"},{"issue":"2","key":"24_CR15","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1007\/BF01211617","volume":"9","author":"Q. Xu","year":"1997","unstructured":"Q. Xu, W.-P. de Roever, and J. He. The rely-guarantee method for verifying shared variable concurrent programs. Formal Aspects of Computing, 9(2):149\u2013174, 1997.","journal-title":"Formal Aspects of Computing"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-36575-3_24","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,2,24]],"date-time":"2019-02-24T12:23:10Z","timestamp":1551010990000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-36575-3_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540008866","9783540365754"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/3-540-36575-3_24","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2003]]}}}