{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,1]],"date-time":"2026-02-01T20:19:25Z","timestamp":1769977165831,"version":"3.49.0"},"publisher-location":"Cham","reference-count":31,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030171261","type":"print"},{"value":"9783030171278","type":"electronic"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2019,4,5]],"date-time":"2019-04-05T00:00:00Z","timestamp":1554422400000},"content-version":"vor","delay-in-days":94,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>The paper develops an abstract (over-approximating) semantics for double-pushout rewriting of graphs and graph-like objects. The focus is on the so-called materialization of left-hand sides from abstract graphs, a central concept in previous work. The first contribution is an accessible, general explanation of how materializations arise from universal properties and categorical constructions, in particular partial map classifiers, in a topos. Second, we introduce an extension by enriching objects with annotations and give a precise characterization of strongest post-conditions, which are effectively computable under certain assumptions.<\/jats:p>","DOI":"10.1007\/978-3-030-17127-8_10","type":"book-chapter","created":{"date-parts":[[2019,4,5]],"date-time":"2019-04-05T11:11:46Z","timestamp":1554462706000},"page":"169-188","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Rewriting Abstract Structures: Materialization Explained Categorically"],"prefix":"10.1007","author":[{"given":"Andrea","family":"Corradini","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tobias","family":"Heindel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Barbara","family":"K\u00f6nig","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Dennis","family":"Nolte","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Arend","family":"Rensink","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2019,4,5]]},"reference":[{"key":"10_CR1","unstructured":"Backes, P.: Cluster abstraction of graph transformation systems. Ph.D. thesis, Saarland University (2015)"},{"key":"10_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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). https:\/\/doi.org\/10.1007\/978-3-662-46081-8_8"},{"key":"10_CR3","doi-asserted-by":"crossref","unstructured":"Bauer, J.: Analysis of communication topologies by partner abstraction. Ph.D. thesis, Saarland University (2006)","DOI":"10.1007\/978-3-540-74061-2_16"},{"key":"10_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1007\/978-3-540-74061-2_16","volume-title":"Static Analysis","author":"J Bauer","year":"2007","unstructured":"Bauer, J., Wilhelm, R.: Static analysis of dynamic communication systems by partner abstraction. In: Nielson, H.R., Fil\u00e9, G. (eds.) SAS 2007. LNCS, vol. 4634, pp. 249\u2013264. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-74061-2_16"},{"issue":"6","key":"10_CR5","doi-asserted-by":"publisher","first-page":"26:1","DOI":"10.1145\/2049697.2049700","volume":"58","author":"C Calcagno","year":"2011","unstructured":"Calcagno, C., Distefano, D., O\u2019Hearn, P.W., Yang, H.: Compositional shape analysis by means of bi-abduction. J. ACM 58(6), 26:1\u201326:66 (2011)","journal-title":"J. ACM"},{"key":"10_CR6","doi-asserted-by":"crossref","unstructured":"Chang, B.-Y.E., Rival, X.: Relational inductive shape analysis. In: Proceedings of POPL 2008, pp. 247\u2013260. ACM (2008)","DOI":"10.1145\/1328438.1328469"},{"key":"10_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"30","DOI":"10.1007\/11841883_4","volume-title":"Graph Transformations","author":"A Corradini","year":"2006","unstructured":"Corradini, A., Heindel, T., Hermann, F., K\u00f6nig, B.: Sesqui-pushout rewriting. In: Corradini, A., Ehrig, H., Montanari, U., Ribeiro, L., Rozenberg, G. (eds.) ICGT 2006. LNCS, vol. 4178, pp. 30\u201345. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11841883_4"},{"key":"10_CR8","doi-asserted-by":"crossref","unstructured":"Corradini, A., Heindel, T., K\u00f6nig, B., Nolte, D., Rensink, A.: Rewriting abstract structures: materialization explained categorically (2019). arXiv:1902.04809","DOI":"10.1007\/978-3-030-17127-8_10"},{"key":"10_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1007\/978-3-319-61470-0_5","volume-title":"Graph Transformation","author":"A Corradini","year":"2017","unstructured":"Corradini, A., K\u00f6nig, B., Nolte, D.: Specifying graph languages with type graphs. In: de Lara, J., Plump, D. (eds.) ICGT 2017. LNCS, vol. 10373, pp. 73\u201389. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-61470-0_5"},{"key":"10_CR10","unstructured":"Corradini, A., K\u00f6nig, B., Nolte, D.: Specifying graph languages with type graphs. J. Log. Algebraic Methods Program. (to appear)"},{"key":"10_CR11","doi-asserted-by":"crossref","unstructured":"Corradini, A., Montanari, U., Rossi, F., Ehrig, H., Heckel, R., L\u00f6we, M.: Algebraic approaches to graph transformation\u2013part I: basic concepts and double pushout approach, Chap. 3. In: Rozenberg, G. (ed.) Handbook of Graph Grammars and Computing by Graph Transformation: Foundations, vol. 1. World Scientific (1997)","DOI":"10.1142\/9789812384720_0003"},{"issue":"2","key":"10_CR12","doi-asserted-by":"publisher","first-page":"324","DOI":"10.1145\/234528.234740","volume":"28","author":"P Cousot","year":"1996","unstructured":"Cousot, P.: Abstract interpretation. ACM Comput. Surv. 28(2), 324\u2013328 (1996). https:\/\/dl.acm.org\/citation.cfm?id=234740","journal-title":"ACM Comput. Surv."},{"issue":"1\u20132","key":"10_CR13","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1016\/0022-4049(87)90124-1","volume":"49","author":"R Dyckhoff","year":"1987","unstructured":"Dyckhoff, R., Tholen, W.: Exponentiable morphisms, partial products and pullback complements. J. Pure Appl. Algebra 49(1\u20132), 103\u2013116 (1987)","journal-title":"J. Pure Appl. Algebra"},{"issue":"102","key":"10_CR14","first-page":"111","volume":"3","author":"H Ehrig","year":"2013","unstructured":"Ehrig, H., Golas, U., Hermann, F., et al.: Categorical frameworks for graph transformation and HLR systems based on the DPO approach. Bull. EATCS 3(102), 111\u2013121 (2013)","journal-title":"Bull. EATCS"},{"key":"10_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"144","DOI":"10.1007\/978-3-540-30203-2_12","volume-title":"Graph Transformations","author":"H Ehrig","year":"2004","unstructured":"Ehrig, H., Habel, A., Padberg, J., Prange, U.: Adhesive high-level replacement categories and systems. In: Ehrig, H., Engels, G., Parisi-Presicce, F., Rozenberg, G. (eds.) ICGT 2004. LNCS, vol. 3256, pp. 144\u2013160. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-30203-2_12"},{"key":"10_CR16","doi-asserted-by":"crossref","unstructured":"Ehrig, H., Pfender, M., Schneider, H.J.: Graph-grammars: an algebraic approach. In: 14th Annual Symposium on Switching and Automata Theory, Iowa City, Iowa, USA, 15\u201317 October 1973, pp. 167\u2013180 (1973)","DOI":"10.1109\/SWAT.1973.11"},{"issue":"1","key":"10_CR17","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1017\/S0004972700044828","volume":"7","author":"P Freyd","year":"1972","unstructured":"Freyd, P.: Aspects of topoi. Bull. Aust. Math. Soc. 7(1), 1\u201376 (1972)","journal-title":"Bull. Aust. Math. Soc."},{"key":"10_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1007\/978-3-540-31847-7_17","volume-title":"Formal Methods in Software and Systems Modeling","author":"A Habel","year":"2005","unstructured":"Habel, A., Pennemann, K.-H.: Nested constraints and application conditions for high-level structures. In: Kreowski, H.-J., Montanari, U., Orejas, F., Rozenberg, G., Taentzer, G. (eds.) Formal Methods in Software and Systems Modeling. LNCS, vol. 3393, pp. 293\u2013308. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/978-3-540-31847-7_17"},{"key":"10_CR19","series-title":"Studies in Logic and the Foundation of Mathematics","volume-title":"Categorical Logic and Type Theory","author":"B Jacobs","year":"1999","unstructured":"Jacobs, B.: Categorical Logic and Type Theory. Studies in Logic and the Foundation of Mathematics, vol. 141. Elsevier, Amsterdam (1999)"},{"key":"10_CR20","unstructured":"K\u00f6nig, B.: Description and verification of mobile processes with graph rewriting techniques. Ph.D. thesis, Technische Universit\u00e4t M\u00fcnchen (1999)"},{"issue":"3","key":"10_CR21","doi-asserted-by":"publisher","first-page":"511","DOI":"10.1051\/ita:2005028","volume":"39","author":"S Lack","year":"2005","unstructured":"Lack, S., Soboci\u0144ski, P.: Adhesive and quasiadhesive categories. RAIRO - Theor. Inform. Appl. 39(3), 511\u2013545 (2005)","journal-title":"RAIRO - Theor. Inform. Appl."},{"key":"10_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"184","DOI":"10.1007\/11841883_14","volume-title":"Graph Transformations","author":"S Lack","year":"2006","unstructured":"Lack, S., Soboci\u0144ski, P.: Toposes are adhesive. In: Corradini, A., Ehrig, H., Montanari, U., Ribeiro, L., Rozenberg, G. (eds.) ICGT 2006. LNCS, vol. 4178, pp. 184\u2013198. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11841883_14"},{"key":"10_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1007\/978-3-319-09108-2_2","volume-title":"Graph Transformation","author":"L Lambers","year":"2014","unstructured":"Lambers, L., Orejas, F.: Tableau-based reasoning for graph properties. In: Giese, H., K\u00f6nig, B. (eds.) ICGT 2014. LNCS, vol. 8571, pp. 17\u201332. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-09108-2_2"},{"key":"10_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"90","DOI":"10.1007\/978-3-662-48288-9_6","volume-title":"Static Analysis","author":"H Li","year":"2015","unstructured":"Li, H., Rival, X., Chang, B.-Y.E.: Shape analysis for unstructured sharing. In: Blazy, S., Jensen, T. (eds.) SAS 2015. LNCS, vol. 9291, pp. 90\u2013108. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-48288-9_6"},{"key":"10_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"218","DOI":"10.1007\/978-3-642-15928-2_15","volume-title":"Graph Transformations","author":"M L\u00f6we","year":"2010","unstructured":"L\u00f6we, M.: Graph rewriting in span-categories. In: Ehrig, H., Rensink, A., Rozenberg, G., Sch\u00fcrr, A. (eds.) ICGT 2010. LNCS, vol. 6372, pp. 218\u2013233. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-15928-2_15"},{"key":"10_CR26","unstructured":"O\u2019Hearn, P.W.: A primer on separation logic (and automatic program verification and analysis). In: Software Safety and Security: Tools for Analysis and Verification. NATO Science for Peace and Security Series, vol. 33, pp. 286\u2013318 (2012)"},{"key":"10_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"401","DOI":"10.1007\/978-3-540-24725-8_28","volume-title":"Programming Languages and Systems","author":"A Rensink","year":"2004","unstructured":"Rensink, A.: Canonical graph shapes. In: Schmidt, D. (ed.) ESOP 2004. LNCS, vol. 2986, pp. 401\u2013415. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-24725-8_28"},{"key":"10_CR28","unstructured":"Rensink, A., Zambon, E.: Neighbourhood abstraction in GROOVE. In: Proceedings of GraBaTs 2010 (Workshop on Graph-Based Tools). Electronic Communications of the EASST, vol. 32 (2010)"},{"key":"10_CR29","volume-title":"Handbook of Graph Grammars and Computing by Graph Transformation: Foundations","year":"1997","unstructured":"Rozenberg, G. (ed.): Handbook of Graph Grammars and Computing by Graph Transformation: Foundations, vol. 1. World Scientific, Singapore (1997)"},{"issue":"3","key":"10_CR30","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1145\/514188.514190","volume":"24","author":"M Sagiv","year":"2002","unstructured":"Sagiv, M., Reps, T., Wilhelm, R.: Parametric shape analysis via 3-valued logic. TOPLAS (ACM Trans. Program. Lang. Syst.) 24(3), 217\u2013298 (2002)","journal-title":"TOPLAS (ACM Trans. Program. Lang. Syst.)"},{"key":"10_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"92","DOI":"10.1007\/978-3-642-25032-3_7","volume-title":"Formal Methods, Foundations and Applications","author":"D Steenken","year":"2011","unstructured":"Steenken, D., Wehrheim, H., Wonisch, D.: Sound and complete abstract graph transformation. In: Simao, A., Morgan, C. (eds.) SBMF 2011. LNCS, vol. 7021, pp. 92\u2013107. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-25032-3_7"}],"container-title":["Lecture Notes in Computer Science","Foundations of Software Science and Computation Structures"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-17127-8_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,9,5]],"date-time":"2025-09-05T17:04:57Z","timestamp":1757091897000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-17127-8_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030171261","9783030171278"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-17127-8_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"5 April 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FoSSaCS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Foundations of Software Science and Computation Structures","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Prague","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Czech Republic","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8 April 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 April 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fossacs2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.etaps.org\/2019\/fossacs","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}