{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,28]],"date-time":"2025-03-28T10:30:51Z","timestamp":1743157851538,"version":"3.40.3"},"publisher-location":"Cham","reference-count":15,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319211541"},{"type":"electronic","value":"9783319211558"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-21155-8_11","type":"book-chapter","created":{"date-parts":[[2015,7,15]],"date-time":"2015-07-15T03:50:45Z","timestamp":1436932245000},"page":"133-148","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":13,"title":["A Sound Execution Semantics for ATL via Translation Validation"],"prefix":"10.1007","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":[[2015,7,16]]},"reference":[{"key":"11_CR1","unstructured":"Ab.Rahim, L., Whittle, J.: A survey of approaches for verifying model transformations. Soft. Syst. Modeling (2015) (to appear)"},{"key":"11_CR2","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-84882-745-5","volume-title":"Verification of Sequential and Concurrent Programs","author":"KR Apt","year":"2009","unstructured":"Apt, K.R., de Boer, F.S., Olderog, E.R.: Verification of Sequential and Concurrent Programs, 3rd edn. Springer, Berlin (2009)","edition":"3"},{"key":"11_CR3","unstructured":"ATLAS Group: Specification of the ATL virtual machine. Technical report, Lina & INRIA Nantes (2005)"},{"key":"11_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1007\/11804192_17","volume-title":"Formal Methods for Components and Objects","author":"M Barnett","year":"2006","unstructured":"Barnett, M., Chang, B.-Y.E., DeLine, R., Jacobs, B., M. Leino, K.R.: Boogie: a modular reusable verifier for object-oriented programs. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol. 4111, pp. 364\u2013387. Springer, Heidelberg (2006)"},{"key":"11_CR5","series-title":"Lecture Notes in Computer Science","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":"F B\u00fcttner","year":"2012","unstructured":"B\u00fcttner, F., Egea, M., Cabot, J.: On verifying ATL transformations using \u2018off-the-shelf\u2019 SMT solvers. In: France, R.B., Kazmeier, J., Breu, R., Atkinson, C. (eds.) MODELS 2012. LNCS, vol. 7590, pp. 432\u2013448. Springer, Heidelberg (2012)"},{"key":"11_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"112","DOI":"10.1007\/978-3-642-19829-8_8","volume-title":"Formal Methods: Foundations and Applications","author":"D Calegari","year":"2011","unstructured":"Calegari, D., Luna, C., Szasz, N., Tasistro, \u00c1.: A type-theoretic framework for certified model transformations. In: Davies, J. (ed.) SBMF 2010. LNCS, vol. 6527, pp. 112\u2013127. Springer, Heidelberg (2011)"},{"key":"11_CR7","unstructured":"Cheng, Z., Monahan, R., Power, J.F.: Online repository for VeriATL system (2013). https:\/\/github.com\/veriatl\/veriatl"},{"issue":"9","key":"11_CR8","doi-asserted-by":"publisher","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 - an instrumented approach for model verification. J. Softw. 4(9), 943\u2013958 (2009)","journal-title":"J. Softw."},{"issue":"1\u20132","key":"11_CR9","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."},{"issue":"1","key":"11_CR10","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., Kolahdouz-Rahimi, S.: A framework for model transformation verification. Formal Aspects Comput. 27(1), 193\u2013235 (2015)","journal-title":"Formal Aspects Comput."},{"key":"11_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1007\/978-3-642-17511-4_20","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"KRM Leino","year":"2010","unstructured":"Leino, K.R.M.: Dafny: an automatic program verifier for functional correctness. In: Clarke, E.M., Voronkov, A. (eds.) LPAR-16 2010. LNCS, vol. 6355, pp. 348\u2013370. Springer, Heidelberg (2010)"},{"issue":"1","key":"11_CR12","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."},{"key":"11_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"136","DOI":"10.1007\/978-3-642-16145-2_10","volume-title":"Model Driven Engineering Languages and Systems","author":"L L\u00facio","year":"2010","unstructured":"L\u00facio, L., Barroca, B., Amaral, V.: A technique for automatic validation of model transformations. In: Petriu, D.C., Rouquette, N., Haugen, \u00d8. (eds.) MODELS 2010, Part I. LNCS, vol. 6394, pp. 136\u2013150. Springer, Heidelberg (2010)"},{"key":"11_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"214","DOI":"10.1007\/978-3-540-69927-9_15","volume-title":"Theory and Practice of Model Transformations","author":"IH Poernomo","year":"2008","unstructured":"Poernomo, I.H.: Proofs-as-model-transformations. In: Vallecillo, A., Gray, J., Pierantonio, A. (eds.) ICMT 2008. LNCS, vol. 5063, pp. 214\u2013228. Springer, Heidelberg (2008)"},{"issue":"5","key":"11_CR15","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."}],"container-title":["Lecture Notes in Computer Science","Theory and Practice of Model Transformations"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-21155-8_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,15]],"date-time":"2023-02-15T13:02:11Z","timestamp":1676466131000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-21155-8_11"}},"subtitle":["Research Paper"],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319211541","9783319211558"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-21155-8_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"16 July 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}