{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,21]],"date-time":"2025-05-21T06:12:35Z","timestamp":1747807955617,"version":"3.40.4"},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642341755"},{"type":"electronic","value":"9783642341762"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-34176-2_15","type":"book-chapter","created":{"date-parts":[[2012,10,1]],"date-time":"2012-10-01T05:56:59Z","timestamp":1349071019000},"page":"169-181","source":"Crossref","is-referenced-by-count":2,"title":["Locality in Reasoning about Graph Transformations"],"prefix":"10.1007","author":[{"given":"Martin","family":"Strecker","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"15_CR1","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1109\/ICST.2010.42","volume-title":"Proc. of the 3rd International Conference on Software Testing, Verification, and Validation","author":"M. Asztalos","year":"2010","unstructured":"Asztalos, M., Lengyel, L., Levendovszky, T.: Towards automated, formal verification of model transformations. In: Proc. of the 3rd International Conference on Software Testing, Verification, and Validation, pp. 15\u201324. IEEE Computer Society, Los Alamitos (2010)"},{"key":"15_CR2","unstructured":"Baldan, P., Corradini, A., Esparza, J., Heindel, T., K\u00f6nig, B., Kozioura, V.: Verifying red-black trees. In: Proc. of Concurrent Systems with Dynamic Allocated Heaps, COSMICAH 2005 (2005); Proceedings available as report RR-05-04 (Queen Mary, University of London)"},{"issue":"7","key":"15_CR3","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":"15_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/978-3-540-30538-5_9","volume-title":"FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science","author":"J. Berdine","year":"2004","unstructured":"Berdine, J., Calcagno, C., O\u2019Hearn, P.: A decidable fragment of separation logic. In: Lodaya, K., Mahajan, M. (eds.) FSTTCS 2004. LNCS, vol.\u00a03328, pp. 97\u2013109. Springer, Heidelberg (2004)"},{"issue":"4","key":"15_CR5","doi-asserted-by":"publisher","first-page":"373","DOI":"10.3166\/jancl.18.373-411","volume":"18","author":"R. Caferra","year":"2008","unstructured":"Caferra, R., Echahed, R., Peltier, N.: A term-graph clausal logic: Completeness and incompleteness results. Journal of Applied Non-classical Logics\u00a018(4), 373\u2013411 (2008)","journal-title":"Journal of Applied Non-classical Logics"},{"key":"15_CR6","doi-asserted-by":"crossref","unstructured":"da Costa, S.A., Ribeiro, L.: Formal verification of graph grammars using mathematical induction. In: Proc. of the 11th Brazilian Symposium on Formal Methods (SBMF 2008). ENTCS, vol.\u00a0240, pp. 43\u201360. Elsevier (2009)","DOI":"10.1016\/j.entcs.2009.05.044"},{"key":"15_CR7","unstructured":"Dodds, M.: Graph Transformation and Pointer Structures. Ph.D. thesis, University of York (2008)"},{"key":"15_CR8","unstructured":"Ghamarian, A.H., de Mol, M.J., Rensink, A., Zambon, E., Zimakova, M.V.: Modelling and analysis using GROOVE. Tech. Rep. TR-CTIT-10-18, Centre for Telematics and Information Technology, University of Twente, Enschede (2010)"},{"issue":"02","key":"15_CR9","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1017\/S0960129508007202","volume":"19","author":"A. Habel","year":"2009","unstructured":"Habel, A., Pennemann, K.H.: Correctness of high-level transformation systems relative to nested conditions. Mathematical Structures in Computer Science\u00a019(02), 245\u2013296 (2009)","journal-title":"Mathematical Structures in Computer Science"},{"key":"15_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"160","DOI":"10.1007\/978-3-540-30124-0_15","volume-title":"Computer Science Logic","author":"N. Immerman","year":"2004","unstructured":"Immerman, N., Rabinovich, A., Reps, T., Sagiv, M., Yorsh, G.: The Boundary Between Decidability and Undecidability for Transitive-Closure Logics. In: Marcinkowski, J., Tarlecki, A. (eds.) CSL 2004. LNCS, vol.\u00a03210, pp. 160\u2013174. Springer, Heidelberg (2004)"},{"key":"15_CR11","unstructured":"Kastenberg, H.: Graph-Based Software Specification and Verification. Ph.D. thesis, University of Twente (2008), http:\/\/eprints.eemcs.utwente.nl\/13615\/"},{"key":"15_CR12","doi-asserted-by":"crossref","unstructured":"K\u00f6nig, B., Kozioura, V.: Augur\u00a02 \u2013 A new version of a tool for the analysis of graph transformation systems. In: Proc. of the 5th Int. Workshop on Graph Transformation and Visual Modeling Techniques. ENTCS, vol.\u00a0211, pp. 201\u2013210. Elsevier (2008)","DOI":"10.1016\/j.entcs.2008.04.042"},{"key":"15_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"476","DOI":"10.1007\/11513988_47","volume-title":"Computer Aided Verification","author":"S. McPeak","year":"2005","unstructured":"McPeak, S., Necula, G.C.: Data Structure Specifications via Local Equality Axioms. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 476\u2013490. Springer, Heidelberg (2005)"},{"key":"15_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL. A Proof Assistant for Higher-Order Logic","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL. LNCS, vol.\u00a02283. Springer, Heidelberg (2002)"},{"key":"15_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"289","DOI":"10.1007\/978-3-540-87405-8_20","volume-title":"Graph Transformations","author":"K.H. Pennemann","year":"2008","unstructured":"Pennemann, K.H.: Resolution-Like Theorem Proving for High-Level Conditions. In: Ehrig, H., Heckel, R., Rozenberg, G., Taentzer, G. (eds.) ICGT 2008. LNCS, vol.\u00a05214, pp. 289\u2013304. Springer, Heidelberg (2008)"},{"key":"15_CR16","doi-asserted-by":"crossref","unstructured":"Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: Proc. of the 17th Annual IEEE Symposium on Logic in Computer Science, pp. 55\u201374. IEEE Computer Society (2002)","DOI":"10.1109\/LICS.2002.1029817"},{"key":"15_CR17","unstructured":"Ribeiro, L., Dotti, F.L., da Costa, S.A., Dillenburg, F.C.: Towards theorem proving graph grammars using Event-B. In: Ermel, C., Ehrig, H., Orejas, F., Taentzer, G. (eds.) Proc. of the International Colloquium on Graph and Model Transformation 2010. ECEASST, vol.\u00a030 (2010)"},{"key":"15_CR18","doi-asserted-by":"crossref","unstructured":"Strecker, M.: Modeling and verifying graph transformations in proof assistants. In: Mackie, I., Plump, D. (eds.) International Workshop on Computing with Terms and Graphs. ENTCS, vol.\u00a0203, pp. 135\u2013148. Elsevier (2008)","DOI":"10.1016\/j.entcs.2008.03.039"},{"issue":"3","key":"15_CR19","doi-asserted-by":"publisher","first-page":"214","DOI":"10.1016\/j.scico.2007.05.004","volume":"68","author":"D. Varr\u00f3","year":"2007","unstructured":"Varr\u00f3, D., Balogh, A.: The model transformation language of the VIATRA2 framework. Science of Computer Programming\u00a068(3), 214\u2013234 (2007)","journal-title":"Science of Computer Programming"},{"issue":"1-2","key":"15_CR20","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1016\/j.jlap.2006.12.001","volume":"73","author":"G. Yorsh","year":"2007","unstructured":"Yorsh, G., Rabinovich, A.M., Sagiv, M., Meyer, A., Bouajjani, A.: A logic of reachable patterns in linked data-structures. The Journal of Logic and Algebraic Programming\u00a073(1-2), 111\u2013142 (2007)","journal-title":"The Journal of Logic and Algebraic Programming"}],"container-title":["Lecture Notes in Computer Science","Applications of Graph Transformations with Industrial Relevance"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-34176-2_15.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,9]],"date-time":"2025-04-09T20:51:14Z","timestamp":1744231874000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-34176-2_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642341755","9783642341762"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-34176-2_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}