{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T19:04:54Z","timestamp":1743102294532,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":13,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540402534"},{"type":"electronic","value":"9783540448808"}],"license":[{"start":{"date-parts":[[2003,1,1]],"date-time":"2003-01-01T00:00:00Z","timestamp":1041379200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2003,1,1]],"date-time":"2003-01-01T00:00:00Z","timestamp":1041379200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/3-540-44880-2_18","type":"book-chapter","created":{"date-parts":[[2007,7,3]],"date-time":"2007-07-03T16:12:53Z","timestamp":1183479173000},"page":"280-299","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Compositional Verification for Object-Z"],"prefix":"10.1007","author":[{"given":"Kirsten","family":"Winter","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Graeme","family":"Smith","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2003,5,27]]},"reference":[{"key":"18_CR1","doi-asserted-by":"crossref","unstructured":"E. A. Emerson. Temporal and modal logic. In J. van Leeuwen, editor, Handbook of Theoretical Coomputer Science, volume B. Elsevier Science Publishers, 1990.","DOI":"10.1016\/B978-0-444-88074-1.50021-4"},{"issue":"3","key":"18_CR2","doi-asserted-by":"publisher","first-page":"843","DOI":"10.1145\/177492.177725","volume":"16","author":"O. Grumberg","year":"1994","unstructured":"O. Grumberg and D.E. Long. Model checking and modular verification. ACM Transactions on Programming Languages and Systems, 16(3):843\u2013871, 1994.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"18_CR3","doi-asserted-by":"crossref","unstructured":"A. Griffiths. Modular reasoning in Object-Z. In W. Wong and K. Leung, editors, Proc. of the Joint 1997 Asia Pacific Software Engineering Conference and International Computer Science Conference, IEEE, pages 140\u2013149. Computer Society Press, 1997.","DOI":"10.1109\/APSEC.1997.640171"},{"key":"18_CR4","doi-asserted-by":"crossref","unstructured":"A. Pnueli. In transition from global to modular temporal reasoning about programs. In K. R. Apt, editor, Logics and Models of Concurrent Systems, volume 13 of NATO ASI Series, pages 123\u2013144. Springer-Verlag, 1985.","DOI":"10.1007\/978-3-642-82453-1_5"},{"key":"18_CR5","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"82","DOI":"10.1007\/3-540-45648-1_5","volume-title":"Proc. of Int. Conf. of Z and B Users (ZB 2002)","author":"G. Smith","year":"2002","unstructured":"G. Smith, F. Kamm\u00fcller, and T. Santen. Encoding Object-Z in Isabelle\/HOL. In D. Bert, J.P. Bowen, M.C. Henson, and K. Robinson, editors, Proc. of Int. Conf. of Z and B Users (ZB 2002), volume 2272 of LNCS, pages 82\u201399. Springer-Verlag, 2002."},{"key":"18_CR6","unstructured":"G. Smith. An Object-Oriented Approach to Formal Specification. PhD thesis, Department of Computer Science, University of Queensland, 1992."},{"issue":"3","key":"18_CR7","doi-asserted-by":"publisher","first-page":"289","DOI":"10.1007\/BF01211075","volume":"7","author":"G. Smith","year":"1995","unstructured":"G. Smith. A fully abstract semantics of classes for Object-Z. Formal Aspects of Computing, 7(3):289\u2013313, 1995.","journal-title":"Formal Aspects of Computing"},{"key":"18_CR8","doi-asserted-by":"crossref","unstructured":"G. Smith. Reasoning about Object-Z specifications. In Proc. of the Asia-Pacific Software Engineering Conference (APSEC95), IEEE, pages 489\u2013497. Computer Society Press, 1995.","DOI":"10.1109\/APSEC.1995.496998"},{"key":"18_CR9","doi-asserted-by":"crossref","unstructured":"G. Smith. The Object-Z Specification Language. Kluwer Academic Publishers, 2000.","DOI":"10.1007\/978-1-4615-5265-9"},{"key":"18_CR10","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"588","DOI":"10.1007\/3-540-36103-0_60","volume-title":"Proc. on Int. Conference on Formal Engineering Methods (ICFEM 2002)","author":"G. Smith","year":"2002","unstructured":"G. Smith. Introducing reference semantics via refinement. In C. George and H. Miao, editors, Proc. on Int. Conference on Formal Engineering Methods (ICFEM 2002), volume 2495 of LNCS, pages 588\u2013599. Springer-Verlag, 2002."},{"key":"18_CR11","unstructured":"J.M. Spivey. The Z Notation \u2014 A Reference Manual. Prentice Hall, 1992."},{"key":"18_CR12","series-title":"Lect Notes Comput Sci","volume-title":"3rd International Conference of Z and B USers (ZB 2003)","author":"G. Smith","year":"2003","unstructured":"G. Smith and K. Winter. Proving temporal properties of Z specificatons using abstraction. In 3rd International Conference of Z and B USers (ZB 2003), LNCS. Springer-Verlag, 2003. This volume."},{"key":"18_CR13","doi-asserted-by":"crossref","unstructured":"J.C.P. Woodcock and S.M. Brien. $$ \\mathcal{W} $$ : A logic for Z. In Z User Workshop (ZUM\u201992), Workshops in Computing, pages 77\u201398. Springer-Verlag, 1992.","DOI":"10.1007\/978-1-4471-3203-5_4"}],"container-title":["Lecture Notes in Computer Science","ZB 2003: Formal Specification and Development in Z and B"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44880-2_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,18]],"date-time":"2025-01-18T04:04:09Z","timestamp":1737173049000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/3-540-44880-2_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540402534","9783540448808"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/3-540-44880-2_18","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2003]]},"assertion":[{"value":"27 May 2003","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}