{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,1]],"date-time":"2025-06-01T22:10:05Z","timestamp":1748815805508,"version":"3.41.0"},"publisher-location":"Berlin, Heidelberg","reference-count":37,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662496640"},{"type":"electronic","value":"9783662496657"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"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":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-662-49665-7_6","type":"book-chapter","created":{"date-parts":[[2016,3,21]],"date-time":"2016-03-21T08:09:42Z","timestamp":1458547782000},"page":"87-103","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":24,"title":["Iterative and Incremental Model Generation by\u00a0Logic Solvers"],"prefix":"10.1007","author":[{"given":"Oszk\u00e1r","family":"Semer\u00e1th","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andr\u00e1s","family":"V\u00f6r\u00f6s","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"D\u00e1niel","family":"Varr\u00f3","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"1","key":"6_CR1","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1007\/s10270-008-0110-3","volume":"9","author":"K Anastasakis","year":"2010","unstructured":"Anastasakis, K., Bordbar, B., Georg, G., Ray, I.: On challenges of model transformation from UML to alloy. Soft. Syst. Model. 9(1), 69\u201386 (2010)","journal-title":"Soft. Syst. Model."},{"unstructured":"Bak, K., Diskin, Z., Antkiewicz, M., Czarnecki, K., Wasowski, A.: Clafer: unifying class and feature modeling. Softw. Syst. Model., pp. 1\u201335 (2013)","key":"6_CR2"},{"unstructured":"Beckert, B., Keller, U., Schmitt, P.H.: Translating the object constraint language into first-order predicate logic. In: Proceedings of the VERIFY, Workshop at Federated Logic Conferences (FLoC), Copenhagen, Denmark (2002)","key":"6_CR3"},{"doi-asserted-by":"crossref","unstructured":"Brottier, E., Fleurey, F., Steel, J., Baudry, B., Le Traon, Y.: Metamodel-based test generation for model transformations: an algorithm and a tool. In: 17th International Symposium on Software Reliability Engineering, ISSRE 2006, pp. 85\u201394, November 2006","key":"6_CR4","DOI":"10.1109\/ISSRE.2006.27"},{"unstructured":"Brucker, A.D., Wolff, B.: The HOL-OCL tool (2007). http:\/\/www.brucker.ch\/","key":"6_CR5"},{"key":"6_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1007\/978-3-642-31491-9_19","volume-title":"Modelling Foundations and Applications","author":"F B\u00fcttner","year":"2012","unstructured":"B\u00fcttner, F., Cabot, J.: Lightweight string reasoning for OCL. In: Vallecillo, A., Tolvanen, J.-P., Kindler, E., St\u00f6rrle, H., Kolovos, D. (eds.) ECMFA 2012. LNCS, vol. 7349, pp. 244\u2013258. Springer, Heidelberg (2012)"},{"key":"6_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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. 7635, pp. 198\u2013213. Springer, Heidelberg (2012)"},{"doi-asserted-by":"crossref","unstructured":"Cabot, J., Clariso, R., Riera, D.: Verification of UML\/OCL class diagrams using constraint programming. In: IEEE International Conference on Software Testing Verification and Validation Workshopp, ICSTW 2008, pp. 73\u201380, April 2008","key":"6_CR8","DOI":"10.1109\/ICSTW.2008.54"},{"doi-asserted-by":"crossref","unstructured":"Cabot, J., Claris\u00f3, R., Riera, D.: UMLtoCSP: a tool for the formal verification of UML\/OCL models using constraint programming. In: Proceedings of the 22nd IEEE\/ACM International Conference on Automated Software Engineering (ASE 2007), pp. 547\u2013548. NY, USA. ACM, New York (2007)","key":"6_CR9","DOI":"10.1145\/1321631.1321737"},{"unstructured":"Clavel, M., Egea, M.: The ITP\/OCL tool (2008). http:\/\/maude.sip.ucm.es\/itp\/ocl\/","key":"6_CR10"},{"unstructured":"Crawford, J., Ginsberg, M., Luks, E., Roy, A.: Symmetry-breaking predicates for search problems. In: KR 1996, pp. 148\u2013159 (1996)","key":"6_CR11"},{"doi-asserted-by":"crossref","unstructured":"Famelis, M., Salay, R., Chechik, M.: Partial models: Towards modeling and reasoning with uncertainty. In: Proceedings of the 34th International Conference on Software Engineering, pp. 573\u2013583. IEEE Press, Piscataway, NJ, USA (2012)","key":"6_CR12","DOI":"10.1109\/ICSE.2012.6227159"},{"doi-asserted-by":"crossref","unstructured":"Fleurey, F., Steel, J., Baudry, B.: Validation in model-driven engineering: Testing model transformations. In: International Workshop on Model, Design and Validation, pp. 29\u201340, November 2004","key":"6_CR13","DOI":"10.1109\/MODEVA.2004.1425846"},{"key":"6_CR14","doi-asserted-by":"publisher","first-page":"386","DOI":"10.1007\/s10270-005-0089-y","volume":"4","author":"M Gogolla","year":"2005","unstructured":"Gogolla, M., Bohling, J., Richters, M.: Validating UML and OCL models in USE by automatic snapshot generation. Softw. Syst. Model. 4, 386\u2013398 (2005)","journal-title":"Softw. Syst. Model."},{"key":"6_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"152","DOI":"10.1007\/978-3-642-02138-1_10","volume-title":"Formal Techniques for Distributed Systems","author":"H Gr\u00f6nniger","year":"2009","unstructured":"Gr\u00f6nniger, H., Ringert, J.O., Rumpe, B.: System model-based definition of modeling language semantics. In: Lee, D., Lopes, A., Poetzsch-Heffter, A. (eds.) FMOODS 2009. LNCS, vol. 5522, pp. 152\u2013166. Springer, Heidelberg (2009)"},{"issue":"2","key":"6_CR16","doi-asserted-by":"publisher","first-page":"256","DOI":"10.1145\/505145.505149","volume":"11","author":"D Jackson","year":"2002","unstructured":"Jackson, D.: Alloy: a lightweight object modelling notation. ACM Trans. Softw. Eng. Methodol. 11(2), 256\u2013290 (2002)","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"key":"6_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"653","DOI":"10.1007\/978-3-642-24485-8_48","volume-title":"Model Driven Engineering Languages and Systems","author":"EK Jackson","year":"2011","unstructured":"Jackson, E.K., Levendovszky, T., Balasubramanian, D.: Reasoning about metamodeling with formal specifications and automatic proofs. In: Whittle, J., Clark, T., K\u00fchne, T. (eds.) MODELS 2011. LNCS, vol. 6981, pp. 653\u2013667. Springer, Heidelberg (2011)"},{"doi-asserted-by":"crossref","unstructured":"Jackson, E.K., Sztipanovits, J.: Towards a formal foundation for domain specific modeling languages. In: Proceedings of the 6th ACM \/ IEEE International Conference on Embedded Software, EMSOFT 2006, pp. 53\u201362, NY, USA. ACM, New York (2006)","key":"6_CR18","DOI":"10.1145\/1176887.1176896"},{"key":"6_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"405","DOI":"10.1007\/978-3-540-75209-7_28","volume-title":"Model Driven Engineering Languages and Systems","author":"EK Jackson","year":"2007","unstructured":"Jackson, E.K., Sztipanovits, J.: Constructive techniques for meta- and model-level reasoning. In: Engels, G., Opdyke, B., Schmidt, D.C., Weil, F. (eds.) MODELS 2007. LNCS, vol. 4735, pp. 405\u2013419. Springer, Heidelberg (2007)"},{"key":"6_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"33","DOI":"10.1007\/978-3-642-21292-5_3","volume-title":"Foundations of Computer Software","author":"E Kang","year":"2011","unstructured":"Kang, E., Jackson, E., Schulte, W.: An approach for effective design space exploration. In: Calinescu, R., Jackson, E. (eds.) Monterey Workshop 2010. LNCS, vol. 6662, pp. 33\u201354. Springer, Heidelberg (2011)"},{"key":"6_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1007\/978-3-642-02959-2_17","volume-title":"Automated Deduction \u2013 CADE-22","author":"L Kov\u00e1cs","year":"2009","unstructured":"Kov\u00e1cs, L., Voronkov, A.: Interpolation and symbol elimination. In: Schmidt, R.A. (ed.) CADE-22. LNCS, vol. 5663, pp. 199\u2013213. Springer, Heidelberg (2009)"},{"key":"6_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"290","DOI":"10.1007\/978-3-642-21952-8_21","volume-title":"Objects, Models, Components, Patterns","author":"M Kuhlmann","year":"2011","unstructured":"Kuhlmann, M., Hamann, L., Gogolla, M.: Extensive validation of OCL models by integrating SAT solving into USE. In: Bishop, J., Vallecillo, A. (eds.) TOOLS 2011. LNCS, vol. 6705, pp. 290\u2013306. Springer, Heidelberg (2011)"},{"key":"6_CR23","first-page":"59","volume":"7","author":"D Berre Le","year":"2010","unstructured":"Le Berre, D., Parrain, A.: The sat4j library, release 2.2. J. Satisf. Boolean Model. Comput. 7, 59\u201364 (2010)","journal-title":"J. Satisf. Boolean Model. Comput."},{"doi-asserted-by":"crossref","unstructured":"Milicevic, A., Near, J.P., Kang, E., Jackson, D.: Alloy*: A general-purpose higher-order relational constraint solver. In: 37th IEEE\/ACM International Conference on Software Engineering, ICSE, pp. 609\u2013619 (2015)","key":"6_CR24","DOI":"10.1109\/ICSE.2015.77"},{"key":"6_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"130","DOI":"10.1007\/978-3-642-02674-4_10","volume-title":"Model Driven Architecture - Foundations and Applications","author":"A Mougenot","year":"2009","unstructured":"Mougenot, A., Darrasse, A., Blanc, X., Soria, M.: Uniform random generation of huge metamodel instances. In: Paige, R.F., Hartman, A., Rensink, A. (eds.) ECMDA-FA 2009. LNCS, vol. 5562, pp. 130\u2013145. Springer, Heidelberg (2009)"},{"key":"6_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.S.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"unstructured":"The Object Management Group: Object Constraint Language, v2.0., May 2006","key":"6_CR27"},{"key":"6_CR28","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.datak.2011.09.004","volume":"73","author":"A Queralt","year":"2012","unstructured":"Queralt, A., Artale, A., Calvanese, D., Teniente, E.: OCL-Lite: Finite reasoning on UML\/OCL conceptual schemas. Data Knowl. Eng. 73, 1\u201322 (2012)","journal-title":"Data Knowl. Eng."},{"key":"6_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"133","DOI":"10.1007\/978-3-662-46675-9_9","volume-title":"Fundamental Approaches to Software Engineering","author":"R Salay","year":"2015","unstructured":"Salay, R., Chechik, M.: A generalized formal framework for partial modeling. In: Egyed, A., Schaefer, I. (eds.) FASE 2015. LNCS, vol. 9033, pp. 133\u2013148. Springer, Heidelberg (2015)"},{"issue":"3","key":"6_CR30","doi-asserted-by":"publisher","first-page":"1\u20133","DOI":"10.5381\/jot.2015.14.3.a3","volume":"14","author":"R Salay","year":"2015","unstructured":"Salay, R., Chechik, M., Famelis, M., Gorzny, J.: A methodology for verifying refinements of partial models. J. Object Technol. 14(3), 1\u20133\u20131\u201331 (2015)","journal-title":"J. Object Technol."},{"key":"6_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"224","DOI":"10.1007\/978-3-642-28872-2_16","volume-title":"Fundamental Approaches to Software Engineering","author":"R Salay","year":"2012","unstructured":"Salay, R., Famelis, M., Chechik, M.: Language independent refinement using partial modeling. In: de Lara, J., Zisman, A. (eds.) Fundamental Approaches to Software Engineering. LNCS, vol. 7212, pp. 224\u2013239. Springer, Heidelberg (2012)"},{"doi-asserted-by":"crossref","unstructured":"Semer\u00e1th, O., Barta, A., Horv\u00e1th, A., Szatm\u00e1ri, Z., Varr\u00f3, D.: Formal validation of domain-specific languages with derived features and well-formedness constraints. Softw. Syst. Model., pp. 1\u201336 (2015)","key":"6_CR32","DOI":"10.1007\/s10270-015-0485-x"},{"key":"6_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"32","DOI":"10.1007\/978-3-642-04425-0_4","volume-title":"Model Driven Engineering Languages and Systems","author":"S Sen","year":"2009","unstructured":"Sen, S., Moha, N., Baudry, B., J\u00e9z\u00e9quel, J.-M.: Meta-model pruning. In: Sch\u00fcrr, A., Selic, B. (eds.) MODELS 2009. LNCS, vol. 5795, pp. 32\u201346. Springer, Heidelberg (2009)"},{"doi-asserted-by":"crossref","unstructured":"Shah, S.M.A., Anastasakis, K., Bordbar, B.: From UML to Alloy and back again. In: MoDeVVa 2009: Proceedings of the 6th International Workshop on Model-Driven Engineering, Verification and Validation, pp. 1\u201310. ACM (2009)","key":"6_CR34","DOI":"10.1145\/1656485.1656489"},{"doi-asserted-by":"crossref","unstructured":"Soeken, M., Wille, R., Kuhlmann, M., Gogolla, M., Drechsler, R.: Verifying UML\/OCL models using boolean satisfiability. In: Design, Automation and Test in Europe, (DATE 2010), pp. 1341\u20131344. IEEE (2010)","key":"6_CR35","DOI":"10.1109\/DATE.2010.5457017"},{"issue":"3","key":"6_CR36","doi-asserted-by":"publisher","first-page":"214","DOI":"10.1016\/j.scico.2007.05.004","volume":"68","author":"D Varr\u00f3","year":"2007","unstructured":"Varr\u00f3, D., Balogh, A.: The model transformation language of the VIATRA2 framework. Sci. Comput. Program. 68(3), 214\u2013234 (2007)","journal-title":"Sci. Comput. Program."},{"unstructured":"Yakindu Statechart Tools: Yakindu. http:\/\/statecharts.org\/","key":"6_CR37"}],"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-49665-7_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,1]],"date-time":"2025-06-01T21:29:21Z","timestamp":1748813361000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-49665-7_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783662496640","9783662496657"],"references-count":37,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-49665-7_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]},"assertion":[{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}