{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T05:01:02Z","timestamp":1725858062539},"publisher-location":"Cham","reference-count":27,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319411347"},{"type":"electronic","value":"9783319411354"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"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":[[2016]]},"DOI":"10.1007\/978-3-319-41135-4_6","type":"book-chapter","created":{"date-parts":[[2016,6,20]],"date-time":"2016-06-20T12:23:38Z","timestamp":1466425418000},"page":"94-111","source":"Crossref","is-referenced-by-count":1,"title":["Lightweight Symbolic Verification of Graph Transformation Systems with Off-the-Shelf Hardware Model Checkers"],"prefix":"10.1007","author":[{"given":"Sebastian","family":"Gabmeyer","sequence":"first","affiliation":[]},{"given":"Martina","family":"Seidl","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,6,21]]},"reference":[{"key":"6_CR1","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press, Cambridge (2008)"},{"key":"6_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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. 4178, pp. 306\u2013320. Springer, Heidelberg (2006)"},{"issue":"6","key":"6_CR3","doi-asserted-by":"crossref","first-page":"139","DOI":"10.1145\/1743546.1743583","volume":"53","author":"B Baudry","year":"2010","unstructured":"Baudry, B., Ghosh, S., Fleurey, F., France, R.B., Le Traon, Y., Mottu, J.-M.: Barriers to systematic model transformation testing. Commun. ACM 53(6), 139\u2013143 (2010)","journal-title":"Commun. ACM"},{"key":"6_CR4","unstructured":"Biermann, E., Ermel, C., Taentzer, G.: Lifting parallel graph transformation concepts to model transformation based on the eclipse modeling framework. Electron. Commun. ECEASST 26 (2010)"},{"issue":"2","key":"6_CR5","doi-asserted-by":"crossref","first-page":"227","DOI":"10.1007\/s10270-011-0199-7","volume":"11","author":"E Biermann","year":"2012","unstructured":"Biermann, E., Ermel, C., Taentzer, G.: Formal foundation of consistent EMF model transformations by algebraic graph transformation. Softw. Syst. Model. 11(2), 227\u2013250 (2012)","journal-title":"Softw. Syst. Model."},{"key":"6_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"221","DOI":"10.1007\/978-3-319-11245-9_13","volume-title":"Software Language Engineering","author":"R Bill","year":"2014","unstructured":"Bill, R., Gabmeyer, S., Kaufmann, P., Seidl, M.: Model checking of CTL-extended OCL specifications. In: Combemale, B., Pearce, D.J., Barais, O., Vinju, J.J. (eds.) SLE 2014. LNCS, vol. 8706, pp. 221\u2013240. Springer, Heidelberg (2014)"},{"key":"6_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"70","DOI":"10.1007\/978-3-642-18275-4_7","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"AR Bradley","year":"2011","unstructured":"Bradley, A.R.: SAT-based model checking without unrolling. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol. 6538, pp. 70\u201387. Springer, Heidelberg (2011)"},{"issue":"3","key":"6_CR8","doi-asserted-by":"crossref","first-page":"621","DOI":"10.1147\/sj.453.0621","volume":"45","author":"K Czarnecki","year":"2006","unstructured":"Czarnecki, K., Helsen, S.: Feature-based survey of model transformation approaches. IBM Syst. J. 45(3), 621\u2013645 (2006)","journal-title":"IBM Syst. J."},{"key":"6_CR9","unstructured":"Dijkstra, E.W.: Cooperating sequential processes, ewd 123. https:\/\/www.cs.utexas.edu\/users\/EWD\/transcriptions\/EWD01xx\/EWD123.html"},{"issue":"10","key":"6_CR10","doi-asserted-by":"crossref","first-page":"859","DOI":"10.1145\/355604.361591","volume":"15","author":"EW Dijkstra","year":"1972","unstructured":"Dijkstra, E.W.: The humble programmer. Commun. ACM 15(10), 859\u2013866 (1972)","journal-title":"Commun. ACM"},{"key":"6_CR11","series-title":"Monographs in Theoretical Computer Science. An EATCS Series","volume-title":"Fundamentals of Algebraic Graph Transformation","author":"H Ehrig","year":"2006","unstructured":"Ehrig, H., Ehrig, K., Prange, U., Taentzer, G.: Fundamentals of Algebraic Graph Transformation. Monographs in Theoretical Computer Science. An EATCS Series. Springer, Heidelberg (2006)"},{"key":"6_CR12","volume-title":"Communicating Sequential Processes","author":"CAR Hoare","year":"1985","unstructured":"Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall International, Upper saddle River (1985)"},{"key":"6_CR13","doi-asserted-by":"crossref","unstructured":"Jackson, D.: Automating first-order relational logic. In: Proceedings of the 8th ACM SIGSOFT International Symposium on Foundations of Software Engineering, pp. 130\u2013139. ACM (2000)","DOI":"10.1145\/355045.355063"},{"issue":"2","key":"6_CR14","doi-asserted-by":"crossref","first-page":"256","DOI":"10.1145\/505145.505149","volume":"11","author":"D Jackson","year":"2002","unstructured":"Jackson, D.: Alloy: a lightweight object modelling notation. ACM Trans. Softw. Eng. Methodol. 11(2), 256\u2013290 (2002)","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"key":"6_CR15","doi-asserted-by":"crossref","first-page":"315","DOI":"10.1016\/j.scico.2014.04.005","volume":"96","author":"P James","year":"2014","unstructured":"James, P., Moller, F., Nguyen, H.N., Roggenbach, M., Schneider, S.A., Treharne, H.: On modelling and verifying railway interlockings. Tracking Train Lengths Sci. Comput. Program. 96, 315\u2013336 (2014)","journal-title":"Tracking Train Lengths Sci. Comput. Program."},{"key":"6_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"299","DOI":"10.1007\/11691617_19","volume-title":"Model Checking Software","author":"H Kastenberg","year":"2006","unstructured":"Kastenberg, H., Rensink, A.: Model checking dynamic states in GROOVE. In: Valmari, A. (ed.) SPIN 2006. LNCS, vol. 3925, pp. 299\u2013305. Springer, Heidelberg (2006)"},{"key":"6_CR17","series-title":"Lecture Notes in Computer Science","first-page":"235","volume-title":"Concurrency: Theory, Language, And Architecture","author":"DL McBurney","year":"1989","unstructured":"McBurney, D.L., Sleep, M.R.: Graph rewriting as a computational model. In: Yonezawa, A., Ito, T. (eds.) Concurrency: Theory, Language, And Architecture. LNCS, vol. 491, pp. 235\u2013256. Springer, Heidelberg (1989)"},{"key":"6_CR18","unstructured":"Naur, P., Randell, B. (eds.) Software Engineering: Report of a Conference Sponsored by the NATO Science Committee, Garmisch, Germany, 7\u201311 October 1968, Brussels, Scientific Affairs Division, NATO. NATO (1969)"},{"key":"6_CR19","doi-asserted-by":"crossref","unstructured":"Niemann, P., Hilken, F., Gogolla, M., Wille, R.: Assisted generation of frame conditions for formal models. In: Proceedings of the 2015 Design, Automation & Test in Europe Conference & Exhibition, DATE 2015, San Jose, CA, USA, pp. 309\u2013312. EDA Consortium (2015)","DOI":"10.7873\/DATE.2015.0646"},{"key":"6_CR20","unstructured":"Object Management Group OMG. OMG Unified Modeling Language (OMG UML), Infrastructure V2.4.1, August 2011. http:\/\/www.omg.org\/spec\/UML\/2.4.1\/"},{"key":"6_CR21","series-title":"Foundations","volume-title":"Handbook of Graph Grammars and Computing by Graph Transformations","year":"1997","unstructured":"Rozenberg, G. (ed.): Handbook of Graph Grammars and Computing by Graph Transformations. Foundations, vol. 1. World Scientific, Singapore (1997)"},{"key":"6_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"92","DOI":"10.1007\/978-3-540-45221-8_8","volume-title":"\u00abUML\u00bb 2003 - The Unified Modeling Language. Modeling Languages and Applications","author":"A Schmidt","year":"2003","unstructured":"Schmidt, A., Varr\u00f3, D.: CheckVML: a tool for model checking visual modeling languages. In: Stevens, P., Whittle, J., Booch, G. (eds.) UML 2003. LNCS, vol. 2863, pp. 92\u201395. Springer, Heidelberg (2003)"},{"issue":"5","key":"6_CR23","doi-asserted-by":"crossref","first-page":"42","DOI":"10.1109\/MS.2003.1231150","volume":"20","author":"S Sendall","year":"2003","unstructured":"Sendall, S., Kozaczynski, W.: Model transformation: the heart and soul of model-driven software development. IEEE Softw. 20(5), 42\u201345 (2003)","journal-title":"IEEE Softw."},{"issue":"3","key":"6_CR24","doi-asserted-by":"crossref","first-page":"73","DOI":"10.2307\/2268577","volume":"6","author":"A Tarski","year":"1941","unstructured":"Tarski, A.: On the calculus of relations. J. Symb. Log. 6(3), 73\u201389 (1941)","journal-title":"J. Symb. Log."},{"key":"6_CR25","unstructured":"Torlak, E.: A Constraint Solver for Software Engineering: Finding Models and Cores of Large Relational Specifications. Ph.D. Thesis, Massachusetts Institute of Technology, 2009. AAI0821754"},{"key":"6_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"632","DOI":"10.1007\/978-3-540-71209-1_49","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E Torlak","year":"2007","unstructured":"Torlak, E., Jackson, D.: Kodkod: a relational model finder. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 632\u2013647. Springer, Heidelberg (2007)"},{"key":"6_CR27","volume-title":"Why Programs Fail: A Guide to Systematic Debugging","author":"A Zeller","year":"2009","unstructured":"Zeller, A.: Why Programs Fail: A Guide to Systematic Debugging, 2nd edn. Morgan Kaufmann Publishers Inc., San Francisco (2009)","edition":"2"}],"container-title":["Lecture Notes in Computer Science","Tests and Proofs"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-41135-4_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,6,24]],"date-time":"2017-06-24T12:44:31Z","timestamp":1498308271000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-41135-4_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319411347","9783319411354"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-41135-4_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}