{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T04:11:50Z","timestamp":1751602310436,"version":"3.41.0"},"reference-count":44,"publisher":"Springer Science and Business Media LLC","issue":"6","license":[{"start":{"date-parts":[[2018,4,17]],"date-time":"2018-04-17T00:00:00Z","timestamp":1523923200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2018,11]]},"DOI":"10.1007\/s10009-018-0491-8","type":"journal-article","created":{"date-parts":[[2018,4,17]],"date-time":"2018-04-17T15:12:44Z","timestamp":1523977964000},"page":"645-663","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":9,"title":["Slicing ATL model transformations for scalable deductive verification and fault localization"],"prefix":"10.1007","volume":"20","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"}]}],"member":"297","published-online":{"date-parts":[[2018,4,17]]},"reference":[{"issue":"2","key":"491_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":"491_CR2","doi-asserted-by":"publisher","first-page":"447","DOI":"10.1007\/s10009-010-0145-y","volume":"12","author":"JR Abrial","year":"2010","unstructured":"Abrial, J.R., Butler, M., Hallerstede, S., Hoang, T.S., Mehta, F., Voisin, L.: Rodin: an open toolset for modelling and reasoning in Event-B. Int. J. Softw. Tools Technol. Transf. 12(6), 447\u2013466 (2010)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"491_CR3","doi-asserted-by":"crossref","unstructured":"Aranega, V., Mottu, J., Etien, A., Dekeyser, J.: Traceability mechanism for error localization in model transformation. In: 4th International Conference on Software and Data Technologies, pp. 66\u201373. Sofia, Bulgaria (2009)","DOI":"10.5220\/0002264700660073"},{"key":"491_CR4","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1007\/11804192_17","volume-title":"Formal Methods for Components and Objects","author":"Mike Barnett","year":"2006","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)"},{"key":"491_CR5","doi-asserted-by":"crossref","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, China (2004)","DOI":"10.1109\/SEFM.2004.1347524"},{"key":"491_CR6","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":"491_CR7","volume-title":"Interactive Theorem Proving and Program Development: Coq\u2019Art The Calculus of Inductive Constructions","author":"Y Bertot","year":"2010","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development: Coq\u2019Art The Calculus of Inductive Constructions, 1st edn. Springer, Berlin (2010)","edition":"1"},{"key":"491_CR8","unstructured":"Briand, L.C.: Making model-driven verification practical and scalable\u2014experiences and lessons learned. In: 4th International Conference on Model-Driven Engineering and Software Development. SCITEPRESS, Rome, Italy (2016)"},{"issue":"5","key":"491_CR9","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":"491_CR10","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, Austria (2012)"},{"key":"491_CR11","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, Japan (2012)"},{"key":"491_CR12","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, Brazil (2011)"},{"key":"491_CR13","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, Italy (2015)"},{"issue":"4","key":"491_CR14","doi-asserted-by":"publisher","first-page":"1197","DOI":"10.1007\/s10270-016-0553-x","volume":"17","author":"Zheng Cheng","year":"2016","unstructured":"Cheng, Z., Monahan, R., Power, J.F.: Formalised EMFTVM bytecode language for sound verification of model transformations. Softw. Syst. Model. (2016). https:\/\/doi.org\/10.1007\/s10270-016-0553-x","journal-title":"Software & Systems Modeling"},{"key":"491_CR15","doi-asserted-by":"publisher","first-page":"300","DOI":"10.1007\/978-3-662-54494-5_17","volume-title":"Fundamental Approaches to Software Engineering","author":"Zheng Cheng","year":"2017","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, Sweden (2017)"},{"issue":"4","key":"491_CR16","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1145\/1988042.1988046","volume":"46","author":"K Claessen","year":"2011","unstructured":"Claessen, K., Hughes, J.: QuickCheck: a lightweight tool for random testing of Haskell programs. ACM SIGPLAN Not. 46(4), 53\u201364 (2011)","journal-title":"ACM SIGPLAN Not."},{"key":"491_CR17","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, Italy (2014)","DOI":"10.1109\/ISSRE.2014.10"},{"key":"491_CR18","doi-asserted-by":"crossref","unstructured":"Cuadrado, J.S., Guerra, E., de\u00a0Lara, J., Claris\u00f3, R., Cabot, J.: Translating target to source constraints in model-to-model transformations. In: 20th ACM\/IEEE International Conference on Model Driven Engineering Languages and Systems, pp. 12\u201322. IEEE, Austin, TX, USA (2017)","DOI":"10.1109\/MODELS.2017.12"},{"key":"491_CR19","doi-asserted-by":"crossref","unstructured":"Filli\u00e2tre, J.C., Paskevich, A.: Why3\u2014where 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"},{"issue":"1","key":"491_CR20","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1016\/S0164-1212(02)00135-8","volume":"68","author":"M Harman","year":"2003","unstructured":"Harman, M., Binkley, D., Danicic, S.: Amorphous program slicing. J. Syst. Softw. 68(1), 45\u201364 (2003)","journal-title":"J. Syst. Softw."},{"issue":"3","key":"491_CR21","doi-asserted-by":"publisher","first-page":"16:1","DOI":"10.1145\/2187671.2187678","volume":"44","author":"J Hatcliff","year":"2012","unstructured":"Hatcliff, J., Leavens, G.T., Leino, K.R.M., M\u00fcller, P., Parkinson, M.J.: Behavioral interface specification languages. ACM Comput. Surv. 44(3), 16:1\u201316:58 (2012)","journal-title":"ACM Comput. Surv."},{"key":"491_CR22","doi-asserted-by":"crossref","unstructured":"Hidaka, S., Jouault, F., Tisi, M.: On additivity in transformation languages. In: 2017 ACM\/IEEE 20th International Conference on Model Driven Engineering Languages and Systems, pp. 23\u201333. IEEE, Austin, TX, USA (2017)","DOI":"10.1109\/MODELS.2017.21"},{"issue":"10","key":"491_CR23","doi-asserted-by":"publisher","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":"491_CR24","unstructured":"Howard, W.A.: The formulae-as-types notion of construction. In: To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pp. 479\u2013490. Academic Press (1980)"},{"key":"491_CR25","doi-asserted-by":"publisher","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)"},{"issue":"5","key":"491_CR26","doi-asserted-by":"publisher","first-page":"649","DOI":"10.1109\/TSE.2010.62","volume":"37","author":"Y Jia","year":"2011","unstructured":"Jia, Y., Harman, M.: An analysis and survey of the development of mutation testing. IEEE Trans. Softw. Eng. 37(5), 649\u2013678 (2011)","journal-title":"IEEE Trans. Softw. Eng."},{"issue":"1\u20132","key":"491_CR27","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":"491_CR28","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/978-3-319-42064-6_12","volume-title":"Theory and Practice of Model Transformations","author":"Timo Kehrer","year":"2016","unstructured":"Kehrer, T., Taentzer, G., Rindt, M., Kelter, U.: Automatically deriving the specification of model editing operations from meta-models. In: 9th International Conference on Model Transformation, pp. 173\u2013188. Springer, Vienna, Austria (2016)"},{"issue":"1","key":"491_CR29","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. Form. Asp. Comput. 27(1), 193\u2013235 (2014)","journal-title":"Form. Asp. Comput."},{"key":"491_CR30","unstructured":"Leino, K.R.M., Moskal, M., Schulte, W.: Verification condition splitting. https:\/\/www.microsoft.com\/en-us\/research\/publication\/verification-condition-splitting\/ (2008)"},{"key":"491_CR31","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"},{"key":"491_CR32","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":"491_CR33","unstructured":"Object Management Group: Unified modeling language (ver. 2.5). http:\/\/www.omg.org\/spec\/UML\/2.5\/ (2015)"},{"key":"491_CR34","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":"491_CR35","doi-asserted-by":"publisher","first-page":"156","DOI":"10.1007\/s10009-004-0183-4","volume":"7","author":"MR Prasad","year":"2005","unstructured":"Prasad, M.R., Biere, A., Gupta, A.: A survey of recent advances in SAT-based formal verification. Int. J. Softw. Tools Technol. Transf. 7(2), 156\u2013173 (2005)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"491_CR36","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1007\/978-3-319-21145-9_10","volume-title":"Graph Transformation","author":"Hendrik Radke","year":"2015","unstructured":"Radke, H., Arendt, T., Becker, J.S., Habel, A., Taentzer, G.: Translating essential OCL invariants to nested graph constraints focusing on set operations. In: 8th International Conference on Graph Transformation, pp. 155\u2013170. Springer, L\u2019Aquila, Italy (2015)"},{"key":"491_CR37","doi-asserted-by":"publisher","first-page":"68","DOI":"10.1145\/2856103","volume":"59","author":"A Roychoudhury","year":"2016","unstructured":"Roychoudhury, A., Chandra, S.: Formula-based software debugging. Commun. ACM 59, 68\u201377 (2016)","journal-title":"Commun. ACM"},{"key":"491_CR38","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, Denmark (2012)"},{"key":"491_CR39","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"},{"key":"491_CR40","unstructured":"Tip, F.: A survey of program slicing techniques. Tech. rep., Centrum Wiskunde & Informatica (1994)"},{"key":"491_CR41","first-page":"656","volume-title":"Lecture Notes in Computer Science","author":"Massimo Tisi","year":"2013","unstructured":"Tisi, M., Perez, S.M., Choura, H.: Parallel execution of ATL transformation rules. In: 16th International Conference on Model-Driven Engineering Languages and Systems, pp. 656\u2013672. Springer, Miami, FL, USA (2013)"},{"key":"491_CR42","unstructured":"Wagelaar, D.: Using ATL\/EMFTVM for import\/export of medical data. In: 2nd Software Development Automation Conference. Amsterdam, Netherlands (2014)"},{"key":"491_CR43","unstructured":"Weiser, M.: Program slicing. In: 5th International Conference on Software Engineering, pp. 439\u2013449. IEEE, NJ, USA (1981)"},{"key":"491_CR44","first-page":"1","volume":"99","author":"WE Wong","year":"2016","unstructured":"Wong, W.E., Gao, R., Li, Y., Abreu, R., Wotawa, F.: A survey on software fault localization. IEEE Trans. Softw. Eng. Pre-Print 99, 1\u201341 (2016)","journal-title":"IEEE Trans. Softw. Eng. Pre-Print"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-018-0491-8\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-018-0491-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-018-0491-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,3]],"date-time":"2025-07-03T18:50:23Z","timestamp":1751568623000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-018-0491-8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,4,17]]},"references-count":44,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2018,11]]}},"alternative-id":["491"],"URL":"https:\/\/doi.org\/10.1007\/s10009-018-0491-8","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"type":"print","value":"1433-2779"},{"type":"electronic","value":"1433-2787"}],"subject":[],"published":{"date-parts":[[2018,4,17]]},"assertion":[{"value":"17 April 2018","order":1,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}