{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,27]],"date-time":"2026-09-27T14:37:42Z","timestamp":1790519862421,"version":"4.1.0"},"reference-count":52,"publisher":"Springer Science and Business Media LLC","issue":"5","license":[{"start":{"date-parts":[[2022,5,3]],"date-time":"2022-05-03T00:00:00Z","timestamp":1651536000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2022,5,3]],"date-time":"2022-05-03T00:00:00Z","timestamp":1651536000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Softw Syst Model"],"published-print":{"date-parts":[[2022,10]]},"DOI":"10.1007\/s10270-022-01004-1","type":"journal-article","created":{"date-parts":[[2022,5,3]],"date-time":"2022-05-03T07:03:57Z","timestamp":1651561437000},"page":"1831-1852","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Deep specification and proof preservation for the CoqTL transformation language"],"prefix":"10.1007","volume":"21","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-6361-1103","authenticated-orcid":false,"given":"Zheng","family":"Cheng","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Massimo","family":"Tisi","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2022,5,3]]},"reference":[{"issue":"2","key":"1004_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":"2104","key":"1004_CR2","doi-asserted-by":"publisher","first-page":"20160331","DOI":"10.1098\/rsta.2016.0331","volume":"375","author":"AW Appel","year":"2017","unstructured":"Appel, A.W., Beringer, L., Chlipala, A., Pierce, B.C., Shao, Z., Weirich, S., Zdancewic, S.: Position paper: the science of deep specification. Philos. Trans. R. Soc. A Math. Phys. Eng. Sci. 375(2104), 20160331 (2017)","journal-title":"Philos. Trans. R. Soc. A Math. Phys. Eng. Sci."},{"key":"1004_CR3","unstructured":"ATLAS Group: Specification of the ATL virtual machine. Technical report, Lina & INRIA Nantes (2005)"},{"issue":"6","key":"1004_CR4","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":"1004_CR5","doi-asserted-by":"crossref","unstructured":"Benzaken, V., Contejean, E.: A Coq mechanised formal semantics for realistic SQL queries: formally reconciling SQL and bag relational algebra. In: 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, pp. 249\u2013261. ACM, Cascais (2019)","DOI":"10.1145\/3293880.3294107"},{"key":"1004_CR6","doi-asserted-by":"crossref","unstructured":"Benzaken, V., Contejean, E., Keller, C., Martins, E.: A Coq formalisation of SQL\u2019s execution engines. In: 9th International Conference on Interactive Theorem Proving, pp. 88\u2013107. Springer, Oxford (2018)","DOI":"10.1007\/978-3-319-94821-8_6"},{"key":"1004_CR7","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"},{"key":"1004_CR8","doi-asserted-by":"crossref","unstructured":"Bodin, M., Chargueraud, A., Filaretti, D., Gardner, P., Maffeis, S., Naudziuniene, D., Schmitt, A., Smith, G.: A trusted mechanised JavaScript specification. In: 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 87\u2013100. ACM, San Diego (2014)","DOI":"10.1145\/2535838.2535876"},{"key":"1004_CR9","doi-asserted-by":"crossref","unstructured":"Boronat, A.: Experimentation with a big-step semantics for ATL model transformations. In: 10th International Conference on Theory and Practice of Model Transformations, pp. 3\u201318. Springer, Marburg (2017)","DOI":"10.1007\/978-3-319-61473-1_1"},{"issue":"5","key":"1004_CR10","doi-asserted-by":"publisher","first-page":"490","DOI":"10.1109\/TSE.2014.2375201","volume":"41","author":"L Burgue\u00f1o","year":"2014","unstructured":"Burgue\u00f1o, L., Troya, J., Wimmer, M., Vallecillo, A.: Static fault localization in model transformations. IEEE Trans. Software Eng. 41(5), 490\u2013506 (2014)","journal-title":"IEEE Trans. Software Eng."},{"key":"1004_CR11","doi-asserted-by":"crossref","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)","DOI":"10.1007\/978-3-642-33666-9_28"},{"key":"1004_CR12","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 (2012)","DOI":"10.1007\/978-3-642-34281-3_16"},{"key":"1004_CR13","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 (2011)","DOI":"10.1007\/978-3-642-19829-8_8"},{"key":"1004_CR14","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 (2015)","DOI":"10.1007\/978-3-319-21155-8_11"},{"issue":"4","key":"1004_CR15","doi-asserted-by":"publisher","first-page":"1197","DOI":"10.1007\/s10270-016-0553-x","volume":"17","author":"Z Cheng","year":"2018","unstructured":"Cheng, Z., Monahan, R., Power, J.F.: Formalised EMFTVM bytecode language for sound verification of model transformations. Softw. Syst. Model. 17(4), 1197\u20131225 (2018)","journal-title":"Softw. Syst. Model."},{"key":"1004_CR16","doi-asserted-by":"crossref","unstructured":"Cheng, Z., Tisi, M.: A deductive approach for fault localization in ATL model transformations. In: 20th International Conference on Fundamental Approaches to Software Engineering, pp. 300\u2013317. Springer, Uppsala (2017)","DOI":"10.1007\/978-3-662-54494-5_17"},{"key":"1004_CR17","doi-asserted-by":"crossref","unstructured":"Cheng, Z., Tisi, M.: Incremental deductive verification for relational model transformations. In: 10th IEEE International Conference on Software Testing, Verification and Validation, no. 379\u2013389. IEEE, Tokyo (2017)","DOI":"10.1109\/ICST.2017.41"},{"issue":"6","key":"1004_CR18","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."},{"issue":"2","key":"1004_CR19","doi-asserted-by":"publisher","first-page":"425","DOI":"10.1007\/s10270-019-00765-6","volume":"19","author":"Z Cheng","year":"2020","unstructured":"Cheng, Z., Tisi, M., Douence, R.: CoqTL: a Coq DSL for rule-based model transformation. Softw. Syst. Model. 19(2), 425\u2013439 (2020)","journal-title":"Softw. Syst. Model."},{"key":"1004_CR20","doi-asserted-by":"crossref","unstructured":"Cheng, Z., Tisi, M., Hotonnier, J.: Certifying a rule-based model transformation engine for proof preservation. In: 23rd ACM\/IEEE International Conference on Model Driven Engineering Languages and Systems, pp. 297\u2013307. ACM, Montreal (2020)","DOI":"10.1145\/3365438.3410949"},{"key":"1004_CR21","unstructured":"Chlipala, A., Delaware, B., Duchovni, S., Gross, J., Pit-Claudel, C., Suriyakarn, S., Wang, P., Ye, K.: The end of history? Using a proof assistant to replace language design with library design. In: 2nd Summit on Advances in Programming Languages, no.\u00a03, pp. 1\u201315. Asilomar (2017)"},{"key":"1004_CR22","doi-asserted-by":"crossref","unstructured":"Choi, J., Vijayaraghavan, M., Sherman, B., Chlipala, A.: Kami: a platform for high-level parametric hardware specification and its modular verification. In: Proceedings of the ACM on Programming Languages 1(ICFP), pp. 1\u201330 (2017)","DOI":"10.1145\/3110268"},{"issue":"9","key":"1004_CR23","doi-asserted-by":"publisher","first-page":"868","DOI":"10.1109\/TSE.2016.2635137","volume":"43","author":"JS Cuadrado","year":"2016","unstructured":"Cuadrado, J.S., Guerra, E., de Lara, J.: Static analysis of model transformations. IEEE Trans. Softw. Eng. 43(9), 868\u2013897 (2016)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"1004_CR24","doi-asserted-by":"crossref","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)","DOI":"10.4204\/EPTCS.108.5"},{"issue":"2","key":"1004_CR25","doi-asserted-by":"publisher","first-page":"185","DOI":"10.1007\/s10270-007-0074-8","volume":"8","author":"F Fleurey","year":"2009","unstructured":"Fleurey, F., Baudry, B., Muller, P., Traon, Y.L.: Qualifying input test data for model transformations. Softw. Syst. Model. 8(2), 185\u2013203 (2009)","journal-title":"Softw. Syst. Model."},{"issue":"2","key":"1004_CR26","doi-asserted-by":"publisher","first-page":"623","DOI":"10.1007\/s10270-013-0369-x","volume":"14","author":"E Guerra","year":"2015","unstructured":"Guerra, E., Soeken, M.: Specification-driven model transformation testing. Softw. Syst. Model. 14(2), 623\u2013644 (2015)","journal-title":"Softw. Syst. Model."},{"key":"1004_CR27","doi-asserted-by":"crossref","unstructured":"He, X., Hu, Z.: Putback-based bidirectional model transformations. In: 26th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering, pp. 434\u2013444. ACM (2018)","DOI":"10.1145\/3236024.3236070"},{"key":"1004_CR28","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. IEEE, Austin (2017)","DOI":"10.1109\/MODELS.2017.21"},{"issue":"1\u20132","key":"1004_CR29","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":"1004_CR30","doi-asserted-by":"crossref","unstructured":"Jouault, F., B\u00e9zivin, J.: KM3: a DSL for metamodel specification. In: 8th International Conference on Formal Methods for Open Object-Based Distributed Systems, pp. 171\u2013185. Springer, Bologna (2006)","DOI":"10.1007\/11768869_14"},{"key":"1004_CR31","doi-asserted-by":"crossref","unstructured":"Ko, H.S., Zan, T., Hu, Z.: BiGUL: a formally verified core language for putback-based bidirectional programming. In: ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, pp. 61\u201372. ACM, St. Petersburg (2016)","DOI":"10.1145\/2847538.2847544"},{"key":"1004_CR32","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":"1004_CR33","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 Aspects Comput. 27(1), 193\u2013235 (2014)","journal-title":"Formal Aspects Comput."},{"issue":"7","key":"1004_CR34","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1145\/1538788.1538814","volume":"52","author":"X Leroy","year":"2009","unstructured":"Leroy, X.: Formal verification of a realistic compiler. Commun. ACM 52(7), 107\u2013115 (2009)","journal-title":"Commun. ACM"},{"issue":"C","key":"1004_CR35","doi-asserted-by":"publisher","first-page":"104","DOI":"10.1016\/j.is.2016.06.008","volume":"62","author":"JJ L\u00f3pez-Fern\u00e1ndez","year":"2016","unstructured":"L\u00f3pez-Fern\u00e1ndez, J.J., Guerra, E., de Lara, J.: Combining unit and specification-based testing for meta-model validation and verification. Inf. Syst. 62(C), 104\u2013135 (2016)","journal-title":"Inf. Syst."},{"key":"1004_CR36","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.scico.2016.08.006","volume":"136","author":"S Mart\u00ednez","year":"2017","unstructured":"Mart\u00ednez, S., Tisi, M., Douence, R.: Reactive model transformation with ATL. Sci. Comput. Program. 136, 1\u201316 (2017)","journal-title":"Sci. Comput. Program."},{"key":"1004_CR37","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1016\/j.entcs.2005.10.021","volume":"152","author":"T Mens","year":"2006","unstructured":"Mens, T., Van Gorp, P.: A taxonomy of model transformation. Electron. Notes Theor. Comput. Sci. 152, 125\u2013142 (2006)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"1004_CR38","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 (2015)","DOI":"10.1109\/MODELS.2015.7338256"},{"key":"1004_CR39","unstructured":"Object Management Group: Query\/view\/transformation specification (ver. 1.3). http:\/\/www.omg.org\/spec\/QVT\/1.3\/ (2016)"},{"key":"1004_CR40","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 (2010)","DOI":"10.1007\/978-3-642-16901-4_6"},{"key":"1004_CR41","doi-asserted-by":"crossref","unstructured":"Ringer, T., Yazdani, N., Leo, J., Grossman, D.: Adapting proof automation to adapt proofs. In: 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, pp. 115\u2013129. ACM, Los Angeles (2018)","DOI":"10.1145\/3167094"},{"issue":"6","key":"1004_CR42","doi-asserted-by":"publisher","first-page":"397","DOI":"10.1016\/j.jlap.2010.03.012","volume":"79","author":"G Ro\u015fu","year":"2010","unstructured":"Ro\u015fu, G., \u015eerb\u0103nu\u0163\u0103, T.F.: An overview of the K semantic framework. J. Log. Algebraic Program. 79(6), 397\u2013434 (2010)","journal-title":"J. Log. Algebraic Program."},{"key":"1004_CR43","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 (2012)","DOI":"10.1007\/978-3-642-31491-9_9"},{"key":"1004_CR44","doi-asserted-by":"crossref","unstructured":"Sen, S., Baudry, B., Mottu, J.M.: Automatic model generation strategies for model transformation testing. In: 2nd International Conference on Model Transformations, pp. 148\u2013164. Springer, Zurich (2009)","DOI":"10.1007\/978-3-642-02408-5_11"},{"key":"1004_CR45","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":"1004_CR46","doi-asserted-by":"crossref","unstructured":"Tisi, M., Cheng, Z.: CoqTL: an internal DSL for model transformation in Coq. In: 11th International Conference on Model Transformations, pp. 142\u2013156. Springer, Uppsala (2018)","DOI":"10.1007\/978-3-319-93317-7_7"},{"key":"1004_CR47","doi-asserted-by":"crossref","unstructured":"Tisi, M., Mart\u00ednez, S., 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. Springer, Wellington (2011)","DOI":"10.1007\/978-3-642-24485-8_4"},{"issue":"5","key":"1004_CR48","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."},{"issue":"3","key":"1004_CR49","doi-asserted-by":"publisher","first-page":"313","DOI":"10.1007\/s10270-006-0015-y","volume":"5","author":"G Varr\u00f3","year":"2006","unstructured":"Varr\u00f3, G., Friedl, K., Varr\u00f3, D.: Implementing a graph transformation engine in relational databases. Softw. Syst. Model. 5(3), 313\u2013341 (2006)","journal-title":"Softw. Syst. Model."},{"key":"1004_CR50","unstructured":"Wagelaar, D.: Using ATL\/EMFTVM for import\/export of medical data. In: 2nd Software Development Automation Conference. Amsterdam, Netherlands (2014)"},{"key":"1004_CR51","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 (2011)","DOI":"10.1007\/978-3-642-24485-8_46"},{"key":"1004_CR52","doi-asserted-by":"crossref","unstructured":"Weirich, S., Voizard, A., de\u00a0Amorim, P.H.A., Eisenberg, R.A.: A specification for dependent types in Haskell. Proceedings of the ACM on Programming Languages 1(ICFP) (2017)","DOI":"10.1145\/3110275"}],"container-title":["Software and Systems Modeling"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-022-01004-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10270-022-01004-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-022-01004-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,9,30]],"date-time":"2022-09-30T10:22:52Z","timestamp":1664533372000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10270-022-01004-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,5,3]]},"references-count":52,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2022,10]]}},"alternative-id":["1004"],"URL":"https:\/\/doi.org\/10.1007\/s10270-022-01004-1","relation":{},"ISSN":["1619-1366","1619-1374"],"issn-type":[{"value":"1619-1366","type":"print"},{"value":"1619-1374","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,5,3]]},"assertion":[{"value":"8 March 2021","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"18 March 2022","order":2,"name":"revised","label":"Revised","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"28 March 2022","order":3,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"3 May 2022","order":4,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}