{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,7]],"date-time":"2026-02-07T03:40:58Z","timestamp":1770435658967,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":37,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642103728","type":"print"},{"value":"9783642103735","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-10373-5_18","type":"book-chapter","created":{"date-parts":[[2009,11,16]],"date-time":"2009-11-16T11:45:27Z","timestamp":1258371927000},"page":"347-366","source":"Crossref","is-referenced-by-count":11,"title":["A Graph-Based Operational Semantics of OO Programs"],"prefix":"10.1007","author":[{"given":"Wei","family":"Ke","sequence":"first","affiliation":[]},{"given":"Zhiming","family":"Liu","sequence":"additional","affiliation":[]},{"given":"Shuling","family":"Wang","sequence":"additional","affiliation":[]},{"given":"Liang","family":"Zhao","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"18_CR1","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4419-8598-9","volume-title":"A Theory of Objects","author":"M. Abadi","year":"1996","unstructured":"Abadi, M., Cardelli, L.: A Theory of Objects. Springer, Heidelberg (1996)"},{"key":"18_CR2","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1109\/WICSA.2004.1310699","volume-title":"4th Working IEEE\/IFIP Conference on Software Architecture","author":"L. Baresi","year":"2004","unstructured":"Baresi, L., Heckel, R., Th\u00f6ne, S., Varr\u00f3, D.: Style-based refinement of dynamic software architectures. In: 4th Working IEEE\/IFIP Conference on Software Architecture, pp. 155\u2013164. IEEE Computer Society, Los Alamitos (2004)"},{"issue":"1-3","key":"18_CR3","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1016\/j.scico.2004.03.003","volume":"52","author":"P. Borba","year":"2004","unstructured":"Borba, P., Sampaio, A., Cavalcanti, A., Corn\u00e9lio, M.: Algebraic reasoning for object-oriented programming. Sci. Comput. Program.\u00a052(1-3), 53\u2013100 (2004)","journal-title":"Sci. Comput. Program."},{"key":"18_CR4","series-title":"Lecture Notes in Computer Science","first-page":"1","volume-title":"ECOOP 2003 - Object-Oriented Programming","author":"P. Borba","year":"2003","unstructured":"Borba, P., Sampaio, A., Corn\u00e9lio, M.: A refinement algebra for object-oriented programming. In: Cardelli, L. (ed.) ECOOP 2003. LNCS, vol.\u00a02743, pp. 1\u201337. Springer, Heidelberg (2003)"},{"issue":"6","key":"18_CR5","doi-asserted-by":"publisher","first-page":"533","DOI":"10.1002\/spe.370","volume":"31","author":"J. Boyland","year":"2001","unstructured":"Boyland, J.: Alias burying: Unique variables without destructive reads. Software Practice and Experience\u00a031(6), 533\u2013553 (2001)","journal-title":"Software Practice and Experience"},{"key":"18_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"344","DOI":"10.1007\/978-3-540-27864-1_25","volume-title":"Static Analysis","author":"M. Bozga","year":"2004","unstructured":"Bozga, M., Iosif, R., Lakhnech, Y.: On logics of aliasing. In: Giacobazzi, R. (ed.) SAS 2004. LNCS, vol.\u00a03148, pp. 344\u2013360. Springer, Heidelberg (2004)"},{"issue":"1-3","key":"18_CR7","doi-asserted-by":"publisher","first-page":"227","DOI":"10.1016\/j.tcs.2006.12.034","volume":"375","author":"S. Brookes","year":"2007","unstructured":"Brookes, S.: A semantics for concurrent separation logic. Theor. Comput. Sci.\u00a0375(1-3), 227\u2013270 (2007)","journal-title":"Theor. Comput. Sci."},{"key":"18_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1439","DOI":"10.1007\/3-540-48118-4_26","volume-title":"FM\u201999 - Formal Methods","author":"A. Cavalcanti","year":"1999","unstructured":"Cavalcanti, A., Naumann, D.: A weakest precondition semantics for an object-oriented language of refinement. In: Woodcock, J.C.P., Davies, J., Wing, J.M. (eds.) FM 1999. LNCS, vol.\u00a01709, pp. 1439\u20131460. Springer, Heidelberg (1999)"},{"key":"18_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1007\/11783596_10","volume-title":"Mathematics of Program Construction","author":"Y. Chen","year":"2006","unstructured":"Chen, Y., Sanders, J.W.: Compositional reasoning for pointer structures. In: Uustalu, T. (ed.) MPC 2006. LNCS, vol.\u00a04014, pp. 115\u2013139. Springer, Heidelberg (2006)"},{"key":"18_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/3-540-45337-7_4","volume-title":"ECOOP 2001 - Object-Oriented Programming","author":"D. Clarke","year":"2001","unstructured":"Clarke, D., Noble, J., Potter, J.: Simple ownership types for object containment. In: Knudsen, J.L. (ed.) ECOOP 2001. LNCS, vol.\u00a02072, pp. 53\u201376. Springer, Heidelberg (2001)"},{"issue":"10","key":"18_CR11","doi-asserted-by":"publisher","first-page":"48","DOI":"10.1145\/286942.286947","volume":"33","author":"D. Clarke","year":"1998","unstructured":"Clarke, D., Potter, J., Noble, J.: Ownership types for flexible alias protection. SIGPLAN Not.\u00a033(10), 48\u201364 (1998)","journal-title":"SIGPLAN Not."},{"key":"18_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"383","DOI":"10.1007\/978-3-540-30203-2_27","volume-title":"Graph Transformations","author":"A. Corradini","year":"2004","unstructured":"Corradini, A., Dotti, F.L., Foss, L., Ribeiro, L.: Translating Java code to graph transformation systems. In: Ehrig, H., Engels, G., Parisi-Presicce, F., Rozenberg, G. (eds.) ICGT 2004. LNCS, vol.\u00a03256, pp. 383\u2013398. Springer, Heidelberg (2004)"},{"issue":"3,4","key":"18_CR13","doi-asserted-by":"crossref","first-page":"241","DOI":"10.3233\/FI-1996-263402","volume":"26","author":"A. Corradini","year":"1996","unstructured":"Corradini, A., Montanari, U., Rossi, F.: Graph processes. Fundamenta Informaticae\u00a026(3,4), 241\u2013265 (1996)","journal-title":"Fundamenta Informaticae"},{"issue":"1","key":"18_CR14","first-page":"31","volume":"74","author":"H. Ehrig","year":"2006","unstructured":"Ehrig, H., Ehrig, K., Prange, U., Taentzer, G.: Fundamental theory for typed attributed graphs and graph transformation based on adhesive HLR categories. Fundamenta Informaticae\u00a074(1), 31\u201361 (2006)","journal-title":"Fundamenta Informaticae"},{"issue":"4","key":"18_CR15","first-page":"101","volume":"175","author":"A.P.L. Ferreira","year":"2007","unstructured":"Ferreira, A.P.L., Foss, L., Ribeiro, L.: Formal verification of object-oriented graph grammars specifications. ENTCS\u00a0175(4), 101\u2013114 (2007)","journal-title":"ENTCS"},{"key":"18_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"553","DOI":"10.1007\/BFb0055805","volume-title":"Mathematical Foundations of Computer Science 1998","author":"M. Gro\u00dfe-Rhode","year":"1998","unstructured":"Gro\u00dfe-Rhode, M., Parisi-Presicce, F., Simeoni, M.: Spatial and temporal refinement of typed graph transformation systems. In: Brim, L., Gruska, J., Zlatu\u0161ka, J. (eds.) MFCS 1998. LNCS, vol.\u00a01450, pp. 553\u2013561. Springer, Heidelberg (1998)"},{"key":"18_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1007\/978-3-540-85762-4_10","volume-title":"Theoretical Aspects of Computing - ICTAC 2008","author":"W. Harwood","year":"2008","unstructured":"Harwood, W., Cavalcanti, A., Woodcock, J.: A theory of pointers for the UTP. In: Fitzgerald, J.S., Haxthausen, A.E., Yenigun, H. (eds.) ICTAC 2008. LNCS, vol.\u00a05160, pp. 141\u2013155. Springer, Heidelberg (2008)"},{"issue":"1-2","key":"18_CR18","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1016\/j.tcs.2006.07.034","volume":"365","author":"J. He","year":"2006","unstructured":"He, J., Li, X., Liu, Z.: rCOS: A refinement calculus for object systems. Theor. Comput. Sci.\u00a0365(1-2), 109\u2013142 (2006)","journal-title":"Theor. Comput. Sci."},{"key":"18_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1007\/3-540-45832-8_14","volume-title":"Graph Transformation","author":"R. Heckel","year":"2002","unstructured":"Heckel, R., K\u00fcster, J.M., Taentzer, G.: Confluence of typed attributed graph transformation systems. In: Corradini, A., Ehrig, H., Kreowski, H.-J., Rozenberg, G. (eds.) ICGT 2002. LNCS, vol.\u00a02505, pp. 161\u2013176. Springer, Heidelberg (2002)"},{"key":"18_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-48743-3_1","volume-title":"ECOOP \u201999 - Object-Oriented Programming","author":"C.A.R. Hoare","year":"1999","unstructured":"Hoare, C.A.R., He, J.: A trace model for pointers and objects. In: Guerraoui, R. (ed.) ECOOP 1999. LNCS, vol.\u00a01628, pp. 1\u201317. Springer, Heidelberg (1999)"},{"key":"18_CR21","first-page":"3","volume":"212","author":"T. Hoare","year":"2008","unstructured":"Hoare, T., O\u2019Hearn, P.: Separation logic semantics for communicating processes. ENTCS\u00a0212, 3\u201325 (2008)","journal-title":"ENTCS"},{"issue":"1","key":"18_CR22","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1016\/0020-0190(89)90102-6","volume":"31","author":"T. Kamada","year":"1989","unstructured":"Kamada, T., Kawai, S.: An algorithm for drawing general undirected graphs. Information processing letters\u00a031(1), 7\u201315 (1989)","journal-title":"Information processing letters"},{"key":"18_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"186","DOI":"10.1007\/11768869_15","volume-title":"Formal Methods for Open Object-Based Distributed Systems","author":"H. Kastenberg","year":"2006","unstructured":"Kastenberg, H., Kleppe, A., Rensink, A.: Defining object-oriented execution semantics using graph transformations. In: Gorrieri, R., Wehrheim, H. (eds.) FMOODS 2006. LNCS, vol.\u00a04037, pp. 186\u2013201. Springer, Heidelberg (2006)"},{"key":"18_CR24","unstructured":"Ke, W., Liu, Z., Wang, S., Zhao, L.: Graph-based type system, operational semantics and implementation of an object-oriented programming language. Technical Report 410, UNU-IIST, P.O. Box 3058, Macau (2009), http:\/\/www.iist.unu.edu\/www\/docs\/techreports\/reports\/report410.pdf"},{"issue":"4","key":"18_CR25","doi-asserted-by":"publisher","first-page":"619","DOI":"10.1145\/1146809.1146811","volume":"28","author":"G. Klein","year":"2006","unstructured":"Klein, G., Nipkow, T.: A machine-checked model for a Java-like language, virtual machine, and compiler. ACM TOPLAS\u00a028(4), 619\u2013695 (2006)","journal-title":"ACM TOPLAS"},{"key":"18_CR26","unstructured":"Liu, Z., Morisset, C., Stolz, V.: rCOS: Theory and tool for component-based model driven development. Technical Report 406, UNU-IIST, P.O. Box 3058, Macau (2009), http:\/\/www.iist.unu.edu\/www\/docs\/techreports\/reports\/report406.pdf (to appear in LNCS)"},{"key":"18_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"189","DOI":"10.1007\/BFb0053062","volume-title":"ECOOP \u201996 - Object-Oriented Programming","author":"N. Minsky","year":"1996","unstructured":"Minsky, N.: Towards alias-free pointers. In: Cointe, P. (ed.) ECOOP 1996. LNCS, vol.\u00a01098, pp. 189\u2013209. Springer, Heidelberg (1996)"},{"issue":"1","key":"18_CR28","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/S0167-6423(00)00005-8","volume":"41","author":"D.A. Naumann","year":"2001","unstructured":"Naumann, D.A.: Predicate transformer semantics of a higher-order imperative language with record subtyping. Sci. Comput. Program.\u00a041(1), 1\u201351 (2001)","journal-title":"Sci. Comput. Program."},{"issue":"1","key":"18_CR29","doi-asserted-by":"publisher","first-page":"247","DOI":"10.1145\/1047659.1040326","volume":"40","author":"M. Parkinson","year":"2005","unstructured":"Parkinson, M., Bierman, G.: Separation logic and abstraction. SIGPLAN Not.\u00a040(1), 247\u2013258 (2005)","journal-title":"SIGPLAN Not."},{"key":"18_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"64","DOI":"10.1007\/978-3-540-39958-2_5","volume-title":"Formal Methods for Open Object-Based Distributed Systems","author":"C. Pierik","year":"2003","unstructured":"Pierik, C., de Boer, F.: A syntax-directed Hoare logic for object-oriented programming concepts. In: Najm, E., Nestmann, U., Stevens, P. (eds.) FMOODS 2003. LNCS, vol.\u00a02884, pp. 64\u201378. Springer, Heidelberg (2003)"},{"key":"18_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1007\/3-540-49099-X_11","volume-title":"Programming Languages and Systems","author":"A. Poetzsch-Heffter","year":"1999","unstructured":"Poetzsch-Heffter, A., M\u00fcller, P.: A programming logic for sequential Java. In: Swierstra, S.D. (ed.) ESOP 1999. LNCS, vol.\u00a01576, pp. 162\u2013176. Springer, Heidelberg (1999)"},{"key":"18_CR32","volume-title":"Proc. 17th Annual IEEE Symposium on Logic in Computer Science","author":"J. Reynolds","year":"2002","unstructured":"Reynolds, J.: Separation logic: A logic for shared mutable data structures. In: Proc. 17th Annual IEEE Symposium on Logic in Computer Science. IEEE Computer Society, Los Alamitos (2002) (invited paper)"},{"key":"18_CR33","series-title":"Foundations","volume-title":"Handbook of Graph Grammars and Computing by Graph Transformation","year":"1997","unstructured":"Rozenberg, G. (ed.): Handbook of Graph Grammars and Computing by Graph Transformation. Foundations, vol.\u00a01. World Scientific, Singapore (1997)"},{"key":"18_CR34","unstructured":"van Eekelen, M., de Mol, M.: Mixed lazy\/strict graph semantics. In: Proc. 16th International Workshop on Implementation and Application of Functional Languages, pp. 245\u2013260. Christian-Albrechts-Universitaet zu Kiel (2004)"},{"key":"18_CR35","first-page":"106","volume-title":"Proc. 5th Annual Conference of European Association for Computer Science Logic","author":"M. Eekelen van","year":"1996","unstructured":"van Eekelen, M., Smetsers, S., Plasmeijer, M.: Graph rewriting semantics for functional programming languages. In: Proc. 5th Annual Conference of European Association for Computer Science Logic, pp. 106\u2013128. Springer, Heidelberg (1996)"},{"issue":"2","key":"18_CR36","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1016\/S0167-6423(02)00036-9","volume":"44","author":"M. Wermelinger","year":"2002","unstructured":"Wermelinger, M., Fiadero, J.L.: A graph transformation approach to software architecture reconfiguration. Sci. Comput. Program.\u00a044(2), 133\u2013155 (2002)","journal-title":"Sci. Comput. Program."},{"issue":"1-2","key":"18_CR37","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1007\/s00165-007-0067-y","volume":"21","author":"L. Zhao","year":"2009","unstructured":"Zhao, L., Liu, X., Liu, Z., Qiu, Z.: Graph transformations for object-oriented refinement. Form. Asp. Comput.\u00a021(1-2), 103\u2013131 (2009)","journal-title":"Form. Asp. Comput."}],"container-title":["Lecture Notes in Computer Science","Formal Methods and Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-10373-5_18.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,24]],"date-time":"2020-11-24T02:54:53Z","timestamp":1606186493000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-10373-5_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642103728","9783642103735"],"references-count":37,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-10373-5_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2009]]}}}