{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,12]],"date-time":"2024-09-12T15:16:32Z","timestamp":1726154192376},"publisher-location":"Berlin, Heidelberg","reference-count":28,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642336652"},{"type":"electronic","value":"9783642336669"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-33666-9_28","type":"book-chapter","created":{"date-parts":[[2012,9,18]],"date-time":"2012-09-18T16:50:20Z","timestamp":1347987020000},"page":"432-448","source":"Crossref","is-referenced-by-count":36,"title":["On Verifying ATL Transformations Using \u2018off-the-shelf\u2019 SMT Solvers"],"prefix":"10.1007","author":[{"given":"Fabian","family":"B\u00fcttner","sequence":"first","affiliation":[]},{"given":"Marina","family":"Egea","sequence":"additional","affiliation":[]},{"given":"Jordi","family":"Cabot","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"28_CR1","unstructured":"Anastasakis, K., Bordbar, B., K\u00fcster, J.M.: Analysis of Model Transformations via Alloy. In: Proceedings of MoDeVVa 2007 (2007), http:\/\/www.modeva.org\/2007\/modevva07.pdf"},{"key":"28_CR2","doi-asserted-by":"crossref","unstructured":"Asztalos, M., Lengyel, L., Levendovszky, T.: Towards automated, formal verification of model transformations. In: Proceedings 3rd International Conference on Software Testing, Verification and Validation, ICST 2010, pp. 15\u201324. IEEE Computer Society (2010)","DOI":"10.1109\/ICST.2010.42"},{"key":"28_CR3","unstructured":"ATL User Guide (2012) http:\/\/wiki.eclipse.org\/ATL\/User_Guide_-_The_ATL_Language"},{"key":"28_CR4","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":"28_CR5","doi-asserted-by":"crossref","unstructured":"Baudry, B., Ghosh, S., Fleurey, F., France, R.B., Traon, Y.L., Mottu, J.-M.: Barriers to systematic model transformation testing. Communications of ACM\u00a053(6) (2010)","DOI":"10.1145\/1743546.1743583"},{"key":"28_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/978-3-642-21732-6_9","volume-title":"Theory and Practice of Model Transformations","author":"B. Becker","year":"2011","unstructured":"Becker, B., Lambers, L., Dyck, J., Birth, S., Giese, H.: Iterative Development of Consistency-Preserving Rule-Based Refactorings. In: Cabot, J., Visser, E. (eds.) ICMT 2011. LNCS, vol.\u00a06707, pp. 123\u2013137. Springer, Heidelberg (2011)"},{"key":"28_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"18","DOI":"10.1007\/978-3-642-00593-0_2","volume-title":"Fundamental Approaches to Software Engineering","author":"A. Boronat","year":"2009","unstructured":"Boronat, A., Heckel, R., Meseguer, J.: Rewriting Logic Semantics and Verification of Model Transformations. In: Chechik, M., Wirsing, M. (eds.) FASE 2009. LNCS, vol.\u00a05503, pp. 18\u201333. Springer, Heidelberg (2009)"},{"key":"28_CR8","doi-asserted-by":"crossref","unstructured":"B\u00fcttner, F., Egea, M., Cabot, J.: On verifying ATL transformations using \u2018off-the-shelf\u2019 SMT solvers: Examples (2012), http:\/\/www.emn.fr\/z-info\/atlanmod\/index.php\/MODELS_2012_SMT","DOI":"10.1007\/978-3-642-33666-9_28"},{"key":"28_CR9","unstructured":"B\u00fcttner, F., Egea, M., Cabot, J., Gogolla, M.: Verification of ATL transformations using transformation models and model finders. In: Proceedings of 14th International Conference on Formal Engineering Methods, ICFEM 2012, Kyoto, Japan, November 12-16. LNCS, Springer (in press, 2012)"},{"key":"28_CR10","doi-asserted-by":"crossref","unstructured":"Cabot, J., Clariso, R., Guerra, E., Lara, J.: Verification and validation of declarative model-to-model transformations through invariants. Journal of Systems and Software\u00a083(2) (2010)","DOI":"10.1016\/j.jss.2009.08.012"},{"key":"28_CR11","unstructured":"Clavel, M., Egea, M., de Dios, M.A.G.: Checking unsatisfiability for OCL constraints. Electronic Communications of the EASST\u00a024 (2009)"},{"issue":"9","key":"28_CR12","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1145\/1995376.1995394","volume":"54","author":"L.M. Moura de","year":"2011","unstructured":"de Moura, L.M., Bj\u00f8rner, N.: Satisfiability modulo theories: Introduction and applications. Communications of ACM\u00a054(9), 69\u201377 (2011)","journal-title":"Communications of ACM"},{"key":"28_CR13","unstructured":"Dutertre, B., Moura, L.D.: The Yices SMT solver. Technical report, Computer Science Laboratory, SRI International (2006), http:\/\/yices.csl.sri.com\/tool-paper.pdf"},{"key":"28_CR14","unstructured":"Ehrig, H., Ehrig, K., Prange, U., Taentzer, G.: Fundamentals of Algebraic Graph Transformation. Monographs in Theoretical Computer Science. An EATCS Series. Springer (2006)"},{"key":"28_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"306","DOI":"10.1007\/978-3-642-02658-4_25","volume-title":"Computer Aided Verification","author":"Y. Ge","year":"2009","unstructured":"Ge, Y., de Moura, L.M.: Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol.\u00a05643, pp. 306\u2013320. Springer, Heidelberg (2009)"},{"key":"28_CR16","doi-asserted-by":"crossref","unstructured":"Inaba, K., Hidaka, S., Hu, Z., Kato, H., Nakano, K.: Graph-transformation verification using monadic second-order logic. In: Schneider-Kamp, P., Hanus, M. (eds.) Proceedings of ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, PPDP 2011, pp. 17\u201328. ACM (2011)","DOI":"10.1145\/2003476.2003482"},{"key":"28_CR17","doi-asserted-by":"crossref","unstructured":"Jouault, F., Allilaire, F., B\u00e9zivin, J., Kurtev, I.: ATL: A model transformation tool. Science of Computer Programming\u00a072(1-2) (2008)","DOI":"10.1016\/j.scico.2007.08.002"},{"key":"28_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"128","DOI":"10.1007\/11663430_14","volume-title":"Satellite Events at the MoDELS 2005 Conference","author":"F. Jouault","year":"2006","unstructured":"Jouault, F., Kurtev, I.: Transforming Models with ATL. In: Bruel, J.-M. (ed.) MoDELS 2005. LNCS, vol.\u00a03844, pp. 128\u2013138. Springer, Heidelberg (2006), http:\/\/sosym.dcs.kcl.ac.uk\/events\/mtip05\/submissions\/jouault_kurtev__transforming_models_with_atl.pdf"},{"key":"28_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1007\/978-3-642-21732-6_4","volume-title":"Theory and Practice of Model Transformations","author":"K. Lano","year":"2011","unstructured":"Lano, K., Kolahdouz-Rahimi, S.: Model-Driven Development of Model Transformations. In: Cabot, J., Visser, E. (eds.) ICMT 2011. LNCS, vol.\u00a06707, pp. 47\u201361. Springer, Heidelberg (2011)"},{"key":"28_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"136","DOI":"10.1007\/978-3-642-16145-2_10","volume-title":"Model Driven Engineering Languages and Systems","author":"L. Lucio","year":"2010","unstructured":"Lucio, L., Barroca, B., Amaral, V.: A Technique for Automatic Validation of Model Transformations. In: Petriu, D.C., Rouquette, N., Haugen, O. (eds.) MODELS 2010, Part I. LNCS, vol.\u00a06394, pp. 136\u2013150. Springer, Heidelberg (2010)"},{"key":"28_CR21","unstructured":"OMG. The Object Constraint Language Specification v. 2.2 (Document formal\/2010-02-01). Object Management Group, Inc. (2010), http:\/\/www.omg.org\/spec\/OCL\/2.2\/"},{"key":"28_CR22","unstructured":"OMG. Meta Object Facility (MOF) Core Specification 2.4.1 (Document formal\/2011-08-07). Object Management Group, Inc. (2011), http:\/\/www.omg.org"},{"issue":"1-2","key":"28_CR23","doi-asserted-by":"crossref","first-page":"135","DOI":"10.3233\/FI-2012-708","volume":"118","author":"C.M. Poskitt","year":"2012","unstructured":"Poskitt, C.M., Plump, D.: Hoare-style verification of graph programs. Fundamenta Informaticae\u00a0118(1-2), 135\u2013175 (2012)","journal-title":"Fundamenta Informaticae"},{"key":"28_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1007\/978-3-540-68679-8_8","volume-title":"Concurrency, Graphs and Models","author":"A. Rensink","year":"2008","unstructured":"Rensink, A.: Explicit State Model Checking for Graph Grammars. In: Degano, P., De Nicola, R., Meseguer, J. (eds.) Concurrency, Graphs and Models. LNCS, vol.\u00a05065, pp. 114\u2013132. Springer, Heidelberg (2008)"},{"key":"28_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"449","DOI":"10.1007\/978-3-540-49524-6_35","volume-title":"Conceptual Modeling \u2013 ER \u201998","author":"M. Richters","year":"1998","unstructured":"Richters, M., Gogolla, M.: On Formalizing the UML Object Constraint Language OCL. In: Ling, T.-W., Ram, S., Li Lee, M. (eds.) ER 1998. LNCS, vol.\u00a01507, pp. 449\u2013464. Springer, Heidelberg (1998)"},{"key":"28_CR26","doi-asserted-by":"crossref","unstructured":"Troya, J., Vallecillo, A.: A Rewriting Logic Semantics for ATL. Journal of Object Technology\u00a010 (2011)","DOI":"10.5381\/jot.2011.10.1.a5"},{"key":"28_CR27","unstructured":"Yices, http:\/\/yices.csl.sri.com\/"},{"key":"28_CR28","unstructured":"Z3, http:\/\/research.microsoft.com\/en-us\/um\/redmond\/projects\/z3\/"}],"container-title":["Lecture Notes in Computer Science","Model Driven Engineering Languages and Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-33666-9_28.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,4]],"date-time":"2021-05-04T12:18:12Z","timestamp":1620130692000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-33666-9_28"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642336652","9783642336669"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-33666-9_28","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}