{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,1]],"date-time":"2025-06-01T22:10:05Z","timestamp":1748815805359,"version":"3.41.0"},"publisher-location":"Berlin, Heidelberg","reference-count":42,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662496640"},{"type":"electronic","value":"9783662496657"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-662-49665-7_3","type":"book-chapter","created":{"date-parts":[[2016,3,21]],"date-time":"2016-03-21T08:09:42Z","timestamp":1458547782000},"page":"31-48","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["A Graph-Based Semantics Workbench for Concurrent Asynchronous Programs"],"prefix":"10.1007","author":[{"given":"Claudio","family":"Corrodi","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alexander","family":"Heu\u00dfner","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Christopher M.","family":"Poskitt","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"3_CR1","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/1086.001.0001","volume-title":"ACTORS: A Model of Concurrent Computation in Distributed Systems","author":"G Agha","year":"1986","unstructured":"Agha, G.: ACTORS: A Model of Concurrent Computation in Distributed Systems. MIT Press, Cambridge (1986)"},{"key":"3_CR2","volume-title":"Concurrent Programming in ERLANG","author":"J Armstrong","year":"1996","unstructured":"Armstrong, J., Virding, R., Williams, M.: Concurrent Programming in ERLANG, 2nd edn. Prentice Hall, Englewood Cliffs (1996)","edition":"2"},{"key":"3_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"135","DOI":"10.1007\/978-3-662-46081-8_8","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"P Backes","year":"2015","unstructured":"Backes, P., Reineke, J.: Analysis of infinite-state graph transformation systems by cluster abstraction. In: D\u2019Souza, D., Lal, A., Larsen, K.G. (eds.) VMCAI 2015. LNCS, vol. 8931, pp. 135\u2013152. Springer, Heidelberg (2015)"},{"key":"3_CR4","doi-asserted-by":"crossref","unstructured":"Bogdanas, D., Rosu, G.: K-Java: A complete semantics of Java. In: Proceedings of POPL 2015, pp. 445\u2013456. ACM (2015)","DOI":"10.1145\/2775051.2676982"},{"issue":"4","key":"3_CR5","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1007\/s00165-008-0096-1","volume":"21","author":"PJ Brooke","year":"2009","unstructured":"Brooke, P.J., Paige, R.F.: Cameo: an alternative model of concurrency for Eiffel. Formal Aspects Comput. 21(4), 363\u2013391 (2009)","journal-title":"Formal Aspects Comput."},{"issue":"4","key":"3_CR6","doi-asserted-by":"publisher","first-page":"487","DOI":"10.1007\/s00165-007-0033-8","volume":"19","author":"PJ Brooke","year":"2007","unstructured":"Brooke, P.J., Paige, R.F., Jacob, J.L.: A CSP model of Eiffel\u2019s SCOOP. Formal Aspects Comput. 19(4), 487\u2013512 (2007)","journal-title":"Formal Aspects Comput."},{"key":"3_CR7","unstructured":"Caltais, G., Meyer, B.: Coffman deadlocks in SCOOP. In: Proceedings of NWPT 2014 (2014). http:\/\/arxiv.org\/abs\/1409.7514"},{"key":"3_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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. 3256, pp. 383\u2013398. Springer, Heidelberg (2004)"},{"key":"3_CR9","doi-asserted-by":"crossref","unstructured":"Dotti, F.L., Duarte, L.M., Foss, L., Ribeiro, L., Russi, D., dos Santos, O.M.: An environment for the development of concurrent object-based applications. In: Proceedings of GraBaTs 2004. ENTCS, vol. 127, pp. 3\u201313. Elsevier (2005)","DOI":"10.1016\/j.entcs.2004.12.026"},{"key":"3_CR10","unstructured":"Downey, A.B.: The Little Book of Semaphores. http:\/\/greenteapress.com\/semaphores\/ . Accessed Jan 2016"},{"key":"3_CR11","unstructured":"Eiffel Documentation: Concurrent Eiffel with SCOOP. https:\/\/docs.eiffel.com\/book\/solutions\/concurrent-eiffel-scoop . Accessed Oct 2015"},{"key":"3_CR12","doi-asserted-by":"crossref","unstructured":"Ferreira, A.P.L., Foss, L., Ribeiro, L.: Formal verification of object-oriented graph grammars specifications. In: Proceedings of GT-VC 2006. ENTCS, vol. 175, pp. 101\u2013114. Elsevier (2007)","DOI":"10.1016\/j.entcs.2007.04.020"},{"key":"3_CR13","doi-asserted-by":"crossref","unstructured":"Ferreira, A.P.L., Ribeiro, L.: A graph-based semantics for object-oriented programming constructs. In: Proceedings of CTCS 2004. ENTCS, vol. 122, pp. 89\u2013104. Elsevier (2005)","DOI":"10.1016\/j.entcs.2004.06.053"},{"key":"3_CR14","unstructured":"Grand Central Dispatch (GCD) Reference. https:\/\/developer.apple.com\/library\/mac\/documentation\/Performance\/Reference\/GCD_libdispatch_Ref\/index.html . Accessed Oct 2015"},{"issue":"3","key":"3_CR15","doi-asserted-by":"publisher","first-page":"58","DOI":"10.1145\/2700072","volume":"14","author":"G Geeraerts","year":"2015","unstructured":"Geeraerts, G., Heu\u00dfner, A., Raskin, J.: On the verification of concurrent, asynchronous programs with waiting queues. ACM Trans. Embed. Comput. Syst. 14(3), 58 (2015)","journal-title":"ACM Trans. Embed. Comput. Syst."},{"issue":"1","key":"3_CR16","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1007\/s10009-011-0186-x","volume":"14","author":"AH Ghamarian","year":"2012","unstructured":"Ghamarian, A.H., de Mol, M., Rensink, A., Zambon, E., Zimakova, M.: Modelling and analysis using GROOVE. Int. J. Softw. Tools Technol. Transf. 14(1), 15\u201340 (2012)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"3_CR17","unstructured":"Groove (project web page). http:\/\/groove.cs.utwente.nl\/ . Accessed October 2015"},{"key":"3_CR18","doi-asserted-by":"crossref","first-page":"32","DOI":"10.4204\/EPTCS.181.3","volume":"181","author":"Alexander Heu\u00dfner","year":"2015","unstructured":"Heu\u00dfner, A., Poskitt, C.M., Corrodi, C., Morandi, B.: Towards practical graph-based verification for an object-oriented concurrency model. In: Proceedings of GaM 2015. EPTCS, vol. 181, pp. 32\u201347 (2015)","journal-title":"Electronic Proceedings in Theoretical Computer Science"},{"key":"3_CR19","doi-asserted-by":"crossref","unstructured":"Johnsen, E.B., Owe, O., Axelsen, E.W.: A run-time environment for concurrent objects with asynchronous method calls. In: Proceedings of WRLA 2004. ENTCS, vol. 117, pp. 375\u2013392. Elsevier(2005)","DOI":"10.1016\/j.entcs.2004.06.012"},{"issue":"1\u20132","key":"3_CR20","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1016\/j.tcs.2006.07.031","volume":"365","author":"EB Johnsen","year":"2006","unstructured":"Johnsen, E.B., Owe, O., Yu, I.C.: Creol: a type-safe object-oriented model for distributed concurrent systems. Theor. Comput. Sci. 365(1\u20132), 23\u201366 (2006)","journal-title":"Theor. Comput. Sci."},{"key":"3_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/978-3-642-34005-5_3","volume-title":"Rewriting Logic and Its Applications","author":"D Lucanu","year":"2012","unstructured":"Lucanu, D., \u015eerb\u0103nu\u0163\u0103, T.F., Ro\u015fu, G.: $$\\mathbb{K}$$ K framework distilled. In: Dur\u00e1n, F. (ed.) WRLA 2012. LNCS, vol. 7571, pp. 31\u201353. Springer, Heidelberg (2012)"},{"issue":"1","key":"3_CR22","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1016\/0304-3975(92)90182-F","volume":"96","author":"J Meseguer","year":"1992","unstructured":"Meseguer, J.: Conditioned rewriting logic as a united model of concurrency. Theor. Comput. Sci. 96(1), 73\u2013155 (1992)","journal-title":"Theor. Comput. Sci."},{"issue":"7\u20138","key":"3_CR23","doi-asserted-by":"publisher","first-page":"721","DOI":"10.1016\/j.jlap.2012.06.003","volume":"81","author":"J Meseguer","year":"2012","unstructured":"Meseguer, J.: Twenty years of rewriting logic. J. Logic Algebraic Program. 81(7\u20138), 721\u2013781 (2012)","journal-title":"J. Logic Algebraic Program."},{"issue":"9","key":"3_CR24","doi-asserted-by":"publisher","first-page":"56","DOI":"10.1145\/162685.162705","volume":"36","author":"B Meyer","year":"1993","unstructured":"Meyer, B.: Systematic concurrent object-oriented programming. Commun. ACM (CACM) 36(9), 56\u201380 (1993)","journal-title":"Commun. ACM (CACM)"},{"key":"3_CR25","volume-title":"Object-Oriented Software Construction","author":"B Meyer","year":"1997","unstructured":"Meyer, B.: Object-Oriented Software Construction, 2nd edn. Prentice Hall, Upper Saddle River (1997)","edition":"2"},{"key":"3_CR26","doi-asserted-by":"crossref","unstructured":"Morandi, B., Schill, M., Nanz, S., Meyer, B.: Prototyping a concurrency model. In: Proceedings of ACSD 2013, pp. 170\u2013179. IEEE (2013)","DOI":"10.1109\/ACSD.2013.21"},{"key":"3_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1007\/978-3-662-43376-8_7","volume-title":"Coordination Models and Languages","author":"B Morandi","year":"2014","unstructured":"Morandi, B., Nanz, S., Meyer, B.: Safe and efficient data sharing for message-passing concurrency. In: K\u00fchn, E., Pugliese, R. (eds.) COORDINATION 2014. LNCS, vol. 8459, pp. 99\u2013114. Springer, Heidelberg (2014)"},{"key":"3_CR28","unstructured":"Nienaltowski, P.: Practical framework for contract-based concurrent object-oriented programming. Doctoral dissertation, ETH Z\u00fcrich (2007)"},{"issue":"4","key":"3_CR29","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1007\/s00165-008-0073-8","volume":"21","author":"JS Ostroff","year":"2009","unstructured":"Ostroff, J.S., Torshizi, F.A., Huang, H.F., Schoeller, B.: Beyond contracts for concurrency. Formal Aspects Comput. 21(4), 319\u2013346 (2009)","journal-title":"Formal Aspects Comput."},{"key":"3_CR30","doi-asserted-by":"crossref","unstructured":"Park, D., \u015etef\u0103nescu, A., Ro\u015fu, G.: KJS: a complete formal semantics of JavaScript. In: Proceedings of PLDI 2015, pp. 346\u2013356. ACM (2015)","DOI":"10.1145\/2813885.2737991"},{"key":"3_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"6","DOI":"10.1007\/978-3-642-17322-6_2","volume-title":"Graph Transformations and Model-Driven Engineering","author":"A Rensink","year":"2010","unstructured":"Rensink, A.: The edge of graph transformation \u2014 graphs for behavioural specification. In: Engels, G., Lewerentz, C., Sch\u00e4fer, W., Sch\u00fcrr, A., Westfechtel, B. (eds.) Nagl Festschrift. LNCS, vol. 5765, pp. 6\u201332. Springer, Heidelberg (2010)"},{"key":"3_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1007\/978-3-642-02138-1_18","volume-title":"Formal Techniques for Distributed Systems","author":"A Rensink","year":"2009","unstructured":"Rensink, A., Zambon, E.: A type graph model for Java programs. In: Lee, D., Lopes, A., Poetzsch-Heffter, A. (eds.) FMOODS 2009. LNCS, vol. 5522, pp. 237\u2013242. Springer, Heidelberg (2009)"},{"issue":"6","key":"3_CR33","doi-asserted-by":"publisher","first-page":"397","DOI":"10.1016\/j.jlap.2010.03.012","volume":"79","author":"G Rosu","year":"2010","unstructured":"Rosu, G., Serbanuta, T.: An overview of the K semantic framework. J. Logic Algebraic Program. 79(6), 397\u2013434 (2010)","journal-title":"J. Logic Algebraic Program."},{"key":"3_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1007\/978-3-642-14107-2_13","volume-title":"ECOOP 2010 \u2013 Object-Oriented Programming","author":"J Sch\u00e4fer","year":"2010","unstructured":"Sch\u00e4fer, J., Poetzsch-Heffter, A.: JCoBox: generalizing active objects to concurrent components. In: D\u2019Hondt, T. (ed.) ECOOP 2010. LNCS, vol. 6183, pp. 275\u2013299. Springer, Heidelberg (2010)"},{"key":"3_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"294","DOI":"10.1007\/978-3-642-33654-6_20","volume-title":"Graph Transformations","author":"TF \u015eerb\u0103nu\u0163\u0103","year":"2012","unstructured":"\u015eerb\u0103nu\u0163\u0103, T.F., Ro\u015fu, G.: A truly concurrent semantics for the $$\\mathbb{K}$$ K framework based on graph transformations. In: Ehrig, H., Engels, G., Kreowski, H.-J., Rozenberg, G. (eds.) ICGT 2012. LNCS, vol. 7562, pp. 294\u2013310. Springer, Heidelberg (2012)"},{"key":"3_CR36","unstructured":"Supplementary material. http:\/\/www.swt-bamberg.de\/fase2016_supp\/"},{"key":"3_CR37","doi-asserted-by":"crossref","unstructured":"Torshizi, F.A., Ostroff, J.S., Paige, R.F., Chechik, M.: The SCOOP concurrency model in Java-like languages. In: Proceedings of CpPA 2009. Concurrent Systems Engineering Series, vol. 67, pp. 7\u201327. IOS Press (2009)","DOI":"10.3233\/978-1-60750-065-0-7"},{"key":"3_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"382","DOI":"10.1007\/978-3-642-24690-6_26","volume-title":"Software Engineering and Formal Methods","author":"J Tschannen","year":"2011","unstructured":"Tschannen, J., Furia, C.A., Nordio, M., Meyer, B.: Usable verification of object-oriented programs by combining static and dynamic techniques. In: Barthe, G., Pardo, A., Schneider, G. (eds.) SEFM 2011. LNCS, vol. 7041, pp. 382\u2013398. Springer, Heidelberg (2011)"},{"key":"3_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"597","DOI":"10.1007\/978-3-642-16901-4_39","volume-title":"Formal Methods and Software Engineering","author":"S West","year":"2010","unstructured":"West, S., Nanz, S., Meyer, B.: A modular scheme for deadlock prevention in an object-oriented programming model. In: Dong, J.S., Zhu, H. (eds.) ICFEM 2010. LNCS, vol. 6447, pp. 597\u2013612. Springer, Heidelberg (2010)"},{"key":"3_CR40","doi-asserted-by":"crossref","unstructured":"West, S., Nanz, S., Meyer, B.: Efficient and reasonable object-oriented concurrency. In: Proceedings of ESEC\/FSE 2015, pp. 734\u2013744. ACM (2015)","DOI":"10.1145\/2688500.2688545"},{"key":"3_CR41","doi-asserted-by":"crossref","unstructured":"Zambon, E., Rensink, A.: Using graph transformations and graph abstractions for software verification. In: Proceedings of ICGT-DS 2010. ECEASST, vol. 38 (2011)","DOI":"10.1007\/978-3-642-15928-2_37"},{"key":"3_CR42","unstructured":"Zambon, E., Rensink, A.: Solving the N-Queens problem with GROOVE - towards a compendium of best practices. In: Proceedings of GT-VMT 2014. ECEASST, vol. 67 (2014)"}],"container-title":["Lecture Notes in Computer Science","Fundamental Approaches to Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-49665-7_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,1]],"date-time":"2025-06-01T21:29:22Z","timestamp":1748813362000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-49665-7_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783662496640","9783662496657"],"references-count":42,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-49665-7_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]},"assertion":[{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}