{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T07:18:38Z","timestamp":1672557518967},"reference-count":73,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2016,8,16]],"date-time":"2016-08-16T00:00:00Z","timestamp":1471305600000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Softw Syst Model"],"published-print":{"date-parts":[[2018,10]]},"DOI":"10.1007\/s10270-016-0553-x","type":"journal-article","created":{"date-parts":[[2016,8,16]],"date-time":"2016-08-16T03:27:54Z","timestamp":1471318074000},"page":"1197-1225","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Formalised EMFTVM bytecode language for sound verification of model transformations"],"prefix":"10.1007","volume":"17","author":[{"given":"Zheng","family":"Cheng","sequence":"first","affiliation":[]},{"given":"Rosemary","family":"Monahan","sequence":"additional","affiliation":[]},{"given":"James F.","family":"Power","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,8,16]]},"reference":[{"key":"553_CR1","doi-asserted-by":"crossref","unstructured":"Amrani, M., Lucio, L., Selim, G., Combemale, B., Dingel, J., Vangheluwe, H., Le\u00a0Traon, Y., Cordy, J.R.: A tridimensional approach for studying the formal verification of model transformations. In: 5th International Conference on Software Testing, Verification and Validation. pp. 921\u2013928. IEEE, Washington, DC, USA (2012)","DOI":"10.1109\/ICST.2012.197"},{"key":"553_CR2","unstructured":"Anastasakis, K., Bordbar, B., K\u00fcster., J.M.: Analysis of model transformations via Alloy. In: 4th Workshop on Model-Driven Engineering, Verification and Validation. pp. 47\u201356. Nashville, TN, USA (2007)"},{"key":"553_CR3","doi-asserted-by":"crossref","unstructured":"Arendt, T., Biermann, E., Jurack, S., Krause, C., Taentzer, G.: Henshin: advanced concepts and tools for in-place EMF model transformations. In: 13th International Conference on Model Driven Engineering Languages and Systems, pp. 121\u2013135. Springer, Oslo, Norway (2010)","DOI":"10.1007\/978-3-642-16145-2_9"},{"issue":"5","key":"553_CR4","doi-asserted-by":"crossref","first-page":"405","DOI":"10.1002\/stvr.1502","volume":"23","author":"M Asztalos","year":"2013","unstructured":"Asztalos, M., Lengyel, L., Levendovszky, T.: Formal specification and analysis of functional properties of graph rewriting-based model transformation. Softw. Test. Verif. Reliab. 23(5), 405\u2013435 (2013)","journal-title":"Softw. Test. Verif. Reliab."},{"key":"553_CR5","unstructured":"ATLAS Group: Specification of the ATL virtual machine. Tech. rep., Lina & INRIA Nantes (2005)"},{"key":"553_CR6","doi-asserted-by":"crossref","unstructured":"Barnett, M., Chang, B.Y.E., DeLine, R., Jacobs, B., Leino, K.R.M.: Boogie: a modular reusable verifier for object-oriented programs. In: 4th International Conference on Formal Methods for Components and Objects, pp. 364\u2013387. Springer, Amsterdam, Netherlands (2006)","DOI":"10.1007\/11804192_17"},{"key":"553_CR7","doi-asserted-by":"crossref","unstructured":"Barnett, M., Leino, K.R.M., Schulte, W.: The Spec# programming system: an overview. In: 1st International Workshop on Construction and Analysis of Safe, Secure, and Interoperable Smart Devices, pp. 49\u201369. Springer, Marseille, France (2005)","DOI":"10.1007\/978-3-540-30569-9_3"},{"issue":"6","key":"553_CR8","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., Le Traon, Y., Mottu, J.M.: Barriers to systematic model transformation testing. Commun. ACM 53(6), 139\u2013143 (2010)","journal-title":"Commun. ACM"},{"key":"553_CR9","doi-asserted-by":"crossref","unstructured":"Benelellam, A., Gomez-Llana, A., Tisi, M., Cabot, J.: Distributed model-to-model transformation with ATL on MapReduce. In: 8th International Conference on Software Language Engineering, pp. 37\u201348. ACM, Pittsburg, USA (2015)","DOI":"10.1145\/2814251.2814258"},{"key":"553_CR10","doi-asserted-by":"crossref","unstructured":"Berry, G.: Synchronous design and verification of critical embedded systems using SCADE and Esterel. In: 12th International Workshop on Formal Methods for Industrial Critical Systems, pp. 2\u20132. Springer, Berlin, Germany (2008)","DOI":"10.1007\/978-3-540-79707-4_2"},{"key":"553_CR11","volume-title":"Implementing Domain-Specific Languages with Xtext and Xtend","author":"L Bettini","year":"2013","unstructured":"Bettini, L.: Implementing Domain-Specific Languages with Xtext and Xtend. Packt Publishing, Birmingham (2013)"},{"key":"553_CR12","unstructured":"Bock, C., Cook, S., Rivett, P., Rutt, T., Seidewitz, E., Selic, B., Tolbert, D.: OMG Unified Modeling Language (ver. 2.5). Tech. Rep. formal\/2015-03-01 (2015)"},{"key":"553_CR13","doi-asserted-by":"crossref","unstructured":"Bornat, R.: Proving pointer programs in Hoare logic. In: International Conference on Mathematics of Program Construction, pp. 102\u2013126. Springer, Ponte de Lima, Portugal (2000)","DOI":"10.1007\/10722010_8"},{"issue":"5","key":"553_CR14","doi-asserted-by":"crossref","first-page":"490","DOI":"10.1109\/TSE.2014.2375201","volume":"41","author":"L Burgue\u00f1o","year":"2015","unstructured":"Burgue\u00f1o, L., Troya, J., Wimmer, M., Vallecillo, A.: Static fault localization in model transformations. IEEE Trans. Softw. Eng. 41(5), 490\u2013506 (2015)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"553_CR15","doi-asserted-by":"crossref","unstructured":"B\u00fcttner, F., Egea, M., Cabot, J., Gogolla, M.: Verification of ATL transformations using transformation models and model finders. In: 14th International Conference on Formal Engineering Methods, pp. 198\u2013213. Springer, Kyoto, Japan (2012)","DOI":"10.1007\/978-3-642-34281-3_16"},{"key":"553_CR16","doi-asserted-by":"crossref","unstructured":"Calegari, D., Luna, C., Szasz, N., Tasistro, \u00c1.: A type-theoretic framework for certified model transformations. In: 13th Brazilian Symposium on Formal Methods, pp. 112\u2013127. Springer, Natal, Brazil (2011)","DOI":"10.1007\/978-3-642-19829-8_8"},{"key":"553_CR17","doi-asserted-by":"crossref","first-page":"5","DOI":"10.1016\/j.entcs.2013.02.002","volume":"292","author":"D Calegari","year":"2013","unstructured":"Calegari, D., Szasz, N.: Verification of model transformations: a survey of the state-of-the-art. Electron. Notes in Theor. Comput. Sci. 292, 5\u201325 (2013)","journal-title":"Electron. Notes in Theor. Comput. Sci."},{"key":"553_CR18","doi-asserted-by":"crossref","unstructured":"Chan, K.: Formal proofs for QoS-oriented transformations. In: 10th International Conference Workshops on Enterprise Distributed Object Computing, pp. 41\u201341. IEEE, Hong Kong, China (2006)","DOI":"10.1109\/EDOCW.2006.38"},{"key":"553_CR19","doi-asserted-by":"crossref","unstructured":"Cheng, Z., Monahan, R., Power, J.F.: A sound execution semantics for ATL via translation validation. In: 8th International Conference on Model Transformation, pp. 133\u2013148. Springer, L\u2019Aquila, Italy (2015)","DOI":"10.1007\/978-3-319-21155-8_11"},{"key":"553_CR20","unstructured":"Cheng, Z., Monahan, R., Power, J.F.: Online repository for formalised EMFTVM bytecode language. https:\/\/github.com\/veriatl\/Compiler.Emftvm2Boogie (2016)"},{"key":"553_CR21","doi-asserted-by":"crossref","unstructured":"Cheng, Z.: Formal Verification of Relational Model Transformations Using an Intermediate Verification Language. Ph.D. thesis, Maynooth University (2016)","DOI":"10.1109\/ICST.2017.41"},{"issue":"9","key":"553_CR22","doi-asserted-by":"crossref","first-page":"943","DOI":"10.4304\/jsw.4.9.943-958","volume":"4","author":"B Combemale","year":"2009","unstructured":"Combemale, B., Cr\u00e9gut, X., Garoche, P., Thirioux, X.: Essay on semantics definition in MDE\u2014an instrumented approach for model verification. J. Softw. 4(9), 943\u2013958 (2009)","journal-title":"J. Softw."},{"key":"553_CR23","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: 4th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, pp. 238\u2013252. ACM, Los Angeles, California (1977)","DOI":"10.1145\/512950.512973"},{"issue":"3","key":"553_CR24","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":"553_CR25","doi-asserted-by":"crossref","unstructured":"Dahlweid, M., Moskal, M., Santen, T., Tobies, S., Schulte, W.: VCC: Contract-based modular verification of concurrent C. In: 31st International Conference on Software Engineering, pp. 429\u2013430. IEEE, Vancouver, British Columbia (2009)","DOI":"10.1109\/ICSE-COMPANION.2009.5071046"},{"key":"553_CR26","doi-asserted-by":"crossref","unstructured":"Darvas, \u00c1., Leino, K.R.M.: Practical reasoning about invocations and implementations of pure methods. In: 10th International Conference on Fundamental Approaches to Software Engineering, pp. 336\u2013351. Springer, Braga, Portugal (2007)","DOI":"10.1007\/978-3-540-71289-3_26"},{"issue":"5","key":"553_CR27","doi-asserted-by":"crossref","first-page":"59","DOI":"10.5381\/jot.2006.5.5.a3","volume":"5","author":"\u00c1 Darvas","year":"2006","unstructured":"Darvas, \u00c1., M\u00fcller, P.: Reasoning about method calls in interface specifications. J. Object Technol. 5(5), 59\u201385 (2006)","journal-title":"J. Object Technol."},{"key":"553_CR28","doi-asserted-by":"crossref","unstructured":"de\u00a0Moura, L., Bj\u00f8rner, N.: Z3: An efficient SMT solver. In: 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 337\u2013340. Springer, Budapest, Hungary (2008)","DOI":"10.1007\/978-3-540-78800-3_24"},{"issue":"3","key":"553_CR29","doi-asserted-by":"crossref","first-page":"365","DOI":"10.1145\/1066100.1066102","volume":"52","author":"D Detlefs","year":"2005","unstructured":"Detlefs, D., Nelson, G., Saxe, J.B.: Simplify: a theorem prover for program checking. J. ACM 52(3), 365\u2013473 (2005)","journal-title":"J. ACM"},{"key":"553_CR30","doi-asserted-by":"crossref","unstructured":"Filli\u00e2tre, J.C., Paskevich, A.: Why3\u2014 where programs meet provers. In: 22nd European Symposium on Programming, pp. 125\u2013128. Springer, Rome, Italy (2013)","DOI":"10.1007\/978-3-642-37036-6_8"},{"key":"553_CR31","doi-asserted-by":"crossref","unstructured":"Filli\u00e2tre, J.C.: Why: A multi-language multi-prover verification tool. Tech. rep., Universit\u00e9 Paris Sud (2003)","DOI":"10.1007\/978-3-540-30482-1_10"},{"issue":"1\u20132","key":"553_CR32","doi-asserted-by":"crossref","first-page":"101","DOI":"10.1007\/s10472-009-9153-6","volume":"55","author":"Y Ge","year":"2009","unstructured":"Ge, Y., Barrett, C., Tinelli, C.: Solving quantified verification conditions using satisfiability modulo theories. Ann. Math. Artif. Intell. 55(1\u20132), 101\u2013122 (2009)","journal-title":"Ann. Math. Artif. Intell."},{"issue":"4","key":"553_CR33","doi-asserted-by":"crossref","first-page":"1447","DOI":"10.1007\/s10270-012-0292-6","volume":"13","author":"E Guerra","year":"2014","unstructured":"Guerra, E., de Lara, J.: Colouring: execution, debug and analysis of QVT-relations transformations through coloured Petri nets. Softw. Syst. Model. 13(4), 1447\u20131472 (2014)","journal-title":"Softw. Syst. Model."},{"issue":"10","key":"553_CR34","doi-asserted-by":"crossref","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"CAR Hoare","year":"1969","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576\u2013580 (1969)","journal-title":"Commun. ACM"},{"key":"553_CR35","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511810275","volume-title":"Logic in Computer Science: Modelling and Reasoning About Systems","author":"M Huth","year":"2004","unstructured":"Huth, M., Ryan, M.: Logic in Computer Science: Modelling and Reasoning About Systems. Cambridge University Press, Cambridge (2004)"},{"key":"553_CR36","doi-asserted-by":"crossref","unstructured":"Jackson, E.K., Levendovszky, T., Balasubramanian, D.: Reasoning about metamodeling with formal specifications and automatic proofs. In: 14th International Conference on Model Driven Engineering Languages and Systems, pp. 653\u2013667. Springer, Wellington, New Zealand (2011)","DOI":"10.1007\/978-3-642-24485-8_48"},{"issue":"2","key":"553_CR37","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":"553_CR38","unstructured":"Jouault, F.: The resolve algorithm implemented in the ASM language. http:\/\/git.eclipse.org\/c\/mmt\/org.eclipse.atl.git\/tree\/dsls\/ATL\/Compiler\/ATL.acg (2007)"},{"issue":"1\u20132","key":"553_CR39","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1016\/j.scico.2007.08.002","volume":"72","author":"F Jouault","year":"2008","unstructured":"Jouault, F., Allilaire, F., B\u00e9zivin, J., Kurtev, I.: ATL: a model transformation tool. Sci. Comput. Program. 72(1\u20132), 31\u201339 (2008)","journal-title":"Sci. Comput. Program."},{"key":"553_CR40","unstructured":"Klatt, B.: Xpand: a closer look at the model2text transformation language. http:\/\/bar54.de\/benjamin.klatt-xpand.pdf (2007)"},{"key":"553_CR41","volume-title":"MDA Explained: The Model Driven Architecture: Practice and Promise","author":"AG Kleppe","year":"2003","unstructured":"Kleppe, A.G., Warmer, J., Bast, W.: MDA Explained: The Model Driven Architecture: Practice and Promise. Addison-Wesley Longman, Boston (2003)"},{"issue":"1","key":"553_CR42","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1007\/s00165-014-0313-z","volume":"27","author":"K Lano","year":"2014","unstructured":"Lano, K., Clark, T., Kolahdouz-Rahimi, S.: A framework for model transformation verification. Formal Aspects Comput. 27(1), 193\u2013235 (2014)","journal-title":"Formal Aspects Comput."},{"key":"553_CR43","doi-asserted-by":"crossref","unstructured":"Lehner, H., M\u00fcller, P.: Formal translation of bytecode into BoogiePL. In: 2nd Workshop on Bytecode Semantics, Verification, Analysis and Transformation, pp. 35\u201350. Elsevier, Budapest, Hungary (2007)","DOI":"10.1016\/j.entcs.2007.02.059"},{"key":"553_CR44","doi-asserted-by":"crossref","unstructured":"Leino, K.R.M., Middelkoop, R.: Proving consistency of pure methods and model fields. In: 12th International Conference on Fundamental Approaches to Software Engineering, pp. 231\u2013245. Springer, York, UK (2009)","DOI":"10.1007\/978-3-642-00593-0_16"},{"key":"553_CR45","doi-asserted-by":"crossref","unstructured":"Leino, K.R.M., Monahan, R.: Reasoning about comprehensions with first-order SMT solvers. In: 24th Annual ACM Symposium on Applied Computing, pp. 615\u2013622. ACM, Hawaii, USA (2009)","DOI":"10.1145\/1529282.1529411"},{"key":"553_CR46","doi-asserted-by":"crossref","unstructured":"Leino, K.R.M.: Dafny: An automatic program verifier for functional correctness. In: 16th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, pp. 348\u2013370. Springer, Dakar, Senegal (2010)","DOI":"10.1007\/978-3-642-17511-4_20"},{"key":"553_CR47","unstructured":"Leino, K.R.M.: This is Boogie 2. http:\/\/research.microsoft.com\/en-us\/um\/people\/leino\/papers\/krml178.pdf . Microsoft Research, Redmond, USA (2008)"},{"key":"553_CR48","doi-asserted-by":"crossref","unstructured":"L\u00facio, L., Barroca, B., Amaral, V.: A technique for automatic validation of model transformations. In: 13th International Conference on Model Driven Engineering Languages and Systems, pp. 136\u2013150. Springer, Oslo, Norway (2010)","DOI":"10.1007\/978-3-642-16145-2_10"},{"key":"553_CR49","unstructured":"L\u00facio, L., Vangheluwe, H.: Model transformations to verify model transformations. In: 2nd Workshop on Verification of Model Transformations. Budapest, Hungary (2013)"},{"key":"553_CR50","first-page":"27","volume":"5","author":"Z Manna","year":"1969","unstructured":"Manna, Z., McCarthy, J.: Properties of programs and partial function logic. Mach. Intell. 5, 27\u201338 (1969)","journal-title":"Mach. Intell."},{"key":"553_CR51","doi-asserted-by":"crossref","unstructured":"Mottu, J., Baudry, B., Traon, Y.L.: Mutation analysis testing for model transformations. In: 2nd European Conference on Model Driven Architecture-Foundations and Applications. pp. 376\u2013390. Springer, Bilbao, Spain (2006)","DOI":"10.1007\/11787044_28"},{"key":"553_CR52","doi-asserted-by":"crossref","unstructured":"Pnueli, A., Siegel, M., Singerman, E.: Translation validation. In: 4th International Conference on Tools and Algorithms for Construction and Analysis of Systems, pp. 151\u2013166. Springer, London, UK (1998)","DOI":"10.1007\/BFb0054170"},{"key":"553_CR53","doi-asserted-by":"crossref","unstructured":"Poernomo, I., Terrell, J.: Correct-by-construction model transformations from partially ordered specifications in Coq. In: 12th International Conference on Formal Engineering Methods, pp. 56\u201373. Springer, Shanghai, China (2010)","DOI":"10.1007\/978-3-642-16901-4_6"},{"key":"553_CR54","doi-asserted-by":"crossref","unstructured":"Poernomo, I.: Proofs-as-model-transformations. In: 1st International Conference on Model Transformation, pp. 214\u2013228. Springer, Z\u00fcrich, Switzerland (2008)","DOI":"10.1007\/978-3-540-69927-9_15"},{"issue":"2","key":"553_CR55","doi-asserted-by":"crossref","first-page":"1003","DOI":"10.1007\/s10270-013-0358-0","volume":"14","author":"LA Rahim","year":"2015","unstructured":"Rahim, L.A., Whittle, J.: A survey of approaches for verifying model transformations. Softw. Syst. Model. 14(2), 1003\u20131028 (2015)","journal-title":"Softw. Syst. Model."},{"issue":"11","key":"553_CR56","doi-asserted-by":"crossref","first-page":"821","DOI":"10.1002\/smr.1735","volume":"27","author":"D Sahin","year":"2015","unstructured":"Sahin, D., Kessentini, M., Wimmer, M., Deb, K.: Model transformation testing: a bi-level search-based software engineering approach. J. Softw. Evol. Process 27(11), 821\u2013837 (2015)","journal-title":"J. Softw. Evol. Process"},{"key":"553_CR57","unstructured":"Sch\u00e4tz, B.: Verification of model transformations. In: 9th International Workshop on Graph Transformation and Visual Modeling Techniques, pp. 130\u2013142. EASST, Paphos, Cyprus (2010)"},{"key":"553_CR58","doi-asserted-by":"crossref","unstructured":"Selim, G., Wang, S., Cordy, J., Dingel, J.: Model transformations for migrating legacy models: an industrial case study. In: 8th European Conference on Modelling Foundations and Applications, pp. 90\u2013101. Springer, Lyngby, Denmark (2012)","DOI":"10.1007\/978-3-642-31491-9_9"},{"key":"553_CR59","volume-title":"EMF: eclipse modeling framework","author":"D Steinberg","year":"2008","unstructured":"Steinberg, D., Budinsky, F., Merks, E., Paternostro, M.: EMF: eclipse modeling framework, 2nd edn. Pearson Education, London (2008)","edition":"2"},{"issue":"2","key":"553_CR60","doi-asserted-by":"crossref","first-page":"387","DOI":"10.1007\/s10270-011-0205-0","volume":"12","author":"E Syriani","year":"2013","unstructured":"Syriani, E., Vangheluwe, H.: A modular timed graph transformation language for simulation-based design. Softw. Syst. Model. 12(2), 387\u2013414 (2013)","journal-title":"Softw. Syst. Model."},{"key":"553_CR61","doi-asserted-by":"crossref","unstructured":"Tristan, J., Govereau, P., Morrisett, G.: Evaluating value-graph translation validation for LLVM. In: 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 295\u2013305. ACM, San Jose, USA (2011)","DOI":"10.1145\/1993498.1993533"},{"key":"553_CR62","doi-asserted-by":"crossref","unstructured":"Tristan, J., Leroy, X.: A simple, verified validator for software pipelining. In: 37th ACM Symposium on Principles of Programming Languages, pp. 83\u201392. ACM, Madrid, Spain (2010)","DOI":"10.1145\/1706299.1706311"},{"issue":"5","key":"553_CR63","first-page":"1","volume":"10","author":"J Troya","year":"2011","unstructured":"Troya, J., Vallecillo, A.: A rewriting logic semantics for ATL. J. Object Technol. 10(5), 1\u201329 (2011)","journal-title":"J. Object Technol."},{"key":"553_CR64","unstructured":"Tschannen, J., Furia, C.A., Nordio, M., Meyer, B.: Verifying Eiffel programs with Boogie. In: Computing Research Repository abs\/1106.4700 (2011)"},{"key":"553_CR65","doi-asserted-by":"crossref","unstructured":"Varr\u00f3, G., Varr\u00f3, D., Friedl, K.: Adaptive graph pattern matching for model transformations using model-sensitive search plans. In: 1st International Workshop on Graph and Model Transformations, pp. 191\u2013205. Elsevier, Brighton, United Kingdom (2006)","DOI":"10.1016\/j.entcs.2005.10.025"},{"key":"553_CR66","unstructured":"V\u00e9pa, \u00c9., B\u00e9zivin, J., Bruneli\u00e8re, H., Jouault, F.: Measuring model repositories. In: Summary of the 2006 Model Size Metrics Workshop. Springer, Genoa, Italy (2006)"},{"key":"553_CR67","unstructured":"Vignaga, A.: Metrics for measuring ATL model transformations. Tech. rep., Universidad de Chile (2009)"},{"key":"553_CR68","doi-asserted-by":"crossref","unstructured":"Wagelaar, D., Iovino, L., Ruscio, D.D., Pierantonio, A.: Translational semantics of a co-evolution specific language with the EMF transformation virtual machine. In: 5th International Conference on Model Transformation, pp. 192\u2013207. Springer, Prague, Czech Republic (2012)","DOI":"10.1007\/978-3-642-30476-7_13"},{"key":"553_CR69","doi-asserted-by":"crossref","unstructured":"Wagelaar, D., Tisi, M., Cabot, J., Jouault, F.: Towards a general composition semantics for rule-based model transformation. In: 14th International Conference on Model Driven Engineering Languages and Systems, pp. 623\u2013637. Springer, Wellington, New Zealand (2011)","DOI":"10.1007\/978-3-642-24485-8_46"},{"key":"553_CR70","unstructured":"Wagelaar, D.: The resolve algorithm implemented in the EMFTVM language. http:\/\/git.eclipse.org\/c\/mmt\/org.eclipse.atl.git\/tree\/plugins\/org.eclipse.m2m.atl.emftvm\/src\/org\/eclipse\/m2m\/atl\/emftvm\/util\/OCLOperations.java (2011)"},{"key":"553_CR71","unstructured":"Wagelaar, D.: Using ATL\/EMFTVM for import\/export of medical data. In: 2nd Software Development Automation Conference. Amsterdam, Netherlands (2014)"},{"key":"553_CR72","unstructured":"Wimmer, M., Kappel, G., Kusel, A., Retschitzegger, W., Schoenboeck, J., Schwinger, W.: Right or wrong? Verification of model transformations using colored Petri nets. In: 9th OOPSLA Workshop on Domain-Specific Modeling, pp. 101\u2013106. Helsinki School of Economics, Orlando, USA (2009)"},{"key":"553_CR73","doi-asserted-by":"crossref","unstructured":"Wu, H., Monahan, R., Power, J.: Exploiting attributed type graphs to generate metamodel instances using an SMT solver. In: 7th International Symposium on Theoretical Aspects of Software Engineering, pp. 175\u2013182. IEEE, Birmingham, UK (2013)","DOI":"10.1109\/TASE.2013.31"}],"container-title":["Software & Systems Modeling"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10270-016-0553-x\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-016-0553-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-016-0553-x","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-016-0553-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,7,6]],"date-time":"2022-07-06T01:09:20Z","timestamp":1657069760000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10270-016-0553-x"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,8,16]]},"references-count":73,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2018,10]]}},"alternative-id":["553"],"URL":"https:\/\/doi.org\/10.1007\/s10270-016-0553-x","relation":{},"ISSN":["1619-1366","1619-1374"],"issn-type":[{"value":"1619-1366","type":"print"},{"value":"1619-1374","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016,8,16]]}}}