{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,14]],"date-time":"2026-03-14T15:14:41Z","timestamp":1773501281867,"version":"3.50.1"},"reference-count":49,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2016,7,27]],"date-time":"2016-07-27T00:00:00Z","timestamp":1469577600000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"name":"TAPAS","award":["TIN2012-32273"],"award-info":[{"award-number":["TIN2012-32273"]}]},{"name":"THEOS","award":["TIC-5906"],"award-info":[{"award-number":["TIC-5906"]}]},{"name":"COPAS","award":["P12-TIC-1867"],"award-info":[{"award-number":["P12-TIC-1867"]}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Softw Syst Model"],"published-print":{"date-parts":[[2018,7]]},"DOI":"10.1007\/s10270-016-0548-7","type":"journal-article","created":{"date-parts":[[2016,7,27]],"date-time":"2016-07-27T10:13:05Z","timestamp":1469614385000},"page":"815-849","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":16,"title":["Full contract verification for ATL using symbolic execution"],"prefix":"10.1007","volume":"17","author":[{"given":"Bentley James","family":"Oakes","sequence":"first","affiliation":[]},{"given":"Javier","family":"Troya","sequence":"additional","affiliation":[]},{"given":"Levi","family":"L\u00facio","sequence":"additional","affiliation":[]},{"given":"Manuel","family":"Wimmer","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,7,27]]},"reference":[{"key":"548_CR1","unstructured":"A Short Introduction to SyVOLT. https:\/\/www.youtube.com\/watch?v=8PrR5RhPptY"},{"key":"548_CR2","unstructured":"ATL Zoo. http:\/\/www.eclipse.org\/atl\/atlTransformations"},{"key":"548_CR3","unstructured":"ATL2DSLTrans Artifacts. http:\/\/msdl.cs.mcgill.ca\/people\/levi\/files\/MODELS2015_SoSyM"},{"key":"548_CR4","unstructured":"Atlas Transformation Language (ATL). http:\/\/eclipse.org\/atl"},{"key":"548_CR5","doi-asserted-by":"publisher","unstructured":"Amrani, M., L\u00facio, L., Selim, G.M.K., Combemale, B., Dingel, J., Vangheluwe, H., Traon, Y.L., Cordy, J.R.: A tridimensional approach for studying the formal verification of model transformations. In: Proceedings of ICSTW, pp. 921\u2013928 (2012). doi: 10.1109\/ICST.2012.197","DOI":"10.1109\/ICST.2012.197"},{"key":"548_CR6","unstructured":"Anastasakis, K., Bordbar, B., K\u00fcster, J.M.: Analysis of model transformations via alloy. In: Proceedings of MoDeVVa, pp. 47\u201356 (2007)"},{"key":"548_CR7","doi-asserted-by":"publisher","unstructured":"Arendt, T., Habel, A., Radke, H., Taentzer, G.: From core OCL invariants to nested graph constraints. In: Proceedings of ICGT, 8571, pp. 97\u2013112 (2014). doi: 10.1007\/978-3-319-09108-2_7","DOI":"10.1007\/978-3-319-09108-2_7"},{"key":"548_CR8","doi-asserted-by":"crossref","unstructured":"Balogh, A., et al.: Workflow-driven tool integration using model transformations. In: Graph Transformations and Model-Driven Engineering, pp. 224\u2013248 (2010)","DOI":"10.1007\/978-3-642-17322-6_11"},{"key":"548_CR9","doi-asserted-by":"publisher","unstructured":"Barroca, B., L\u00facio, L., Amaral, V., F\u00e9lix, R., Sousa, V.: DSLTrans: a turing incomplete transformation language. In: Proceedings of SLE, pp. 296\u2013305 (2011). doi: 10.1007\/978-3-642-19440-5_19","DOI":"10.1007\/978-3-642-19440-5_19"},{"key":"548_CR10","doi-asserted-by":"publisher","unstructured":"Bergmann, G.: Translating OCL to graph patterns. In: Proceedings of MoDELS, 8767, pp. 670\u2013686 (2014). doi: 10.1007\/978-3-319-11653-2_41","DOI":"10.1007\/978-3-319-11653-2_41"},{"key":"548_CR11","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-031-02546-4","volume-title":"Model-Driven Software Engineering in Practice","author":"M Brambilla","year":"2012","unstructured":"Brambilla, M., Cabot, J., Wimmer, M.: Model-Driven Software Engineering in Practice. Morgan & Claypool Publishers, San Rafael (2012)"},{"issue":"5","key":"548_CR12","doi-asserted-by":"crossref","first-page":"490","DOI":"10.1109\/TSE.2014.2375201","volume":"41","author":"L Burgueno","year":"2015","unstructured":"Burgueno, 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":"548_CR13","doi-asserted-by":"publisher","unstructured":"B\u00fcttner, F., Egea, M., Cabot, J.: On verifying ATL transformations using \u2019off-the-shelf\u2019 SMT solvers. In: Proceedings of MoDELS, pp. 432\u2013448 (2012). doi: 10.1007\/978-3-642-33666-9_28","DOI":"10.1007\/978-3-642-33666-9_28"},{"key":"548_CR14","doi-asserted-by":"publisher","unstructured":"B\u00fcttner, F., Egea, M., Guerra, E., De Lara, J.: Checking model transformation refinement. In: Proceedings of ICMT, pp. 158\u2013173 (2013). doi: 10.1007\/978-3-642-38883-5_15","DOI":"10.1007\/978-3-642-38883-5_15"},{"key":"548_CR15","doi-asserted-by":"publisher","unstructured":"Calegari, D., Luna, C., Szasz, N., Tasistro, A.: A type-theoretic framework for certified model transformations. In: Proceedings of SBMF, 6527, pp. 112\u2013127 (2010). doi: 10.1007\/978-3-642-19829-8_8","DOI":"10.1007\/978-3-642-19829-8_8"},{"key":"548_CR16","doi-asserted-by":"publisher","unstructured":"Cariou, E., Belloir, N., Barbier, F., Djemam, N.: OCL contracts for the verification of model transformations. ECEASST 24, 1\u201315 (2009). doi: 10.14279\/tuj.eceasst.24.326","DOI":"10.14279\/tuj.eceasst.24.326"},{"key":"548_CR17","doi-asserted-by":"publisher","unstructured":"Cheng, Z., Monahan, R., Power, J.F.: A sound execution semantics for ATL via translation validation. In: Proceedings of ICMT, pp. 133\u2013148 (2015). doi: 10.1007\/978-3-319-21155-8_11","DOI":"10.1007\/978-3-319-21155-8_11"},{"key":"548_CR18","volume-title":"All About Maude\u2013A High-Performance Logical Framework: How to Specify, Program and Verify Systems in Rewriting Logic","author":"M Clavel","year":"2007","unstructured":"Clavel, M., Dur\u00e1n, F., Eker, S., Lincoln, P., Mart\u00ed-Oliet, N., Meseguer, J., Talcott, C.: All About Maude\u2013A High-Performance Logical Framework: How to Specify, Program and Verify Systems in Rewriting Logic. Springer, Berlin (2007)"},{"key":"548_CR19","doi-asserted-by":"publisher","unstructured":"Cuadrado, J.S., Guerra, E., de Lara, J.: Uncovering errors in ATL model transformations using static analysis and constraint solving. In: Proceedings of ISSRE, pp. 34\u201344 (2014). doi: 10.1109\/ISSRE.2014.10","DOI":"10.1109\/ISSRE.2014.10"},{"key":"548_CR20","doi-asserted-by":"publisher","unstructured":"Gammaitoni, L., Kelsen, P.: F-alloy: an alloy based model transformation language. In: Proceedings of ICMT, pp. 166\u2013180 (2015). doi: 10.1007\/978-3-319-21155-8_13","DOI":"10.1007\/978-3-319-21155-8_13"},{"key":"548_CR21","doi-asserted-by":"publisher","unstructured":"Garc\u00eda-Dom\u00ednguez, A., Kolovos, D.S., Rose, L.M., Paige, R.F., Medina-Bulo, I.: EUnit: a unit testing framework for model management tasks. In: Proceedings of MoDELS, pp. 395\u2013409 (2011). doi: 10.1007\/978-3-642-24485-8_29","DOI":"10.1007\/978-3-642-24485-8_29"},{"key":"548_CR22","doi-asserted-by":"publisher","unstructured":"Giner, P., Pelechano, V.: Test-driven development of model transformations. In: Proceedings of MoDELS, pp. 748\u2013752 (2009). doi: 10.1007\/978-3-642-04425-0_61","DOI":"10.1007\/978-3-642-04425-0_61"},{"key":"548_CR23","unstructured":"Gogolla, M., Hamann, L., Hilken, F.: Checking transformation model properties with a UML and OCL model validator. In: Proceedings of VOLT, pp. 16\u201325 (2014)"},{"key":"548_CR24","doi-asserted-by":"publisher","unstructured":"Gogolla, M., Vallecillo, A.: Tractable model transformation testing. In: Proceedings of ECMFA, pp. 221\u2013235 (2011). doi: 10.1007\/978-3-642-21470-7_16","DOI":"10.1007\/978-3-642-21470-7_16"},{"key":"548_CR25","doi-asserted-by":"publisher","unstructured":"Gonz\u00e1lez, C.A., Cabot, J.: ATLTest: a white-box test generation approach for ATL transformations. In: Proceedings of MoDELS, pp. 449\u2013464 (2012). doi: 10.1007\/978-3-642-33666-9_29","DOI":"10.1007\/978-3-642-33666-9_29"},{"issue":"1","key":"548_CR26","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1007\/s10515-012-0102-y","volume":"20","author":"E Guerra","year":"2013","unstructured":"Guerra, E., de Lara, J., Wimmer, M., Kappel, G., Kusel, A., Retschitzegger, W., Sch\u00f6nb\u00f6ck, J., Schwinger, W.: Automated verification of model transformations based on visual contracts. Autom. Softw. Eng. 20(1), 5\u201346 (2013). doi: 10.1007\/s10515-012-0102-y","journal-title":"Autom. Softw. Eng."},{"issue":"1\u20132","key":"548_CR27","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":"548_CR28","doi-asserted-by":"publisher","unstructured":"Kolovos, D.S., Paige, R.F., Polack, F.A.: Model comparison: a foundation for model composition and model transformation testing. In: Proceedings of GaMMa, pp. 13\u201320 (2006). doi: 10.1145\/1138304.1138308","DOI":"10.1145\/1138304.1138308"},{"issue":"1","key":"548_CR29","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/s00165-014-0313-z","volume":"27","author":"K Lano","year":"2015","unstructured":"Lano, K., Clark, T., Rahimi, S.K.: A framework for model transformation verification. Formal Asp. Comput. 27(1), 193\u2013235 (2015). doi: 10.1007\/s00165-014-0313-z","journal-title":"Formal Asp. Comput."},{"key":"548_CR30","doi-asserted-by":"publisher","unstructured":"L\u00facio, L., Barroca, B., Amaral, V.: A technique for automatic validation of model transformations. In: Proceedings of MoDELS, pp. 136\u2013150 (2010). doi: 10.1007\/978-3-642-16145-2_10","DOI":"10.1007\/978-3-642-16145-2_10"},{"key":"548_CR31","unstructured":"L\u00facio, L., Oakes, B., Vangheluwe, H.: A Technique for Symbolically Verifying Properties of Graph-based Model Transformations. Technical report SOCS-TR-2014.1, McGill University (2014)"},{"key":"548_CR32","unstructured":"L\u00facio, L., Oakes, B.J., Gomes, C., Selim, G.M., Dingel, J., Cordy, J.R., Vangheluwe, H.: SyVOLT: Full model transformation verification using contracts. In: Proceedings of MoDELS 2015 Demo and Poster Session, pp. 24\u201327 (2015)"},{"key":"548_CR33","doi-asserted-by":"publisher","unstructured":"L\u00facio, L., Amrani, M., Dingel, J., Lambers, L., Salay, R., Selim, G., Syriani, E., Wimmer, M.: Model transformation intents and their properties. Softw. Syst. Model., pp. 1\u201338 (2014). doi: 10.1007\/s10270-014-0429-x","DOI":"10.1007\/s10270-014-0429-x"},{"key":"548_CR34","doi-asserted-by":"publisher","unstructured":"Mottu, J.M., Baudry, B., Traon, Y.L.: Model transformation testing: oracle issue. In: Proceedings of ICSTW, pp. 105\u2013112 (2008). doi: 10.1109\/icstw.2008.27","DOI":"10.1109\/icstw.2008.27"},{"key":"548_CR35","doi-asserted-by":"publisher","unstructured":"Oakes, B.J., Troya, J., L\u00facio, L., Wimmer, M.: Fully verifying transformation contracts for declarative ATL. In: Proceedings of MoDELS, pp. 256\u2013265 (2015). doi: 10.1109\/models.2015.7338256","DOI":"10.1109\/models.2015.7338256"},{"key":"548_CR36","unstructured":"Paen, E.: Measuring Incrementally Developed Model Transformations Using Change Metrics. Master\u2019s thesis, Queen\u2019s University (2012)"},{"key":"548_CR37","doi-asserted-by":"publisher","unstructured":"Poernomo, I., Terrell, J.: Correct-by-construction model transformations from partially ordered specifications in coq. In: Proceedings of ICFEM, pp. 56\u201373 (2010). doi: 10.1007\/978-3-642-16901-4_6","DOI":"10.1007\/978-3-642-16901-4_6"},{"issue":"1","key":"548_CR38","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1007\/s10270-014-0399-z","volume":"15","author":"E Posse","year":"2016","unstructured":"Posse, E., Dingel, J.: An executable formal semantics for UML-RT. Softw. Syst. Model. 15(1), 179\u2013217 (2016). doi: 10.1007\/s10270-014-0399-z","journal-title":"Softw. Syst. Model."},{"issue":"2","key":"548_CR39","doi-asserted-by":"publisher","first-page":"1003","DOI":"10.1007\/s10270-013-0358-0","volume":"14","author":"L Rahim","year":"2015","unstructured":"Rahim, L., Whittle, J.: A survey of approaches for verifying model transformations. Softw. Syst. Model. 14(2), 1003\u20131028 (2015). doi: 10.1007\/s10270-013-0358-0","journal-title":"Softw. Syst. Model."},{"key":"548_CR40","doi-asserted-by":"publisher","unstructured":"Richa, E., Borde, E., Pautet, L.: Translating ATL model transformations to algebraic graph transformations. In: Proceedings of ICMT, pp. 183\u2013198 (2015). doi: 10.1007\/978-3-319-21155-8_14","DOI":"10.1007\/978-3-319-21155-8_14"},{"key":"548_CR41","unstructured":"Selim, G.M.: Formal Verification of Graph-Based Model Transformations. Ph.D. thesis, Queen\u2019s University (2015)"},{"key":"548_CR42","unstructured":"Selim, G.M., Cordy, J.R., Dingel, J., L\u00facio, L., Oakes, B.J.: Finding and fixing bugs in model transformations with formal verification: an experience report. In: Proceedings of AMT, pp. 26\u201335 (2015)"},{"key":"548_CR43","doi-asserted-by":"publisher","unstructured":"Selim, G.M., L\u00facio, L., Cordy, J.R., Dingel, J., Oakes, B.J.: Specification and verification of graph-based model transformation properties. In: Proceedings of ICGT, pp. 113\u2013129 (2014). doi: 10.1007\/978-3-319-09108-2_8","DOI":"10.1007\/978-3-319-09108-2_8"},{"issue":"3","key":"548_CR44","doi-asserted-by":"publisher","first-page":"1215","DOI":"10.1007\/s10270-013-0370-4","volume":"14","author":"E Syriani","year":"2015","unstructured":"Syriani, E., Vangheluwe, H., LaShomb, B.: T-Core: a framework for custom-built model transformation engines. Softw. Syst. Model. 14(3), 1215\u20131243 (2015). doi: 10.1007\/s10270-013-0370-4","journal-title":"Softw. Syst. Model."},{"key":"548_CR45","unstructured":"SyVOLT tool. http:\/\/msdl.cs.mcgill.ca\/people\/levi\/contractprover"},{"key":"548_CR46","unstructured":"Tisi, M., Mart\u00ednez, S., Jouault, F., Cabot, J.: Refining Models with Rule-based Model Transformations. Research report RR-7582, INRIA (2011)"},{"issue":"5","key":"548_CR47","doi-asserted-by":"publisher","first-page":"1","DOI":"10.5381\/jot.2011.10.1.a5","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). doi: 10.5381\/jot.2011.10.1.a5","journal-title":"J. Object Technol."},{"key":"548_CR48","doi-asserted-by":"crossref","unstructured":"Vallecillo, A., Gogolla, M., Burgueno, L., Wimmer, M., Hamann, L.: Formal specification and testing of model transformations. In: Formal Methods for Model-Driven Engineering, pp. 399\u2013437 (2012)","DOI":"10.1007\/978-3-642-30982-3_11"},{"key":"548_CR49","doi-asserted-by":"crossref","unstructured":"Wieber, M., Anjorin, A., Sch\u00fcrr, A.: On the usage of TGGs for automated model transformation testing. In: Proceedings of ICMT, pp. 1\u201316 (2014)","DOI":"10.1007\/978-3-319-08789-4_1"}],"container-title":["Software & Systems Modeling"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10270-016-0548-7\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-016-0548-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-016-0548-7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-016-0548-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,8,19]],"date-time":"2023-08-19T10:41:38Z","timestamp":1692441698000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10270-016-0548-7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,7,27]]},"references-count":49,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2018,7]]}},"alternative-id":["548"],"URL":"https:\/\/doi.org\/10.1007\/s10270-016-0548-7","relation":{},"ISSN":["1619-1366","1619-1374"],"issn-type":[{"value":"1619-1366","type":"print"},{"value":"1619-1374","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016,7,27]]}}}