{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,1]],"date-time":"2026-02-01T18:00:22Z","timestamp":1769968822733,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642250316","type":"print"},{"value":"9783642250323","type":"electronic"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2011]]},"DOI":"10.1007\/978-3-642-25032-3_7","type":"book-chapter","created":{"date-parts":[[2011,11,8]],"date-time":"2011-11-08T20:27:53Z","timestamp":1320784073000},"page":"92-107","source":"Crossref","is-referenced-by-count":8,"title":["Sound and Complete Abstract Graph Transformation"],"prefix":"10.1007","author":[{"given":"Dominik","family":"Steenken","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Heike","family":"Wehrheim","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Daniel","family":"Wonisch","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"7","key":"7_CR1","doi-asserted-by":"publisher","first-page":"869","DOI":"10.1016\/j.ic.2008.04.002","volume":"206","author":"P. Baldan","year":"2008","unstructured":"Baldan, P., Corradini, A., K\u00f6nig, B.: A framework for the verification of infinite-state graph transformation systems. Information and Computation\u00a0206(7), 869\u2013907 (2008)","journal-title":"Information and Computation"},{"key":"7_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"268","DOI":"10.1007\/3-540-45319-9_19","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T. Ball","year":"2001","unstructured":"Ball, T., Podelski, A., Rajamani, S.: Boolean and cartesian abstraction for model checking c programs. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol.\u00a02031, pp. 268\u2013283. Springer, Heidelberg (2001)"},{"key":"7_CR3","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: Riis Nielson, H., Fil\u00e9, G. (eds.) SAS 2007. LNCS, vol.\u00a04634, pp. 249\u2013264. Springer, Heidelberg (2007)"},{"key":"7_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1007\/978-3-540-87405-8_22","volume-title":"Graph Transformations","author":"J. Bauer","year":"2008","unstructured":"Bauer, J., Boneva, I., Kurb\u00e1n, M., Rensink, A.: A modal-logic based graph abstraction. In: Ehrig, H., Heckel, R., Rozenberg, G., Taentzer, G. (eds.) ICGT 2008. LNCS, vol.\u00a05214, pp. 321\u2013335. Springer, Heidelberg (2008)"},{"key":"7_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"347","DOI":"10.1007\/978-3-540-78743-3_26","volume-title":"Fundamental Approaches to Software Engineering","author":"D. Bisztray","year":"2008","unstructured":"Bisztray, D., Heckel, R., Ehrig, H.: Verification of architectural refactorings by rule extraction. In: Fiadeiro, J.L., Inverardi, P. (eds.) FASE 2008. LNCS, vol.\u00a04961, pp. 347\u2013361. Springer, Heidelberg (2008)"},{"key":"7_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1007\/978-3-540-73368-3_25","volume-title":"Computer Aided Verification","author":"I. Bogudlov","year":"2007","unstructured":"Bogudlov, I., Lev-Ami, T., Reps, T., Sagiv, M.: Revamping TVLA: making parametric shape analysis competitive. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 221\u2013225. Springer, Heidelberg (2007)"},{"key":"7_CR7","first-page":"269","volume-title":"Proceedings of the 6th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, POPL 1979","author":"P. Cousot","year":"1979","unstructured":"Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: Proceedings of the 6th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, POPL 1979, pp. 269\u2013282. ACM, New York (1979)"},{"key":"7_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1007\/978-3-540-89020-1_2","volume-title":"Applications of Graph Transformations with Industrial Relevance","author":"G. Engels","year":"2008","unstructured":"Engels, G., G\u00fcldali, B., Soltenborn, C., Wehrheim, H.: Assuring consistency of business process models and web services using visual contracts. In: Sch\u00fcrr, A., Nagl, M., Z\u00fcndorf, A. (eds.) AGTIVE 2007. LNCS, vol.\u00a05088, pp. 17\u201331. Springer, Heidelberg (2008)"},{"key":"7_CR9","doi-asserted-by":"crossref","first-page":"113","DOI":"10.3233\/FI-1994-201234","volume":"20","author":"M. Fitting","year":"1994","unstructured":"Fitting, M.: Kleene\u2019s three valued logics and their children. FI\u00a020, 113\u2013131 (1994)","journal-title":"FI"},{"key":"7_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1007\/3-540-63166-6_10","volume-title":"Computer Aided Verification","author":"S. Graf","year":"1997","unstructured":"Graf, S., Saidi, H.: Construction of abstract state graphs with pvs. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, pp. 72\u201383. Springer, Heidelberg (1997)"},{"key":"7_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1007\/978-3-642-16265-7_14","volume-title":"Integrated Formal Methods","author":"M. H\u00fclsbusch","year":"2010","unstructured":"H\u00fclsbusch, M., K\u00f6nig, B., Rensink, A., Semenyak, M., Soltenborn, C., Wehrheim, H.: Showing full semantics preservation in model transformation - a comparison of techniques. In: M\u00e9ry, D., Merz, S. (eds.) IFM 2010. LNCS, vol.\u00a06396, pp. 183\u2013198. Springer, Heidelberg (2010)"},{"key":"7_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"152","DOI":"10.1007\/11817963_16","volume-title":"Computer Aided Verification","author":"S. Jha","year":"2006","unstructured":"Jha, S., Lu, Y., Grumberg, O., Clarke, E., Veith, H.: Counterexample-guided Abstraction Refinement. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 152\u2013165. Springer, Heidelberg (2006)"},{"issue":"1-2","key":"7_CR13","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1016\/0304-3975(93)90068-5","volume":"109","author":"M. L\u00f6we","year":"1993","unstructured":"L\u00f6we, M.: Algebraic approach to single-pushout graph transformation. Theoretical Computer Science\u00a0109(1-2), 181\u2013224 (1993)","journal-title":"Theoretical Computer Science"},{"key":"7_CR14","doi-asserted-by":"crossref","unstructured":"Rensink, A.: The GROOVE simulator: A tool for state space generation. Applications of Graph Transformations with Industrial Relevance, 479\u2013485 (2004)","DOI":"10.1007\/978-3-540-25959-6_40"},{"issue":"1","key":"7_CR15","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1016\/j.entcs.2006.01.022","volume":"157","author":"A. Rensink","year":"2006","unstructured":"Rensink, A., Distefano, D.: Abstract graph transformation. Electr. Notes Theor. Comput. Sci.\u00a0157(1), 39\u201359 (2006)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"7_CR16","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1145\/1749608.1749613","volume":"32","author":"T. Reps","year":"2010","unstructured":"Reps, T., Sagiv, M., Loginov, A.: Finite differencing of logical formulas for static analysis. ACM Trans. Program. Lang. Syst.\u00a032, 24:1\u201324:55 (2010)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"7_CR17","series-title":"Lecture Notes in Computer Science","first-page":"3","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"T. Reps","year":"2004","unstructured":"Reps, T., Sagiv, M., Yorsh, G.: Symbolic implementation of the best transformer. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol.\u00a02937, pp. 3\u201325. Springer, Heidelberg (2004)"},{"key":"7_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"252","DOI":"10.1007\/978-3-540-24622-0_21","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"T.W. Reps","year":"2004","unstructured":"Reps, T.W., Sagiv, S., Yorsh, G.: Symbolic implementation of the best transformer. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol.\u00a02937, pp. 252\u2013266. Springer, Heidelberg (2004)"},{"issue":"3","key":"7_CR19","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1145\/514188.514190","volume":"24","author":"S. Sagiv","year":"2002","unstructured":"Sagiv, S., Reps, T.W., Wilhelm, R.: Parametric shape analysis via 3-valued logic. ACM Trans. Program. Lang. Syst.\u00a024(3), 217\u2013298 (2002)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"7_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"18","DOI":"10.1007\/978-3-540-78800-3_3","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M. Saksena","year":"2008","unstructured":"Saksena, M., Wibling, O., Jonsson, B.: Graph grammar modeling and verification of ad hoc routing protocols. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 18\u201332. Springer, Heidelberg (2008)"},{"key":"7_CR21","unstructured":"Steenken, D., Wehrheim, H., Wonisch, D.: Towards a shape analysis for graph transformation systems. In: Proceedings of the 22nd Nordic Workshop on Programming Theory (2010), Technical Report, http:\/\/www.cs.uni-paderborn.de\/fileadmin\/Informatik\/AG-Wehrheim\/Personen\/Dominik_Steenken\/ShapeAnalysis2010TR.pdf"},{"key":"7_CR22","unstructured":"Wonisch, D.: Increasing the preciseness of shape analysis for graph transformation systems. Master\u2019s thesis, University of Paderborn (August 2010)"},{"key":"7_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"530","DOI":"10.1007\/978-3-540-24730-2_39","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"G. Yorsh","year":"2004","unstructured":"Yorsh, G., Reps, T., Sagiv, M.: Symbolically computing most-precise abstract operations for shape analysis. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol.\u00a02988, pp. 530\u2013545. Springer, Heidelberg (2004)"},{"key":"7_CR24","doi-asserted-by":"crossref","unstructured":"Yorsh, G., Reps, T., Sagiv, M., Wilhelm, R.: Logical characterizations of heap abstractions. ACM Trans. Comput. Logic\u00a08 (January 2007)","DOI":"10.1145\/1182613.1182618"}],"container-title":["Lecture Notes in Computer Science","Formal Methods, Foundations and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-25032-3_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,6,27]],"date-time":"2020-06-27T03:56:40Z","timestamp":1593230200000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-25032-3_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642250316","9783642250323"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-25032-3_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011]]}}}