{"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":1773501281834,"version":"3.50.1"},"reference-count":41,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2019,11,16]],"date-time":"2019-11-16T00:00:00Z","timestamp":1573862400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2019,11,16]],"date-time":"2019-11-16T00:00:00Z","timestamp":1573862400000},"content-version":"vor","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":[[2020,3]]},"DOI":"10.1007\/s10270-019-00765-6","type":"journal-article","created":{"date-parts":[[2019,11,16]],"date-time":"2019-11-16T07:02:00Z","timestamp":1573887720000},"page":"425-439","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["CoqTL: a Coq DSL for rule-based model transformation"],"prefix":"10.1007","volume":"19","author":[{"given":"Zheng","family":"Cheng","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Massimo","family":"Tisi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"R\u00e9mi","family":"Douence","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2019,11,16]]},"reference":[{"issue":"2","key":"765_CR1","doi-asserted-by":"publisher","first-page":"1003","DOI":"10.1007\/s10270-013-0358-0","volume":"14","author":"L Ab. Rahim","year":"2015","unstructured":"Ab. Rahim, L., Whittle, J.: A survey of approaches for verifying model transformations. Softw. Syst. Model. 14(2), 1003\u20131028 (2015)","journal-title":"Softw. Syst. Model."},{"issue":"6","key":"765_CR2","doi-asserted-by":"publisher","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":"765_CR3","unstructured":"Berghofer, S., Nipkow, T.: Random testing in isabelle\/HOL. In: 2nd International Conference on Software Engineering and Formal Methods, pp. 230\u2013239. IEEE, Beijing (2004)"},{"key":"765_CR4","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 (2008)","DOI":"10.1007\/978-3-540-79707-4_2"},{"issue":"5","key":"765_CR5","doi-asserted-by":"publisher","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":"765_CR6","doi-asserted-by":"publisher","first-page":"432","DOI":"10.1007\/978-3-642-33666-9_28","volume-title":"Model Driven Engineering Languages and Systems","author":"Fabian B\u00fcttner","year":"2012","unstructured":"B\u00fcttner, F., Egea, M., Cabot, J.: On verifying ATL transformations using \u2018off-the-shelf\u2019 SMT solvers. In: 15th International Conference on Model Driven Engineering Languages and Systems, pp. 198\u2013213. Springer, Innsbruck (2012)"},{"key":"765_CR7","doi-asserted-by":"publisher","first-page":"198","DOI":"10.1007\/978-3-642-34281-3_16","volume-title":"Formal Methods and Software Engineering","author":"Fabian B\u00fcttner","year":"2012","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 (2012)"},{"key":"765_CR8","first-page":"112","volume-title":"Lecture Notes in Computer Science","author":"Daniel Calegari","year":"2011","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 (2011)"},{"issue":"4","key":"765_CR9","doi-asserted-by":"publisher","first-page":"138","DOI":"10.1109\/TBDATA.2015.2505719","volume":"1","author":"L Cheng","year":"2015","unstructured":"Cheng, L., Kotoulas, S.: Scale-out processing of large RDF datasets. IEEE Trans. Big Data 1(4), 138\u2013150 (2015)","journal-title":"IEEE Trans. Big Data"},{"key":"765_CR10","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1007\/978-3-319-21155-8_11","volume-title":"Theory and Practice of Model Transformations","author":"Zheng Cheng","year":"2015","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 (2015)"},{"issue":"6","key":"765_CR11","doi-asserted-by":"publisher","first-page":"645","DOI":"10.1007\/s10009-018-0491-8","volume":"20","author":"Z Cheng","year":"2018","unstructured":"Cheng, Z., Tisi, M.: Slicing ATL model transformations for scalable deductive verification and fault localization. Int. J. Softw. Tools Technol. Transf. 20(6), 645\u2013663 (2018)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"765_CR12","doi-asserted-by":"crossref","unstructured":"Chlipala, A.: The Bedrock structured programming system: Combining generative metaprogramming and hoare logic in an extensible program verifier. In: 18th ACM SIGPLAN International Conference on Functional Programming, pp. 391\u2013402. ICFP \u201913. ACM, Boston, MA (2013)","DOI":"10.1145\/2500365.2500592"},{"key":"765_CR13","doi-asserted-by":"crossref","unstructured":"Cuadrado, J.S., Guerra, E., de\u00a0Lara, J.: Uncovering errors in ATL model transformations using static analysis and constraint solving. In: 25th IEEE International Symposium on Software Reliability Engineering, pp. 34\u201344. IEEE, Naples (2014)","DOI":"10.1109\/ISSRE.2014.10"},{"key":"765_CR14","doi-asserted-by":"publisher","first-page":"158","DOI":"10.1007\/11787044_13","volume-title":"Model Driven Architecture \u2013 Foundations and Applications","author":"Jes\u00fas S\u00e1nchez Cuadrado","year":"2006","unstructured":"Cuadrado, J.S., Molina, J.G., Tortosa, M.M.: RubyTL: A practical, extensible transformation language. In: 2nd European Conference on Model Driven Architecture: Foundations and Applications, pp. 158\u2013172. Springer, Bilbao (2006)"},{"key":"765_CR15","doi-asserted-by":"publisher","first-page":"174","DOI":"10.1007\/3-540-45923-5_12","volume-title":"Fundamental Approaches to Software Engineering","author":"Juan de Lara","year":"2002","unstructured":"de\u00a0Lara, J., Vangheluwe, H.: AToM$$^3$$: a tool for multi-formalism and meta-modelling. In: 5th International Conference on Fundamental Approaches to Software Engineering, pp. 174\u2013188. Springer, Grenoble (2002)"},{"key":"765_CR16","doi-asserted-by":"publisher","first-page":"63","DOI":"10.4204\/EPTCS.108.5","volume":"108","author":"Maribel Fern\u00e1ndez","year":"2013","unstructured":"Fern\u00e1ndez, M., Terrell, J.: Assembling the proofs of ordered model transformations. In: 10th International Workshop on Formal Engineering Approaches to Software Components and Architectures, pp. 63\u201377. EPTCS, Rome (2013)","journal-title":"Electronic Proceedings in Theoretical Computer Science"},{"key":"765_CR17","unstructured":"Gu, R., Shao, Z., Chen, H., Wu, X., Kim, J., Sj\u00f6berg, V., Costanzo, D.: CertiKOS: An extensible architecture for building certified concurrent os kernels. In: 12th USENIX Conference on Operating Systems Design and Implementation, pp. 653\u2013669. USENIX Association, Berkeley, CA (2016)"},{"key":"765_CR18","unstructured":"Hamiaz, M.K., Pantel, M., Combemale, B., Thirioux, X.: A formal framework to prove the correctness of model driven engineering composition operators. In: International Conference on Formal Engineering Methods (2014)"},{"key":"765_CR19","doi-asserted-by":"crossref","unstructured":"He, X., Hu, Z.: Putback-based bidirectional model transformations. In: 2018 ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering, pp. 434\u2013444. ACM, Miami Beach, FL (2018)","DOI":"10.1145\/3236024.3236070"},{"key":"765_CR20","doi-asserted-by":"crossref","unstructured":"Hidaka, S., Hu, Z., Inaba, K., Kato, H., Nakano, K.: GRoundTram: an integrated framework for developing well-behaved bidirectional model transformations. In: 26th IEEE\/ACM International Conference on Automated Software Engineering, pp. 480\u2013483. ACM, KS (2011)","DOI":"10.1109\/ASE.2011.6100104"},{"key":"765_CR21","doi-asserted-by":"crossref","unstructured":"Hidaka, S., Jouault, F., Tisi, M.: On additivity in transformation languages. In: 20th International Conference on Model Driven Engineering Languages and Systems, pp. 23\u201333. ACM\/IEEE, Austin, TX (2017)","DOI":"10.1109\/MODELS.2017.21"},{"issue":"1\u20132","key":"765_CR22","doi-asserted-by":"publisher","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":"765_CR23","doi-asserted-by":"crossref","unstructured":"Kolovos, D.S., Paige, R.F., Polack, F.A.: The Epsilon transformation language. In: 1st International Conference on Model Transformations, pp. 46\u201360. Springer, Z\u00fcrich (2008)","DOI":"10.1007\/978-3-540-69927-9_4"},{"issue":"1","key":"765_CR24","doi-asserted-by":"publisher","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 Asp. Comput. 27(1), 193\u2013235 (2014)","journal-title":"Formal Asp. Comput."},{"issue":"1","key":"765_CR25","doi-asserted-by":"publisher","first-page":"42","DOI":"10.1145\/1111320.1111042","volume":"41","author":"X Leroy","year":"2006","unstructured":"Leroy, X.: Formal certification of a compiler back-end or: programming a compiler with a proof assistant. SIGPLAN Not. 41(1), 42\u201354 (2006)","journal-title":"SIGPLAN Not."},{"issue":"10","key":"765_CR26","doi-asserted-by":"publisher","first-page":"40","DOI":"10.1109\/2.161279","volume":"25","author":"B Meyer","year":"1992","unstructured":"Meyer, B.: Applying design by contract. Computer 25(10), 40\u201351 (1992)","journal-title":"Computer"},{"key":"765_CR27","doi-asserted-by":"crossref","unstructured":"Oakes, B.J., Troya, J., L\u00facio, L., Wimmer, M.: Fully verifying transformation contracts for declarative ATL. In: 18th ACM\/IEEE International Conference on Model Driven Engineering Languages and Systems, pp. 256\u2013265. IEEE, Ottawa, ON (2015)","DOI":"10.1109\/MODELS.2015.7338256"},{"key":"765_CR28","first-page":"133","volume":"39","author":"C Picard","year":"2011","unstructured":"Picard, C., Matthes, R.: Coinductive graph representation: the problem of embedded lists. Electron. Commun. EASST 39, 133\u2013147 (2011)","journal-title":"Electron. Commun. EASST"},{"key":"765_CR29","unstructured":"Pierce, B.C., de\u00a0Amorim, A.A., Casinghino, C., Gaboardi, M., Greenberg, M., Hri\u0163cu, C., Sj\u00f6berg, V., Yorgey, B.: Software Foundations. Electronic textbook (2017)"},{"key":"765_CR30","doi-asserted-by":"publisher","first-page":"56","DOI":"10.1007\/978-3-642-16901-4_6","volume-title":"Formal Methods and Software Engineering","author":"Iman Poernomo","year":"2010","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 (2010)"},{"key":"765_CR31","doi-asserted-by":"publisher","first-page":"90","DOI":"10.1007\/978-3-642-31491-9_9","volume-title":"Modelling Foundations and Applications","author":"Gehan M. K. Selim","year":"2012","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 (2012)"},{"key":"765_CR32","doi-asserted-by":"publisher","first-page":"981","DOI":"10.1007\/s10270-013-0351-7","volume":"14","author":"K Stenzel","year":"2015","unstructured":"Stenzel, K., Moebius, N., Reif, W.: Formal verification of QVT transformations for code generation. Softw. Syst. Model. 14, 981\u20131002 (2015)","journal-title":"Softw. Syst. Model."},{"key":"765_CR33","doi-asserted-by":"publisher","first-page":"446","DOI":"10.1007\/978-3-540-25959-6_35","volume-title":"Applications of Graph Transformations with Industrial Relevance","author":"Gabriele Taentzer","year":"2004","unstructured":"Taentzer, G.: AGG: A graph transformation environment for modeling and validation of software. In: 2nd International Workshop on Applications of Graph Transformations with Industrial Relevance, pp. 446\u2013453 (2003)"},{"key":"765_CR34","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1007\/978-3-319-93317-7_7","volume-title":"Theory and Practice of Model Transformation","author":"Massimo Tisi","year":"2018","unstructured":"Tisi, M., Cheng, Z.: Coqtl: An internal DSL for model transformation in coq. In: 11th International Conference on Model Transformation, pp. 142\u2013156. Springer, Toulouse (2018)"},{"key":"765_CR35","doi-asserted-by":"publisher","first-page":"32","DOI":"10.1007\/978-3-642-24485-8_4","volume-title":"Model Driven Engineering Languages and Systems","author":"Massimo Tisi","year":"2011","unstructured":"Tisi, M., Perez, S.M., Jouault, F., Cabot, J.: Lazy execution of model-to-model transformations. In: 14th International Conference on Model Driven Engineering Languages and Systems, pp. 32\u201346. ACM\/IEEE, Wellington (2011)"},{"issue":"3","key":"765_CR36","doi-asserted-by":"publisher","first-page":"214","DOI":"10.1016\/j.scico.2007.05.004","volume":"68","author":"D Varr\u00f3","year":"2007","unstructured":"Varr\u00f3, D., Balogh, A.: The model transformation language of the VIATRA2 framework. Sci. Comput. Program. 68(3), 214\u2013234 (2007)","journal-title":"Sci. Comput. Program."},{"key":"765_CR37","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1016\/j.entcs.2005.10.025","volume":"152","author":"Gergely Varr\u00f3","year":"2006","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 (2006)","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"765_CR38","unstructured":"Wagelaar, D.: Using ATL\/EMFTVM for import\/export of medical data. In: 2nd Software Development Automation Conference, Amsterdam, Netherlands (2014)"},{"key":"765_CR39","first-page":"530","volume-title":"Lecture Notes in Computer Science","author":"Benjamin Werner","year":"1997","unstructured":"Werner, B.: Sets in types, types in sets. In: Proceedings of TACS\u201997, pp. 530\u2013546. Springer, Berlin (1997)"},{"key":"765_CR40","doi-asserted-by":"publisher","first-page":"58","DOI":"10.1007\/978-3-642-38883-5_8","volume-title":"Theory and Practice of Model Transformations","author":"Edward Willink","year":"2013","unstructured":"Willink, E., Hoyos, H., Kolovos, D.: Yet another three QVT languages. In: 6th International Conference of Model Transformations, pp. 58\u201359. Springer, Budapest (2013)"},{"key":"765_CR41","doi-asserted-by":"publisher","first-page":"42","DOI":"10.1016\/j.jss.2014.02.058","volume":"93","author":"Z Yang","year":"2014","unstructured":"Yang, Z., Hu, K., Ma, D., Bodeveix, J.P., Pi, L., Talpin, J.P.: From AADL to timed abstract state machines: a verified model transformation. J. Syst. Softw. 93, 42\u201368 (2014)","journal-title":"J. Syst. Softw."}],"container-title":["Software and Systems Modeling"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-019-00765-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10270-019-00765-6\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-019-00765-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,15]],"date-time":"2020-11-15T00:27:19Z","timestamp":1605400039000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10270-019-00765-6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,11,16]]},"references-count":41,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2020,3]]}},"alternative-id":["765"],"URL":"https:\/\/doi.org\/10.1007\/s10270-019-00765-6","relation":{},"ISSN":["1619-1366","1619-1374"],"issn-type":[{"value":"1619-1366","type":"print"},{"value":"1619-1374","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,11,16]]},"assertion":[{"value":"16 December 2018","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"31 July 2019","order":2,"name":"revised","label":"Revised","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"16 October 2019","order":3,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"16 November 2019","order":4,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}