{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,26]],"date-time":"2026-08-26T02:03:16Z","timestamp":1787709796329,"version":"build-2784847793"},"publisher-location":"Berlin, Heidelberg","reference-count":31,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642385919","type":"print"},{"value":"9783642385926","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-38592-6_13","type":"book-chapter","created":{"date-parts":[[2013,5,29]],"date-time":"2013-05-29T04:56:11Z","timestamp":1369803371000},"page":"178-192","source":"Crossref","is-referenced-by-count":9,"title":["Bounded Model Checking of Graph Transformation Systems via SMT Solving"],"prefix":"10.1007","author":[{"given":"Tobias","family":"Isenberg","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Dominik","family":"Steenken","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Heike","family":"Wehrheim","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"13_CR1","unstructured":"Backes, P., Reineke, J.: A graph transformation case study for the topology analysis of dynamic communication system. In: Transformation Tool Contest 2010. CTIT Workshop Proceedings, vol.\u00a0WP10-03, pp. 107\u2013118. University of Twente (2010)"},{"key":"13_CR2","unstructured":"Baldan, P., K\u00f6nig, B., Rensink, A.: Summary 2: Graph grammar verification through abstraction. In: K\u00f6nig, B., Montanari, U., Gardner, P. (eds.) Graph Transformations and Process Algebras for Modeling Distributed and Mobile Systems. Dagstuhl Seminar Proceedings, vol. 04241 (2004)"},{"key":"13_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"306","DOI":"10.1007\/11841883_22","volume-title":"Graph Transformations","author":"L. Baresi","year":"2006","unstructured":"Baresi, L., Spoletini, P.: On the use of Alloy to analyze graph transformation systems. In: Corradini, A., Ehrig, H., Montanari, U., Ribeiro, L., Rozenberg, G. (eds.) ICGT 2006. LNCS, vol.\u00a04178, pp. 306\u2013320. Springer, Heidelberg (2006)"},{"key":"13_CR4","unstructured":"Barrett, C., Deters, M., de Moura, L., Oliveras, A., Stump, A.: 6 Years of SMT-COMP. Journal of Automated Reasoning, 1\u201335 (2012), 10.1007\/s10817-012-9246-5"},{"key":"13_CR5","unstructured":"Barrett, C., Stump, A., Tinelli, C.: The SMT-LIB Standard: Version 2.0. In: Gupta, A., Kroening, D. (eds.) Proceedings of the 8th International Workshop on Satisfiability Modulo Theories, Edinburgh, UK (2010)"},{"key":"13_CR6","doi-asserted-by":"crossref","unstructured":"Becker, B., Beyer, D., Giese, H., Klein, F., Schilling, D.: Symbolic invariant verification for systems with dynamic structural adaptation. In: Osterweil, L.J., Rombach, H.D., Soffa, M.L. (eds.) ICSE, pp. 72\u201381. ACM (2006)","DOI":"10.1145\/1134285.1134297"},{"key":"13_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"561","DOI":"10.1007\/978-3-642-20401-2_27","volume-title":"Rigorous Software Engineering for Service-Oriented Systems","author":"G. Bergmann","year":"2011","unstructured":"Bergmann, G., Boronat, A., Heckel, R., Torrini, P., R\u00e1th, I., Varr\u00f3, D.: Advances in model transformations by graph transformation: Specification, execution and analysis. In: Wirsing, M., H\u00f6lzl, M. (eds.) SENSORIA. LNCS, vol.\u00a06582, pp. 561\u2013584. Springer, Heidelberg (2011)"},{"key":"13_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/3-540-49059-0_14","volume-title":"Tools and Algorithms for the Construction of Analysis of Systems","author":"A. Biere","year":"1999","unstructured":"Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without bDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol.\u00a01579, pp. 193\u2013207. Springer, Heidelberg (1999)"},{"key":"13_CR9","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":"13_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/978-3-642-02959-2_12","volume-title":"Automated Deduction \u2013 CADE-22","author":"T. Bouton","year":"2009","unstructured":"Bouton, T., Caminha B. de Oliveira, D., D\u00e9harbe, D., Fontaine, P.: veriT: An open, trustable and efficient smt-solver. In: Schmidt, R.A. (ed.) CADE 2009. LNCS, vol.\u00a05663, pp. 151\u2013156. Springer, Heidelberg (2009)"},{"key":"13_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"248","DOI":"10.1007\/978-3-642-31759-0_19","volume-title":"Model Checking Software","author":"J. Christ","year":"2012","unstructured":"Christ, J., Hoenicke, J., Nutz, A.: SMTInterpol: An Interpolating SMT Solver. In: Donaldson, A., Parker, D. (eds.) SPIN 2012. LNCS, vol.\u00a07385, pp. 248\u2013254. Springer, Heidelberg (2012)"},{"key":"13_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/978-3-642-36742-7_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Cimatti","year":"2013","unstructured":"Cimatti, A., Griggio, A., Schaafsma, B.J., Sebastiani, R.: The MathSAT5 SMT Solver. In: Piterman, N., Smolka, S. (eds.) TACAS 2013. LNCS, vol.\u00a07795, pp. 93\u2013107. Springer, Heidelberg (2013)"},{"key":"13_CR13","doi-asserted-by":"crossref","unstructured":"Ehrig, H., Heckel, R., Korff, M., L\u00f6we, M., Ribeiro, L., Wagner, A., Corradini, A.: Algebraic Approaches to Graph Transformation - Part II: Single Pushout Approach and Comparison with Double Pushout Approach. In: Rozenberg, G. (ed.) Handbook of Graph Grammars, pp. 247\u2013312. World Scientific (1997)","DOI":"10.1142\/9789812384720_0004"},{"key":"13_CR14","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)"},{"issue":"3\/4","key":"13_CR15","doi-asserted-by":"crossref","first-page":"287","DOI":"10.3233\/FI-1996-263404","volume":"26","author":"A. Habel","year":"1996","unstructured":"Habel, A., Heckel, R., Taentzer, G.: Graph grammars with negative application conditions. Fundam. Inform.\u00a026(3\/4), 287\u2013313 (1996)","journal-title":"Fundam. Inform."},{"key":"13_CR16","doi-asserted-by":"crossref","unstructured":"Isenberg, T.: Bounded Model Checking f\u00fcr Graphtransformationssysteme als SMT-Problem. Master\u2019s thesis, University of Paderborn, Germany (2012)","DOI":"10.1007\/978-3-642-38592-6_13"},{"key":"13_CR17","unstructured":"Kastenberg, H.: Graph-based software specification and verification. Ph.D. thesis, University of Twente, Enschede (October 2008)"},{"key":"13_CR18","unstructured":"Kautz, H.A., Selman, B.: Planning as satisfiability. In: ECAI, pp. 359\u2013363 (1992)"},{"key":"13_CR19","doi-asserted-by":"crossref","unstructured":"K\u00f6nig, B., Kozioura, V.: Augur 2 - a new version of a tool for the analysis of graph transformation systems. Electronic Notes in Theoretical Computer Science\u00a0211(0), 201\u2013210 (2008); Proceedings of the Fifth International Workshop on Graph Transformation and Visual Modeling Techniques (GT-VMT 2006)","DOI":"10.1016\/j.entcs.2008.04.042"},{"key":"13_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1007\/978-3-642-15928-2_3","volume-title":"Graph Transformations","author":"H.-J. Kreowski","year":"2010","unstructured":"Kreowski, H.-J., Kuske, S., Wille, R.: Graph Transformation Units Guided by a SAT Solver. In: Ehrig, H., Rensink, A., Rozenberg, G., Sch\u00fcrr, A. (eds.) ICGT 2010. LNCS, vol.\u00a06372, pp. 27\u201342. Springer, Heidelberg (2010)"},{"key":"13_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L. Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.S.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"13_CR22","unstructured":"Rensink, A.: The joys of graph transformation. Nieuwsbrief van de Nederlandse Vereniging voor Theoretische Informatica\u00a09 (2005)"},{"key":"13_CR23","unstructured":"Rensink, A., Zambon, E.: Neighbourhood abstraction in GROOVE. Electronic Communications of the EASST\u00a032 (2011)"},{"key":"13_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"479","DOI":"10.1007\/978-3-540-25959-6_40","volume-title":"Applications of Graph Transformations with Industrial Relevance","author":"A. Rensink","year":"2004","unstructured":"Rensink, A.: The GROOVE simulator: A\u00a0tool for state space generation. In: Pfaltz, J.L., Nagl, M., B\u00f6hlen, B. (eds.) AGTIVE 2003. LNCS, vol.\u00a03062, pp. 479\u2013485. Springer, Heidelberg (2004)"},{"key":"13_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1007\/978-3-642-33654-6_5","volume-title":"Graph Transformations","author":"A. Rensink","year":"2012","unstructured":"Rensink, A., Zambon, E.: Pattern-based graph abstraction. In: Ehrig, H., Engels, G., Kreowski, H.-J., Rozenberg, G. (eds.) ICGT 2012. LNCS, vol.\u00a07562, pp. 66\u201380. Springer, Heidelberg (2012)"},{"key":"13_CR26","unstructured":"Rintanen, J.: Planning and sat. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol.\u00a0185, pp. 483\u2013504. IOS Press (2009)"},{"issue":"3","key":"13_CR27","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. ACM Trans. Program. Lang. Syst.\u00a024(3), 217\u2013298 (2002)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"13_CR28","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.\u00a07021, pp. 92\u2013107. Springer, Heidelberg (2011)"},{"key":"13_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1007\/978-3-642-34176-2_13","volume-title":"Applications of Graph Transformations with Industrial Relevance","author":"M. Tichy","year":"2012","unstructured":"Tichy, M., Kl\u00f6pper, B.: Planning self-adaption with graph transformations. In: Sch\u00fcrr, A., Varr\u00f3, D., Varr\u00f3, G. (eds.) AGTIVE 2011. LNCS, vol.\u00a07233, pp. 137\u2013152. Springer, Heidelberg (2012)"},{"key":"13_CR30","unstructured":"Vandin, A., Lluch-Lafuente, A.: Towards a maude tool for model checking temporal graph properties. ECEASST\u00a041 (2011)"},{"key":"13_CR31","doi-asserted-by":"crossref","unstructured":"Zambon, E., Rensink, A.: Graph subsumption in abstract state space exploration. arXiv preprint arXiv:1210.6413 (2012)","DOI":"10.4204\/EPTCS.99.6"}],"container-title":["Lecture Notes in Computer Science","Formal Techniques for Distributed Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-38592-6_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,7,27]],"date-time":"2020-07-27T07:32:25Z","timestamp":1595835145000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-38592-6_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642385919","9783642385926"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-38592-6_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013]]}}}