{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,4,6]],"date-time":"2024-04-06T02:15:09Z","timestamp":1712369709160},"reference-count":34,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2013,2,27]],"date-time":"2013-02-27T00:00:00Z","timestamp":1361923200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Softw Syst Model"],"published-print":{"date-parts":[[2015,2]]},"DOI":"10.1007\/s10270-013-0315-y","type":"journal-article","created":{"date-parts":[[2013,2,26]],"date-time":"2013-02-26T16:12:33Z","timestamp":1361895153000},"page":"271-285","source":"Crossref","is-referenced-by-count":6,"title":["Automatically reasoning about metamodeling"],"prefix":"10.1007","volume":"14","author":[{"given":"Ethan K.","family":"Jackson","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tihamer","family":"Levendovszky","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Daniel","family":"Balasubramanian","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2013,2,27]]},"reference":[{"key":"315_CR1","doi-asserted-by":"crossref","unstructured":"Clark, T., Evans, A., Kent, S.: The metamodelling language calculus: foundation semantics for UML. In: FASE, pp. 17\u201331 (2001)","DOI":"10.1007\/3-540-45314-8_3"},{"key":"315_CR2","doi-asserted-by":"crossref","unstructured":"Jouault, F., B\u00e9zivin, J.: KM3: a DSL for metamodel specification. In: FMOODS, pp. 171\u2013185 (2006)","DOI":"10.1007\/11768869_14"},{"issue":"3","key":"315_CR3","doi-asserted-by":"crossref","first-page":"187","DOI":"10.1007\/s10270-003-0028-8","volume":"2","author":"D Varr\u00f3","year":"2003","unstructured":"Varr\u00f3, D., Pataricza, A.: VPM: a visual, precise and multilevel metamodeling framework for describing mathematical domains and UML. J. Softw. Syst. Model. 2(3), 187\u2013210 (2003)","journal-title":"J. Softw. Syst. Model."},{"issue":"1","key":"315_CR4","doi-asserted-by":"crossref","first-page":"103","DOI":"10.1007\/s10270-007-0049-9","volume":"7","author":"M Alanen","year":"2008","unstructured":"Alanen, M., Porres, I.: A metamodeling language supporting subset and union properties. Softw. Syst. Model. 7(1), 103\u2013124 (2008)","journal-title":"Softw. Syst. Model."},{"issue":"3\u20134","key":"315_CR5","doi-asserted-by":"crossref","first-page":"269","DOI":"10.1007\/s00165-009-0140-9","volume":"22","author":"A Boronat","year":"2010","unstructured":"Boronat, A., Meseguer, J.: An algebraic semantics for MOF. Formal Asp. Comput. 22(3\u20134), 269\u2013296 (2010)","journal-title":"Formal Asp. Comput."},{"key":"315_CR6","doi-asserted-by":"crossref","unstructured":"Jackson, E.K., Kang, E., Dahlweid, M., Seifert, D., Santen, T.: Components, platforms and possibilities: towards generic automation for MDA. In: EMSOFT, pp. 39\u201348 (2010)","DOI":"10.1145\/1879021.1879027"},{"key":"315_CR7","doi-asserted-by":"crossref","unstructured":"Jackson, E.K., Levendovszky, T., Balasubramanian, D.: Reasoning about metamodeling with formal specifications and automatic proofs. In: MoDELS, pp. 653\u2013667 (2011)","DOI":"10.1007\/978-3-642-24485-8_48"},{"key":"315_CR8","volume-title":"Fundamentals of algebraic graph transformation (monographs in theoretical computer science). An EACTS series","author":"H Ehrig","year":"2006","unstructured":"Ehrig, H., Ehrig, K., Prange, U., Taentzer, G.: Fundamentals of algebraic graph transformation (monographs in theoretical computer science). An EACTS series. Springer, New York (2006)"},{"key":"315_CR9","doi-asserted-by":"crossref","unstructured":"Atkinson, C., K\u00fchne, T.: The essence of multilevel metamodeling. In: UML, pp. 19\u201333 (2001)","DOI":"10.1007\/3-540-45441-1_3"},{"issue":"3","key":"315_CR10","doi-asserted-by":"crossref","first-page":"374","DOI":"10.1145\/502807.502810","volume":"33","author":"E Dantsin","year":"2001","unstructured":"Dantsin, E., Eiter, T., Gottlob, G., Voronkov, A.: Complexity and expressive power of logic programming. ACM Comput. Surv. 33(3), 374\u2013425 (2001)","journal-title":"ACM Comput. Surv."},{"issue":"2","key":"315_CR11","doi-asserted-by":"crossref","first-page":"187","DOI":"10.1016\/S0304-3975(01)00359-0","volume":"285","author":"M Clavel","year":"2002","unstructured":"Clavel, M., Dur\u00e1n, F., Eker, S., Lincoln, P., Mart\u00ed-Oliet, N., Meseguer, J., Quesada, J.F.: Maude: specification and programming in rewriting logic. Theor. Comput. Sci. 285(2), 187\u2013243 (2002)","journal-title":"Theor. Comput. Sci."},{"issue":"2","key":"315_CR12","doi-asserted-by":"crossref","first-page":"85","DOI":"10.1007\/s10270-003-0050-x","volume":"3","author":"D Varr\u00f3","year":"2004","unstructured":"Varr\u00f3, D.: Automated formal verification of visual modeling languages by model checking. Softw. Syst. Model. 3(2), 85\u2013113 (2004)","journal-title":"Softw. Syst. Model."},{"key":"315_CR13","doi-asserted-by":"crossref","unstructured":"Anastasakis, K., Bordbar, B., Georg, G., Ray, I.: UML2Alloy: a challenging model transformation. In: MODELS, pp. 436\u2013450 (2007)","DOI":"10.1007\/978-3-540-75209-7_30"},{"key":"315_CR14","doi-asserted-by":"crossref","unstructured":"Torlak, E., Jackson, D.: Kodkod: a relational model finder. In: TACAS, pp. 632\u2013647 (2007)","DOI":"10.1007\/978-3-540-71209-1_49"},{"key":"315_CR15","doi-asserted-by":"crossref","unstructured":"Kuhlmann, M., Gogolla, M.: From uml and ocl to relational logic and back. In: MoDELS, pp. 415\u2013431 (2012)","DOI":"10.1007\/978-3-642-33666-9_27"},{"key":"315_CR16","doi-asserted-by":"crossref","unstructured":"Kuhlmann, M., Gogolla, M.: Strengthening sat-based validation of uml\/ocl models by representing collections as relations. In: ECMFA, pp. 32\u201348 (2012)","DOI":"10.1007\/978-3-642-31491-9_5"},{"key":"315_CR17","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: ICFEM, pp. 198\u2013213 (2012)","DOI":"10.1007\/978-3-642-34281-3_16"},{"issue":"2","key":"315_CR18","doi-asserted-by":"crossref","first-page":"283","DOI":"10.1016\/j.jss.2009.08.012","volume":"83","author":"J Cabot","year":"2010","unstructured":"Cabot, J., Claris\u00f3, R., Guerra, E., de Lara, J.: Verification and validation of declarative model-to-model transformations through invariants. J. Syst. Softw. 83(2), 283\u2013302 (2010)","journal-title":"J. Syst. Softw."},{"key":"315_CR19","doi-asserted-by":"crossref","unstructured":"Balaban, M., Kifer, M.: Logic-based model-level software development with f-oml. In: MoDELS, pp. 517\u2013532 (2011)","DOI":"10.1007\/978-3-642-24485-8_38"},{"key":"315_CR20","doi-asserted-by":"crossref","unstructured":"Gurevich, Y., Neeman, I.: Dkal: distributed-knowledge authorization language. In: CSF, pp. 149\u2013162 (2008)","DOI":"10.1109\/CSF.2008.8"},{"key":"315_CR21","doi-asserted-by":"crossref","unstructured":"Alvaro, P., Condie, T., Conway, N., Elmeleegy, K., Hellerstein, J.M., Sears, R.: Boom analytics: exploring data-centric, declarative programming for the cloud. In: EuroSys, pp. 223\u2013236 (2010)","DOI":"10.1145\/1755913.1755937"},{"key":"315_CR22","doi-asserted-by":"crossref","unstructured":"de Moura, L.M., Bj\u00f8rner, N.: Z3: An efficient smt solver. In: TACAS, pp. 337\u2013340 (2008)","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"315_CR23","doi-asserted-by":"crossref","unstructured":"B\u00fcttner, F., Egea, M., Cabot, J.: On verifying atl transformations using \u2019off-the-shelf\u2019 smt solvers. In: MoDELS, pp. 432\u2013448 (2012)","DOI":"10.1007\/978-3-642-33666-9_28"},{"issue":"4","key":"315_CR24","doi-asserted-by":"crossref","first-page":"479","DOI":"10.1007\/s10270-008-0095-y","volume":"8","author":"K Ehrig","year":"2009","unstructured":"Ehrig, K., K\u00fcster, J.M., Taentzer, G.: Generating instance models from meta models. Softw. Syst. Model. 8(4), 479\u2013500 (2009)","journal-title":"Softw. Syst. Model."},{"key":"315_CR25","doi-asserted-by":"crossref","unstructured":"Gr\u00f6nniger, H., Ringert, J.O., Rumpe, B.: System model-based definition of modeling language semantics. In: FMOODS\/FORTE, pp. 152\u2013166 (2009)","DOI":"10.1007\/978-3-642-02138-1_10"},{"key":"315_CR26","unstructured":"Mendon\u00e7a, M., Wasowski, A., Czarnecki, K.: SAT-based analysis of feature models is easy. In: SPLC, pp. 231\u2013240 (2009)"},{"key":"315_CR27","doi-asserted-by":"crossref","unstructured":"Jackson, E.K., Sztipanovits, J.: Constructive techniques for meta- and model-level reasoning. In: MODELS, pp. 405\u2013419 (2007)","DOI":"10.1007\/978-3-540-75209-7_28"},{"issue":"1\u20133","key":"315_CR28","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/S0743-1066(98)10002-X","volume":"37","author":"J Jaffar","year":"1998","unstructured":"Jaffar, J., Maher, M.J., Marriott, K., Stuckey, P.J.: The semantics of constraint logic programs. J. Log. Program. 37(1\u20133), 1\u201346 (1998)","journal-title":"J. Log. Program."},{"key":"315_CR29","doi-asserted-by":"crossref","unstructured":"Lifschitz, V.: Twelve definitions of a stable model. In: ICLP, pp. 37\u201351 (2008)","DOI":"10.1007\/978-3-540-89982-2_8"},{"key":"315_CR30","unstructured":"Jackson, E.K., Bj\u00f8rner, N., Schulte, W.: Canonical regular types. In: ICLP (technical communications), pp. 73\u201383 (2011)"},{"key":"315_CR31","doi-asserted-by":"crossref","unstructured":"Sheeran, M., Singh, S., St\u00e5lmarck, G.: Checking safety properties using induction and a sat-solver. In: FMCAD, pp 108\u2013125 (2000)","DOI":"10.1007\/3-540-40922-X_8"},{"key":"315_CR32","unstructured":"Bj\u00f8rner, N., Hoder, K.: Generalized property directed reachability. In: SAT (2012)"},{"key":"315_CR33","doi-asserted-by":"crossref","unstructured":"Ball, T., Bj\u00f8rner, N., de Moura, L.M., McMillan, K.L., Veanes, M.: Beyond first-order satisfaction: Fixed points, interpolants, automata and polynomials. In: SPIN, pp. 1\u20136 (2012)","DOI":"10.1007\/978-3-642-31759-0_1"},{"key":"315_CR34","unstructured":"Object Management Group: Meta object facility (MOF) core specification version 2.4 (2010)"}],"container-title":["Software & Systems Modeling"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-013-0315-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10270-013-0315-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-013-0315-y","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,7,10]],"date-time":"2019-07-10T04:01:27Z","timestamp":1562731287000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10270-013-0315-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,2,27]]},"references-count":34,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2015,2]]}},"alternative-id":["315"],"URL":"https:\/\/doi.org\/10.1007\/s10270-013-0315-y","relation":{},"ISSN":["1619-1366","1619-1374"],"issn-type":[{"value":"1619-1366","type":"print"},{"value":"1619-1374","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013,2,27]]}}}