{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T12:17:28Z","timestamp":1763468248701,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662466742"},{"type":"electronic","value":"9783662466759"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-662-46675-9_20","type":"book-chapter","created":{"date-parts":[[2015,3,31]],"date-time":"2015-03-31T16:24:38Z","timestamp":1427819078000},"page":"301-315","source":"Crossref","is-referenced-by-count":16,"title":["Exploring Scenario Exploration"],"prefix":"10.1007","author":[{"given":"Nuno","family":"Macedo","sequence":"first","affiliation":[]},{"given":"Alcino","family":"Cunha","sequence":"additional","affiliation":[]},{"given":"Tiago","family":"Guimar\u00e3es","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"20_CR1","doi-asserted-by":"crossref","unstructured":"Anastasakis, K., Bordbar, B., Georg, G., Ray, I.: On challenges of model transformation from UML to Alloy. In: SoSyM, vol.\u00a09, pp. 69\u201386 (2010)","DOI":"10.1007\/s10270-008-0110-3"},{"key":"20_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"198","DOI":"10.1007\/978-3-642-34281-3_16","volume-title":"Formal Methods and Software Engineering","author":"F. 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: Aoki, T., Taguchi, K. (eds.) ICFEM 2012. LNCS, vol.\u00a07635, pp. 198\u2013213. Springer, Heidelberg (2012)"},{"key":"20_CR3","doi-asserted-by":"crossref","unstructured":"Cunha, A., Garis, A., Riesco, D.: Translating between Alloy specifications and UML class diagrams annotated with OCL. In: SoSyM (2013)","DOI":"10.1007\/s10270-013-0353-5"},{"key":"20_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"17","DOI":"10.1007\/978-3-642-54804-8_2","volume-title":"Fundamental Approaches to Software Engineering","author":"A. Cunha","year":"2014","unstructured":"Cunha, A., Macedo, N., Guimar\u00e3es, T.: Target oriented relational model finding. In: Gnesi, S., Rensink, A. (eds.) FASE 2014 (ETAPS). LNCS, vol.\u00a08411, pp. 17\u201331. Springer, Heidelberg (2014)"},{"key":"20_CR5","unstructured":"Garcia, M.: Formalization of QVT-Relations: OCL-based static semantics and Alloy-based validation. In: MDSD 2008, pp. 21\u201330. Shaker Verlag (2008)"},{"key":"20_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"224","DOI":"10.1007\/978-3-642-39071-5_17","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2013","author":"M. Iser","year":"2013","unstructured":"Iser, M., Sinz, C., Taghdiri, M.: Minimizing models for tseitin-encoded SAT instances. In: J\u00e4rvisalo, M., Van Gelder, A. (eds.) SAT 2013. LNCS, vol.\u00a07962, pp. 224\u2013232. Springer, Heidelberg (2013)"},{"key":"20_CR7","unstructured":"Jackson, D.: Software Abstractions: Logic, Language, and Analysis. MIT Press, revised edition (2012)"},{"key":"20_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"173","DOI":"10.1007\/978-3-642-13595-8_15","volume-title":"Modelling Foundations and Applications","author":"M. Kleiner","year":"2010","unstructured":"Kleiner, M., Del Fabro, M.D., Albert, P.: Model search: Formalizing and automating constraint solving in MDE platforms. In: K\u00fchne, T., Selic, B., Gervais, M.-P., Terrier, F. (eds.) ECMFA 2010. LNCS, vol.\u00a06138, pp. 173\u2013188. Springer, Heidelberg (2010)"},{"key":"20_CR9","unstructured":"Koshimura, M., Nabeshima, H., Fujita, H., Hasegawa, R.: Minimal model generation with respect to an atom set. In: FTP 2009, pp. 49\u201359 (2009)"},{"key":"20_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"415","DOI":"10.1007\/978-3-642-33666-9_27","volume-title":"Model Driven Engineering Languages and Systems","author":"M. Kuhlmann","year":"2012","unstructured":"Kuhlmann, M., Gogolla, M.: From UML and OCL to relational logic and back. In: France, R.B., Kazmeier, J., Breu, R., Atkinson, C. (eds.) MODELS 2012. LNCS, vol.\u00a07590, pp. 415\u2013431. Springer, Heidelberg (2012)"},{"key":"20_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"297","DOI":"10.1007\/978-3-642-37057-1_22","volume-title":"Fundamental Approaches to Software Engineering","author":"N. Macedo","year":"2013","unstructured":"Macedo, N., Cunha, A.: Implementing QVT-R bidirectional model transformations using alloy. In: Cortellessa, V., Varr\u00f3, D. (eds.) FASE 2013 (ETAPS 2013). LNCS, vol.\u00a07793, pp. 297\u2013311. Springer, Heidelberg (2013)"},{"key":"20_CR12","doi-asserted-by":"crossref","unstructured":"Macedo, N., Cunha, A.: Least-change bidirectional model transformation with QVT-R and ATL. In: SoSyM (2014) (to appear)","DOI":"10.1007\/s10270-014-0437-x"},{"key":"20_CR13","doi-asserted-by":"crossref","unstructured":"Macedo, N., Guimar\u00e3es, T., Cunha, A.: Model repair and transformation with Echo. In: ASE 2013, pp. 694\u2013697. IEEE (2013)","DOI":"10.1109\/ASE.2013.6693135"},{"key":"20_CR14","unstructured":"McCune, W.: A Davis-Putnam program and its application to finite first-order model search: quasigroup existence problem. Technical Report ANL\/MCS-TM-194, Argonne National Laboratory, Argonne, IL (May 1994)"},{"key":"20_CR15","doi-asserted-by":"crossref","unstructured":"Nelson, T., Saghafi, S., Dougherty, D.J., Fisler, K., Krishnamurthi, S.: Aluminum: principled scenario exploration through minimality. In: ICSE 2013, pp. 232\u2013241. IEEE\/ACM (2013)","DOI":"10.1109\/ICSE.2013.6606569"},{"key":"20_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1007\/978-3-642-21470-7_6","volume-title":"Modelling Foundations and Applications","author":"R. Straeten Van Der","year":"2011","unstructured":"Van Der Straeten, R., Pinna Puissant, J., Mens, T.: Assessing the kodkod model finder for resolving model inconsistencies. In: France, R.B., Kuester, J.M., Bordbar, B., Paige, R.F. (eds.) ECMFA 2011. LNCS, vol.\u00a06698, pp. 69\u201384. Springer, Heidelberg (2011)"},{"key":"20_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"632","DOI":"10.1007\/978-3-540-71209-1_49","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E. Torlak","year":"2007","unstructured":"Torlak, E., Jackson, D.: Kodkod: A relational model finder. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol.\u00a04424, pp. 632\u2013647. Springer, Heidelberg (2007)"}],"container-title":["Lecture Notes in Computer Science","Fundamental Approaches to Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-46675-9_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,29]],"date-time":"2019-05-29T14:19:25Z","timestamp":1559139565000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-46675-9_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783662466742","9783662466759"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-46675-9_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]}}}