{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,27]],"date-time":"2025-10-27T16:02:01Z","timestamp":1761580921676,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642244421"},{"type":"electronic","value":"9783642244438"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2011]]},"DOI":"10.1007\/978-3-642-24443-8_25","type":"book-chapter","created":{"date-parts":[[2011,10,6]],"date-time":"2011-10-06T00:34:12Z","timestamp":1317861252000},"page":"237-248","source":"Crossref","is-referenced-by-count":6,"title":["Supporting Model Based Design"],"prefix":"10.1007","author":[{"given":"R\u00e9mi","family":"Delmas","sequence":"first","affiliation":[]},{"given":"David","family":"Doose","sequence":"additional","affiliation":[]},{"given":"Anthony Fernandes","family":"Pires","sequence":"additional","affiliation":[]},{"given":"Thomas","family":"Polacsek","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"25_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"436","DOI":"10.1007\/978-3-540-75209-7_30","volume-title":"Model Driven Engineering Languages and Systems","author":"K. Anastasakis","year":"2007","unstructured":"Anastasakis, K., Bordbar, B., Georg, G., Ray, I.: UML2Alloy: A Challenging Model Transformation. In: Engels, G., Opdyke, B., Schmidt, D.C., Weil, F. (eds.) MODELS 2007. LNCS, vol.\u00a04735, pp. 436\u2013450. Springer, Heidelberg (2007)"},{"key":"25_CR2","doi-asserted-by":"crossref","unstructured":"Bailleux, O., Boufkhad, Y., Roussel, O.: New encodings of Pseudo-Boolean constraints into CNF. In: SAT (2009)","DOI":"10.1007\/978-3-642-02777-2_19"},{"key":"25_CR3","unstructured":"Barrett, C., Stump, A., Tinelli, C.: The smt-lib standard: Version 2.0. In: Proceedings of the 8th International Workshop on Satisfiability Modulo Theories, Edinburgh, England (2010)"},{"key":"25_CR4","doi-asserted-by":"crossref","unstructured":"Berardi, D., Calvanese, D., Giacomo, G.D.: Reasoning on UML class diagrams. Artificial Intelligence\u00a0168 (October 2005)","DOI":"10.1016\/j.artint.2005.05.003"},{"key":"25_CR5","doi-asserted-by":"crossref","unstructured":"Cabot, J., Claris\u00f3, R., Riera, D.: Verification of UML\/OCL Class Diagrams using Constraint Programming. In: ICSTW 2008 (2008)","DOI":"10.1109\/ICSTW.2008.54"},{"key":"25_CR6","doi-asserted-by":"crossref","unstructured":"Davis, M., Logemann, G., Loveland, D.W.: A machine program for theorem-proving. Commun. ACM\u00a05(7) (1962)","DOI":"10.1145\/368273.368557"},{"key":"25_CR7","doi-asserted-by":"crossref","unstructured":"Gogolla, M., B\u00fcttner, F., Richters, M.: USE: A UML-based specification environment for validating UML and OCL. Sci. Comput. Program. 69(1-3) (2007)","DOI":"10.1016\/j.scico.2007.01.013"},{"key":"25_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-44880-2_1","volume-title":"ZB 2003: Formal Specification and Development in Z and B","author":"D. Jackson","year":"2003","unstructured":"Jackson, D.: Alloy: A logical modelling language. In: Bert, D., Bowen, J.P., King, S. (eds.) ZB 2003. LNCS, vol.\u00a02651, p. 1. Springer, Heidelberg (2003)"},{"key":"25_CR9","unstructured":"Jeanneret, C., Eyer, L., Markovi\u00e9, S., Baar, T.: RoclET: Refactoring OCL Expressions by Transformations. In: ICSSEA (2006)"},{"key":"25_CR10","unstructured":"Jussien, N., Rochart, G., Lorca, X.: The CHOCO constraint programming solver. In: CPAIOR 2008 Workshop on Open-Source Software for Integer and Contraint Programming (OSSICP 2008), Paris, France (June 2008)"},{"key":"25_CR11","unstructured":"Leberre, D.: SAT4J, a SATisfiability library for java (2004)"},{"key":"25_CR12","unstructured":"Leberre, D., Parrain, A.: \u00c0 propos de l\u2019extension d\u2019un solveur SAT pour traiter des contraintes pseudo-bool\u00e9ennes. In: JFPC 2007 (2007)"},{"key":"25_CR13","doi-asserted-by":"crossref","unstructured":"Manquinho, V.M., Martins, R., Lynce, I.: Improving unsatisfiability-based algorithms for boolean optimization. In: SAT (2010)","DOI":"10.1007\/978-3-642-14186-7_16"},{"key":"25_CR14","doi-asserted-by":"crossref","unstructured":"Moskewicz, M., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an Efficient SAT Solver. In: DAC (2001)","DOI":"10.1145\/378239.379017"},{"key":"25_CR15","unstructured":"Roache, P.J.: Verification and validation in computational science and engineering. Hermosa Publishers (1998)"},{"key":"25_CR16","unstructured":"de Roquemaurel, M., Polacsek, T., Rolland, J.F., Bodeveix, J.P., Filali, M.: Assistance \u00e0 la conception de mod\u00e8les \u00e0 l\u2019aide de contraintes. In: AFADL 2010 (2010)"},{"key":"25_CR17","doi-asserted-by":"crossref","unstructured":"Sen, S., Baudry, B., Vangheluwe, H.: Towards domain-specific model editors with automatic model completion. Simulation\u00a086(2) (2010)","DOI":"10.1177\/0037549709340530"},{"key":"25_CR18","doi-asserted-by":"crossref","unstructured":"Soeken, M., Wille, R., Kuhlmann, M., Gogolla, M., Drechsler, R.: Verifying UML\/OCL Models Using Boolean Satisfiability. In: Mller, W. (ed.) Proc. Design, Automation and Test in Europe, DATE 2010 (2010)","DOI":"10.1109\/DATE.2010.5457017"},{"key":"25_CR19","volume-title":"EMF: Eclipse Modeling Framework 2.0","author":"D. Steinberg","year":"2009","unstructured":"Steinberg, D., Budinsky, F., Paternostro, M., Merks, E.: EMF: Eclipse Modeling Framework 2.0. Addison-Wesley Professional, Reading (2009)"},{"key":"25_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1007\/978-3-642-12251-4_3","volume-title":"Functional and Logic Programming","author":"N. Tamura","year":"2010","unstructured":"Tamura, N., Tanjo, T., Banbara, M.: Solving constraint satisfaction problems with SAT technology. In: Blume, M., Kobayashi, N., Vidal, G. (eds.) FLOPS 2010. LNCS, vol.\u00a06009, pp. 19\u201323. Springer, Heidelberg (2010)"},{"key":"25_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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)"},{"key":"25_CR22","unstructured":"Tseitin, G.S.: On the complexity of derivations in the propositional calculus. Studies in Mathematics and Mathematical Logic II (1968)"}],"container-title":["Lecture Notes in Computer Science","Model and Data Engineering"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-24443-8_25","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T20:14:13Z","timestamp":1558296853000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-24443-8_25"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642244421","9783642244438"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-24443-8_25","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}