{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,24]],"date-time":"2026-06-24T16:33:50Z","timestamp":1782318830252,"version":"3.54.5"},"reference-count":84,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2021,1,29]],"date-time":"2021-01-29T00:00:00Z","timestamp":1611878400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,1,29]],"date-time":"2021-01-29T00:00:00Z","timestamp":1611878400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Softw Syst Model"],"published-print":{"date-parts":[[2021,8]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Checking the consistency of a metamodel involves finding a valid metamodel instance that provably meets the set of constraints that are defined over the metamodel. These constraints are often specified in Object Constraint Language. Often, a metamodel is inconsistent due to conflicts among the constraints. Existing approaches and tools are typically incapable of pinpointing the conflicting constraints, and this makes it difficult for users to debug and fix their metamodels. In this paper, we present a formal approach for locating conflicting constraints in inconsistent metamodels. Our approach has four distinct features: (1) users can rank individual metamodel features using their own domain-specific knowledge, (2) we transform these ranked features to a weighted maximum satisfiability modulo theories problem and solve it to compute the set of maximum achievable features, (3) we pinpoint the conflicting constraints by solving the set cover problem using a novel algorithm, and (4) we have implemented our approach into a fully automated tool called MaxUSE. Our evaluation results, using our assembled set of benchmarks, demonstrate the scalability of our work and that it is capable of efficiently finding conflicting constraints.<\/jats:p>","DOI":"10.1007\/s10270-020-00849-8","type":"journal-article","created":{"date-parts":[[2021,1,29]],"date-time":"2021-01-29T09:42:05Z","timestamp":1611913325000},"page":"1271-1298","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":12,"title":["A formal approach to finding inconsistencies in a metamodel"],"prefix":"10.1007","volume":"20","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-5010-4746","authenticated-orcid":false,"given":"Hao","family":"Wu","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7708-3877","authenticated-orcid":false,"given":"Marie","family":"Farrell","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2021,1,29]]},"reference":[{"key":"849_CR1","doi-asserted-by":"publisher","first-page":"32","DOI":"10.1007\/978-3-540-72952-5_2","volume-title":"Formal Methods for Open Object-Based Distributed Systems","author":"W Ahrendt","year":"2007","unstructured":"Ahrendt, W., Beckert, B., H\u00e4hnle, R., Schmitt, P.H.: Key: a formal method for object-oriented systems. In: Bonsangue, M.M., Johnsen, E.B. (eds.) Formal Methods for Open Object-Based Distributed Systems, pp. 32\u201343. Springer, Berlin (2007)"},{"key":"849_CR2","doi-asserted-by":"crossref","unstructured":"Alon, N., Awerbuch, B., Azar, Y.: The online set cover problem. In: Symposium on Theory of Computing, pp. 100\u2013105. ACM (2003)","DOI":"10.1145\/780542.780558"},{"key":"849_CR3","doi-asserted-by":"crossref","unstructured":"Anastasakis, K., Bordbar, B., Georg, G., Ray, I.: UML2Alloy: a challenging model transformation. In: International Conference on Model Driven Engineering Languages and Systems, pp. 436\u2013450. Springer (2007)","DOI":"10.1007\/978-3-540-75209-7_30"},{"issue":"1","key":"849_CR4","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. Softw. Syst. Model. 9(1), 69\u201386 (2010)","journal-title":"Softw. Syst. Model."},{"issue":"3","key":"849_CR5","doi-asserted-by":"publisher","first-page":"24:1","DOI":"10.1145\/2491509.2491518","volume":"22","author":"M Balaban","year":"2013","unstructured":"Balaban, M., Maraee, A.: Finite satisfiability of UML class diagrams with constrained class hierarchy. ACM Trans. Softw. Eng. Methodol. 22(3), 24:1\u201324:42 (2013)","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"key":"849_CR6","doi-asserted-by":"crossref","unstructured":"Barrett, C., Conway, C.L., Deters, M., Hadarean, L., Jovanovi\u0107, D., King, T., Reynolds, A., Tinelli, C.: CVC4. In: International Conference on Computer Aided Verification, pp. 171\u2013177. Springer (2011)","DOI":"10.1007\/978-3-642-22110-1_14"},{"key":"849_CR7","unstructured":"Barrett, C., Stump, A., Tinelli, C.: The SMT-LIB standard: version 2.0. In: International Workshop on Satisfiability Modulo Theories. Elsevier Science (2010)"},{"key":"849_CR8","doi-asserted-by":"publisher","first-page":"30","DOI":"10.1007\/3-540-45594-9_3","volume-title":"Business Process Management, Models, Techniques, and Empirical Studies","author":"J Becker","year":"2000","unstructured":"Becker, J., Rosemann, M., von Uthmann, C.: Guidelines of business process modeling. In: van der Aalst, W., Deselm, J., Oberweis, A. (eds.) Business Process Management, Models, Techniques, and Empirical Studies, pp. 30\u201349. Springer, Berlin (2000)"},{"key":"849_CR9","unstructured":"Berardi, D., Calvanese, D., Giacomo, G.D.: Reasoning on UML class diagrams is EXPTIME-hard. In: International Workshop on Description Logics (2003)"},{"issue":"2\u20133","key":"849_CR10","first-page":"59","volume":"7","author":"DL Berre","year":"2010","unstructured":"Berre, D.L., Parrain, A.: The Sat4j library, release 2.2. J. Satisf. Boolean Model. Comput. 7(2\u20133), 59\u201364 (2010)","journal-title":"J. Satisf. Boolean Model. Comput."},{"key":"849_CR11","doi-asserted-by":"crossref","unstructured":"Brucker, A.D., Wolff, B.: HOL-OCL: A formal proof environment for UML\/OCL. In: 11th International Conference on Fundamental Approaches to Software Engineering, pp. 97\u2013100. Springer (2008)","DOI":"10.1007\/978-3-540-78743-3_8"},{"issue":"4","key":"849_CR12","doi-asserted-by":"publisher","first-page":"255","DOI":"10.1007\/s00236-009-0093-8","volume":"46","author":"AD Brucker","year":"2009","unstructured":"Brucker, A.D., Wolff, B.: Semantics, calculi, and analysis for object-oriented specifications. Acta Inform. 46(4), 255\u2013284 (2009)","journal-title":"Acta Inform."},{"key":"849_CR13","doi-asserted-by":"crossref","unstructured":"B\u00fcttner, F., Egea, M., Cabot, J.: On verifying ATL transformations using \u2018off-the-shelf\u2019 SMT solvers. In: International Conference on Model Driven Engineering Languages and Systems, pp. 432\u2013448. Springer (2012)","DOI":"10.1007\/978-3-642-33666-9_28"},{"key":"849_CR14","doi-asserted-by":"crossref","unstructured":"Cabot, J., Claris\u00f3, R., Riera, D.: Verification of UML\/OCL class diagrams using constraint programming. In: International Conference on Software Testing Verification and Validation Workshop, pp. 73\u201380. IEEE (2008)","DOI":"10.1109\/ICSTW.2008.54"},{"key":"849_CR15","doi-asserted-by":"crossref","unstructured":"Cabot, J., Claris\u00f3, R., Riera, D.: Verifying UML\/OCL operation contracts. In: International Conference on Integrated Formal Methods, pp. 40\u201355. Springer (2009)","DOI":"10.1007\/978-3-642-00255-7_4"},{"key":"849_CR16","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.jss.2014.03.023","volume":"93","author":"J Cabot","year":"2014","unstructured":"Cabot, J., Claris\u00f3, R., Riera, D.: On the verification of UML\/OCL class diagrams using constraint programming. J. Syst. Softw. 93, 1\u201323 (2014)","journal-title":"J. Syst. Softw."},{"key":"849_CR17","first-page":"36","volume-title":"Artificial Intelligence and Human-Oriented Computing","author":"M Cadoli","year":"2007","unstructured":"Cadoli, M., Calvanese, D., Giacomo, G., Mancini, T.: Finite model reasoning on UML class diagrams via constraint programming. In: Basili, R., Pazienza, M.T. (eds.) Artificial Intelligence and Human-Oriented Computing, pp. 36\u201347. Springer, Berlin (2007)"},{"key":"849_CR18","unstructured":"Cadoli, M., Calvanese, D., Mancini, T.: Finite satisfiability of UML class diagrams by constraint programming. In: International Workshop on Description Logics (2004)"},{"key":"849_CR19","unstructured":"Calvanese, D.: Finite model reasoning in description logics. In: International Conference on the Principles of Knowledge Representation and Reasoning, pp. 292\u2013303. Morgan Kaufmann (1996)"},{"issue":"POPL","key":"849_CR20","doi-asserted-by":"publisher","first-page":"49:1","DOI":"10.1145\/3290362","volume":"3","author":"T Chen","year":"2019","unstructured":"Chen, T., Hague, M., Lin, A.W., R\u00fcmmer, P., Wu, Z.: Decision procedures for path feasibility of string-manipulating programs with complex operations. Proc. ACM Program. Lang. 3(POPL), 49:1\u201349:30 (2019)","journal-title":"Proc. ACM Program. Lang."},{"issue":"3","key":"849_CR21","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1287\/moor.4.3.233","volume":"4","author":"V Chvatal","year":"1979","unstructured":"Chvatal, V.: A greedy heuristic for the set-covering problem. Math. Oper. Res. 4(3), 233\u2013235 (1979)","journal-title":"Math. Oper. Res."},{"key":"849_CR22","doi-asserted-by":"crossref","unstructured":"Cimatti, A., Franz\u00e9n, A., Griggio, A., Sebastiani, R., Stenico, C.: Satisfiability modulo the theory of costs: foundations and applications. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 99\u2013113. Springer (2010)","DOI":"10.1007\/978-3-642-12002-2_8"},{"key":"849_CR23","doi-asserted-by":"crossref","unstructured":"Cimatti, A., Griggio, A., Schaafsma, B.J., Sebastiani, R.: The mathSAT5 SMT solver. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 93\u2013107. Springer (2013)","DOI":"10.1007\/978-3-642-36742-7_7"},{"key":"849_CR24","first-page":"1","volume":"24","author":"M Clavel","year":"2009","unstructured":"Clavel, M., Egea, M., de Dios, M.A.G.: Checking unsatisfiability for OCL constraints. Electron. Commun. Eur. Assoc. Softw. Sci. Technol. 24, 1\u201313 (2009)","journal-title":"Electron. Commun. Eur. Assoc. Softw. Sci. Technol."},{"key":"849_CR25","unstructured":"Dania, C., Clavel, M.: Ocl2fol+: coping with undefinedness. In: OCL@MoDELS, pp. 53\u201362 (2013)"},{"key":"849_CR26","doi-asserted-by":"crossref","unstructured":"Dania, C., Clavel, M.: Ocl2msfol: a mapping to many-sorted first-order logic for efficiently checking the satisfiability of ocl constraints. In: International Conference on Model Driven Engineering Languages and Systems, pp. 65\u201375. ACM (2016)","DOI":"10.1145\/2976767.2976774"},{"key":"849_CR27","doi-asserted-by":"crossref","unstructured":"De\u00a0Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 337\u2013340. Springer (2008)","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"849_CR28","doi-asserted-by":"crossref","unstructured":"Een, N., S\u00f6rensson, N.: An extensible SAT-solver. In: International Conference on Theory and Applications of Satisfiability Testing, pp. 502\u2013518. Springer (2005)","DOI":"10.1007\/978-3-540-24605-3_37"},{"issue":"4","key":"849_CR29","doi-asserted-by":"publisher","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":"849_CR30","doi-asserted-by":"crossref","unstructured":"El\u00a0Ghazi, A.A., Taghdiri, M.: Relational reasoning via SMT solving. In: International Conference on Formal Methods, pp. 133\u2013148. Springer (2011)","DOI":"10.1007\/978-3-642-21437-0_12"},{"issue":"2","key":"849_CR31","doi-asserted-by":"publisher","first-page":"163","DOI":"10.1016\/j.datak.2004.08.002","volume":"53","author":"C Farr\u00e9","year":"2005","unstructured":"Farr\u00e9, C., Teniente, E., Urp\u00ed, T.: Checking query containment with the cqc method. Data Knowl. Eng. 53(2), 163\u2013223 (2005)","journal-title":"Data Knowl. Eng."},{"issue":"4","key":"849_CR32","doi-asserted-by":"publisher","first-page":"634","DOI":"10.1145\/285055.285059","volume":"45","author":"U Feige","year":"1998","unstructured":"Feige, U.: A threshold of ln n for approximating set cover. J. ACM 45(4), 634\u2013652 (1998)","journal-title":"J. ACM"},{"key":"849_CR33","doi-asserted-by":"crossref","unstructured":"Filli\u00e2tre, J.C., Paskevich, A.: Why3\u2014where programs meet provers. In: European Symposium on Programming, pp. 125\u2013128. Springer (2013)","DOI":"10.1007\/978-3-642-37036-6_8"},{"key":"849_CR34","doi-asserted-by":"crossref","unstructured":"Garis, A., Cunha, A., Riesco, D.: Translating alloy specifications to UML class diagrams annotated with OCL. In: International Conference on Software Engineering and Formal Methods, pp. 221\u2013236. Springer (2011)","DOI":"10.1007\/978-3-642-24690-6_16"},{"key":"849_CR35","doi-asserted-by":"crossref","unstructured":"Gheyi, R., Massoni, T., Borba, P.: A rigorous approach for proving model refactorings. In: International Conference on Automated Software Engineering, pp. 372\u2013375. ACM (2005)","DOI":"10.1145\/1101908.1101973"},{"key":"849_CR36","doi-asserted-by":"crossref","unstructured":"Gogolla, M., B\u00fcttner, F., Cabot, J.: Initiating a benchmark for UML and OCL analysis tools. In: International Conference on Tests and Proofs, pp. 115\u2013132. Springer (2013)","DOI":"10.1007\/978-3-642-38916-0_7"},{"issue":"1\u20133","key":"849_CR37","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1016\/j.scico.2007.01.013","volume":"69","author":"M Gogolla","year":"2007","unstructured":"Gogolla, M., B\u00fcttner, F., Richters, M.: USE: a UML-based specification environment for validating UML and OCL. Sci. Comput. Program. 69(1\u20133), 27\u201334 (2007)","journal-title":"Sci. Comput. Program."},{"key":"849_CR38","doi-asserted-by":"crossref","unstructured":"Gonz\u00e1lez\u00a0P\u00e9rez, C.A., Buettner, F., Claris\u00f3, R., Cabot, J.: EMFtoCSP: A tool for the lightweight verification of EMF models. In: International Workshop on Formal Methods in Software Engineering: Rigorous and Agile Approaches, pp. 44\u201350. IEEE (2012)","DOI":"10.1109\/FormSERA.2012.6229788"},{"key":"849_CR39","doi-asserted-by":"crossref","unstructured":"Gulwani, S., Jha, S., Tiwari, A., Venkatesan, R.: Synthesis of loop-free programs. In: 32nd Conference on Programming Language Design and Implementation. PLDI \u201911, pp. 62\u201373. ACM, New York, NY, USA (2011)","DOI":"10.1145\/1993498.1993506"},{"key":"849_CR40","doi-asserted-by":"crossref","unstructured":"Harris, W.R., Sankaranarayanan, S., Ivan\u010di\u0107, F., Gupta, A.: Program analysis via satisfiability modulo path programs. In: 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL \u201910, pp. 71\u201382. ACM (2010)","DOI":"10.1145\/1706299.1706309"},{"key":"849_CR41","first-page":"1","volume":"29","author":"B Hoffmann","year":"2010","unstructured":"Hoffmann, B., Minas, M.: Defining models\u2014meta models versus graph grammars. Electron. Commun. EASST 29, 1\u201314 (2010)","journal-title":"Electron. Commun. EASST"},{"key":"849_CR42","unstructured":"Hoffmann, B., Minas, M.: Generating instance graphs from class diagrams with adaptive star grammars. In: 3rd International Workshop on Graph Computation Models (2011)"},{"issue":"POPL","key":"849_CR43","first-page":"4:1","volume":"2","author":"L Hol\u00edk","year":"2017","unstructured":"Hol\u00edk, L., Jank\u016f, P., Lin, A.W., R\u00fcmmer, P., Vojnar, T.: String constraints with concatenation and transducers solved efficiently. Proc. ACM Program. Lang. 2(POPL), 4:1\u201343:2 (2017)","journal-title":"Proc. ACM Program. Lang."},{"key":"849_CR44","unstructured":"ILOG: ILOG OPL Studio System Version 3.6.1 User\u2019s Manual. IBM (2002)"},{"issue":"2","key":"849_CR45","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":"849_CR46","doi-asserted-by":"crossref","unstructured":"Jangda, A., Yorsh, G.: Unbounded superoptimization. In: Proceedings of the 2017 ACM SIGPLAN International Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software, Onward! 2017, pp. 78\u201388. ACM (2017)","DOI":"10.1145\/3133850.3133856"},{"key":"849_CR47","doi-asserted-by":"crossref","unstructured":"Jouault, F., Kurtev, I.: Transforming models with ATL. In: The 2005 International Conference on Satellite Events at the MoDELS, pp. 128\u2013138. Springer (2006)","DOI":"10.1007\/11663430_14"},{"key":"849_CR48","unstructured":"Karp, R.M.: Reducibility among combinatorial problems. In: Miller, R.E., Thatcher, J.W., Bohlinger, J.D. (eds.) Complexity of Computer Computations, pp. 85\u2013103. Springer, Boston, MA, IBM Thomas J. Watson Research Center, Yorktown Heights, New York (1972)"},{"key":"849_CR49","doi-asserted-by":"crossref","unstructured":"Kuhlmann, M., Gogolla, M.: From uml and ocl to relational logic and back. In: 15th International Conference on Model Driven Engineering Languages and Systems, pp. 415\u2013431. Springer (2012)","DOI":"10.1007\/978-3-642-33666-9_27"},{"key":"849_CR50","doi-asserted-by":"crossref","unstructured":"Kuhlmann, M., Gogolla, M.: Strengthening SAT-based validation of UML\/OCL models by representing collections as relations. In: Modelling Foundations and Applications, Lecture Notes in Computer Science, vol. 7349, pp. 32\u201348. Springer (2012)","DOI":"10.1007\/978-3-642-31491-9_5"},{"key":"849_CR51","doi-asserted-by":"crossref","unstructured":"Kuhlmann, M., Hamann, L., Gogolla, M.: Extensive validation of OCL models by integrating SAT solving into USE. In; 49th International Conference on Objects. Models, Components, Patterns, pp. 290\u2013306. Springer, Zurich, Switzerland (2011)","DOI":"10.1007\/978-3-642-21952-8_21"},{"key":"849_CR52","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1016\/j.entcs.2004.09.027","volume":"115","author":"M Kyas","year":"2005","unstructured":"Kyas, M., Fecher, H., de Boer, F.S., Jacob, J., Hooman, J., van der Zwaag, M., Arons, T., Kugler, H.: Formalizing UML models and OCL constraints in PVS. Electron. Notes Theor. Comput. Sci. 115, 39\u201347 (2005)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"849_CR53","doi-asserted-by":"crossref","unstructured":"Li, Y., Albarghouthi, A., Kincaid, Z., Gurfinkel, A., Chechik, M.: Symbolic optimization with smt solvers. In: 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL \u201914, pp. 607\u2013618. ACM (2014)","DOI":"10.1145\/2535838.2535857"},{"issue":"3","key":"849_CR54","doi-asserted-by":"publisher","first-page":"206","DOI":"10.1007\/s10703-016-0247-6","volume":"48","author":"T Liang","year":"2016","unstructured":"Liang, T., Reynolds, A., Tsiskaridze, N., Tinelli, C., Barrett, C., Deters, M.: An efficient SMT solver for string constraints. Form. Methods Syst. Des. 48(3), 206\u2013234 (2016)","journal-title":"Form. Methods Syst. Des."},{"issue":"1","key":"849_CR55","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s10817-007-9084-z","volume":"40","author":"MH Liffiton","year":"2008","unstructured":"Liffiton, M.H., Sakallah, K.A.: Algorithms for computing minimal unsatisfiable subsets of constraints. J. Autom. Reason. 40(1), 1\u201333 (2008)","journal-title":"J. Autom. Reason."},{"key":"849_CR56","doi-asserted-by":"crossref","unstructured":"Maoz, S., Ringert, J.O., Rumpe, B.: CD2Alloy: class diagrams analysis using alloy revisited. In: The 14th International Conference on Model Driven Engineering Languages and Systems, pp. 592\u2013607 (2011)","DOI":"10.1007\/978-3-642-24485-8_44"},{"key":"849_CR57","first-page":"235","volume-title":"Removing Redundancies and Deducing Equivalences in UML Class Diagrams","author":"A Maraee","year":"2014","unstructured":"Maraee, A., Balaban, M.: Removing Redundancies and Deducing Equivalences in UML Class Diagrams, pp. 235\u2013251. Springer, Berlin (2014)"},{"key":"849_CR58","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 International Conference on Software Engineering, ICSE \u201915, pp. 609\u2013619. IEEE Press (2015)","DOI":"10.1109\/ICSE.2015.77"},{"key":"849_CR59","first-page":"53","volume":"9","author":"A Niemetz","year":"2015","unstructured":"Niemetz, A., Preiner, M., Biere, A.: Boolector 2.0 system description. J. Satisf. Boolean Model. Comput. 9, 53\u201358 (2015)","journal-title":"J. Satisf. Boolean Model. Comput."},{"key":"849_CR60","first-page":"156","volume-title":"Theory and Applications of Satisfiability Testing","author":"R Nieuwenhuis","year":"2006","unstructured":"Nieuwenhuis, R., Oliveras, A.: On sat modulo theories and optimization problems. In: Biere, A., Gome, C.P. (eds.) Theory and Applications of Satisfiability Testing, pp. 156\u2013169. Springer, Berlin (2006)"},{"key":"849_CR61","doi-asserted-by":"publisher","unstructured":"Perrouin, G., Sen, S., Klein, J., Baudry, B., Le Traon, Y.: Automated and scalable t-wise test case generation strategies for software product lines. In: The 3rd International Conference on Software Testing, Verification and Validation, pp. 459\u2013468 (2010). https:\/\/doi.org\/10.1109\/ICST.2010.43","DOI":"10.1109\/ICST.2010.43"},{"key":"849_CR62","doi-asserted-by":"crossref","unstructured":"Przigoda, N., Hilken, C., Wille, R., Peleska, J., Drechsler, R.: Checking concurrent behavior in uml\/ocl models. In: 18th International Conference on Model Driven Engineering Languages and Systems (MODELS), pp. 176\u2013185 (2015)","DOI":"10.1109\/MODELS.2015.7338248"},{"key":"849_CR63","doi-asserted-by":"crossref","unstructured":"Przigoda, N., Wille, R., Drechsler, R.: Ground setting properties for an efficient translation of OCL in SMT-based model finding. In: 19th International Conference on Model Driven Engineering Languages and Systems, pp. 261\u2013271. ACM (2016)","DOI":"10.1145\/2976767.2976780"},{"key":"849_CR64","first-page":"497","volume-title":"Conceptual Modeling","author":"A Queralt","year":"2006","unstructured":"Queralt, A., Teniente, E.: Reasoning on uml class diagrams with ocl constraints. In: Embley, D.W., Oliv\u00e9, A., Ram, S. (eds.) Conceptual Modeling, pp. 497\u2013512. Springer, Berlin (2006)"},{"key":"849_CR65","doi-asserted-by":"crossref","unstructured":"Reynolds, A., Barbosa, H., Fontaine, P.: Revisiting enumerative instantiation. In: 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 112\u2013131. Springer International Publishing (2018)","DOI":"10.1007\/978-3-319-89963-3_7"},{"key":"849_CR66","doi-asserted-by":"crossref","unstructured":"Reynolds, A., Deters, M., Kuncak, V., Tinelli, C., Barrett, C.: Counterexample-guided quantifier instantiation for synthesis in smt. In: Computer Aided Verification, pp. 198\u2013216. Springer International Publishing, Cham (2015)","DOI":"10.1007\/978-3-319-21668-3_12"},{"issue":"3","key":"849_CR67","doi-asserted-by":"publisher","first-page":"500","DOI":"10.1007\/s10703-017-0290-y","volume":"51","author":"A Reynolds","year":"2017","unstructured":"Reynolds, A., King, T., Kuncak, V.: Solving quantified linear arithmetic by counterexample-guided instantiation. Form. Methods Syst. Des. 51(3), 500\u2013532 (2017)","journal-title":"Form. Methods Syst. Des."},{"key":"849_CR68","doi-asserted-by":"crossref","unstructured":"Singh, R., Gulwani, S., Solar-Lezama, A.: Automated feedback generation for introductory programming assignments. In: 34th ACM SIGPLAN Conference on Programming Language Design and Implementation. PLDI \u201913, pp. 15\u201326. ACM, New York, NY, USA (2013)","DOI":"10.1145\/2491956.2462195"},{"key":"849_CR69","doi-asserted-by":"crossref","unstructured":"Soeken, M., Wille, R., Drechsler, R.: Encoding OCL data types for SAT-based verification of UML\/OCL models. In: 5th International Conference on Tests and Proofs, pp. 152\u2013170. Springer, Zurich, Switzerland (2011)","DOI":"10.1007\/978-3-642-21768-5_12"},{"key":"849_CR70","doi-asserted-by":"crossref","unstructured":"Soeken, M., Wille, R., Drechsler, R.: Towards automatic determination of problem bounds for object instantiation in static model verification. In: 8th International Workshop on Model-Driven Engineering, Verification and Validation, pp. 2:1\u20132:4. ACM, Wellington, New Zealand (2011)","DOI":"10.1145\/2095654.2095657"},{"key":"849_CR71","first-page":"1","volume-title":"Design, Automation Test in Europe","author":"M Soeken","year":"2011","unstructured":"Soeken, M., Wille, R., Drechsler, R.: Verifying dynamic aspects of uml models. In: Preas, K. (ed.) Design, Automation Test in Europe, pp. 1\u20136. IEEE, Grenoble, France (2011)"},{"key":"849_CR72","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 Test in Europe Conference Exhibition, pp. 1341\u20131344. Dresden, Germany (2010)","DOI":"10.1109\/DATE.2010.5457017"},{"key":"849_CR73","doi-asserted-by":"crossref","unstructured":"Tillmann, N., De\u00a0Halleux, J.: Pex: White box test generation for .NET. In: The 2nd International Conference on Tests and Proofs, pp. 134\u2013153 (2008)","DOI":"10.1007\/978-3-540-79124-9_10"},{"key":"849_CR74","doi-asserted-by":"crossref","unstructured":"Torlak, E., Chang, F.S.H., Jackson, D.: Finding minimal unsatisfiable cores of declarative specifications. In: The 15th International Symposium on Formal Methods, pp. 326\u2013341. Springer, Turku, Finland (2008)","DOI":"10.1007\/978-3-540-68237-0_23"},{"key":"849_CR75","doi-asserted-by":"crossref","unstructured":"Torlak, E., Jackson, D.: Kodkod: a relational model finder. In: 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 632\u2013647. Springer, Braga, Portugal (2007)","DOI":"10.1007\/978-3-540-71209-1_49"},{"key":"849_CR76","doi-asserted-by":"crossref","unstructured":"Wille, R., Soeken, M., Drechsler, R.: Debugging of inconsistent UML\/OCL models. In: 2012 Design, Automation Test in Europe Conference Exhibition, pp. 1078\u20131083 (2012)","DOI":"10.1109\/DATE.2012.6176655"},{"key":"849_CR77","doi-asserted-by":"publisher","first-page":"159","DOI":"10.1016\/j.entcs.2008.04.038","volume":"211","author":"J Winkelmann","year":"2008","unstructured":"Winkelmann, J., Taentzer, G., Ehrig, K., K\u00fcster, J.M.: Translation of restricted OCL constraints into graph constraints for generating meta model instances by graph grammars. Electron. Notes Theor. Comput. Sci. 211, 159\u2013170 (2008)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"849_CR78","doi-asserted-by":"crossref","unstructured":"Wu, H.: Generating metamodel instances satisfying coverage criteria via SMT solving. In: The 4th International Conference on Model-Driven Engineering and Software Development, pp. 40\u201351 (2016)","DOI":"10.5220\/0005650000400051"},{"key":"849_CR79","doi-asserted-by":"crossref","unstructured":"Wu, H.: Finding achievable features and constraint conflicts for inconsistent metamodels. In: 13th European Conference on Modelling Foundations and Applications, pp. 179\u2013196. Springer (2017)","DOI":"10.1007\/978-3-319-61482-3_11"},{"key":"849_CR80","doi-asserted-by":"crossref","unstructured":"Wu, H.: Maxuse: a tool for finding achievable constraints and conflicts for inconsistent UML class diagrams. In: Integrated Formal Methods, pp. 348\u2013356. Springer (2017)","DOI":"10.1007\/978-3-319-66845-1_23"},{"key":"849_CR81","doi-asserted-by":"publisher","first-page":"356","DOI":"10.1007\/978-3-319-74730-9_31","volume-title":"Software Technologies: Applications and Foundations","author":"H Wu","year":"2018","unstructured":"Wu, H.: Step 0: an idea for automatic OCL benchmark generation. In: Seidl, M., Zschaler, S. (eds.) Software Technologies: Applications and Foundations, pp. 356\u2013364. Springer, Cham (2018)"},{"key":"849_CR82","doi-asserted-by":"crossref","unstructured":"Wu, H.: Synthesising call sequences from OCL operational contracts. In: 34th ACM\/SIGAPP Symposium on Applied Computing (2019)","DOI":"10.1145\/3297280.3297612"},{"key":"849_CR83","doi-asserted-by":"crossref","unstructured":"Wu, H., Monahan, R., Power, J.F.: Exploiting attributed type graphs to generate metamodel instances using an SMT solver. In: 7th International Symposium on Theoretical Aspects of Software Engineering. Birmingham, UK (2013)","DOI":"10.1109\/TASE.2013.31"},{"key":"849_CR84","doi-asserted-by":"crossref","unstructured":"Zschaler, S., Kolovos, D.S., Drivalos, N., Paige, R.F., Rashid, A.: The 2nd International Conference on Software Language Engineering, Chap. Domain-Specific Metamodelling Languages for Software Language Engineering, pp. 334\u2013353. Springer, Berlin, Heidelberg (2010)","DOI":"10.1007\/978-3-642-12107-4_23"}],"container-title":["Software and Systems Modeling"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-020-00849-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10270-020-00849-8\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-020-00849-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,8,31]],"date-time":"2021-08-31T18:06:27Z","timestamp":1630433187000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10270-020-00849-8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,1,29]]},"references-count":84,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2021,8]]}},"alternative-id":["849"],"URL":"https:\/\/doi.org\/10.1007\/s10270-020-00849-8","relation":{},"ISSN":["1619-1366","1619-1374"],"issn-type":[{"value":"1619-1366","type":"print"},{"value":"1619-1374","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,1,29]]},"assertion":[{"value":"21 December 2018","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"12 November 2020","order":2,"name":"revised","label":"Revised","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"24 November 2020","order":3,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"29 January 2021","order":4,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}