{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,25]],"date-time":"2026-09-25T21:13:46Z","timestamp":1790370826954,"version":"4.1.0"},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783662436516","type":"print"},{"value":"9783662436523","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-662-43652-3_34","type":"book-chapter","created":{"date-parts":[[2014,5,29]],"date-time":"2014-05-29T02:22:12Z","timestamp":1401330132000},"page":"328-333","source":"Crossref","is-referenced-by-count":4,"title":["Optimizing Alloy for Multi-objective Software Product Line Configuration"],"prefix":"10.1007","author":[{"given":"Ed","family":"Zulkoski","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Chris","family":"Kleynhans","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ming-Ho","family":"Yee","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Derek","family":"Rayside","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Krzysztof","family":"Czarnecki","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"34_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"102","DOI":"10.1007\/978-3-642-19440-5_7","volume-title":"Software Language Engineering","author":"K. B\u0105k","year":"2011","unstructured":"B\u0105k, K., Czarnecki, K., W\u0105sowski, A.: Feature and Meta-Models in Clafer: Mixed, Specialized, and Coupled. In: Malloy, B., Staab, S., van den Brand, M. (eds.) SLE 2010. LNCS, vol.\u00a06563, pp. 102\u2013122. Springer, Heidelberg (2011)"},{"key":"34_CR2","unstructured":"Brummayer, R.: Efficient SMT solving for bit vectors and the extensional theory of arrays. Ph.D. thesis, JKU Linz (2010)"},{"key":"34_CR3","unstructured":"Clements, P.C., Northrop, L.: Software Product Lines: Practices and Patterns. Addison-Wesley (2001)"},{"key":"34_CR4","unstructured":"Esfahani, N., Malek, S.: Guided Exploration of the Architectural Solution Space in the Face of Uncertainty. Tech. rep., George Mason U., Dept. of C.S. (March 2011)"},{"key":"34_CR5","unstructured":"Franzen, A.: Efficient solving of the satisfiability modulo bit-vectors problem and some extensions to SMT. Ph.D. thesis, Univ. of Trento (2010)"},{"key":"34_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"519","DOI":"10.1007\/978-3-540-73368-3_52","volume-title":"Computer Aided Verification","author":"V. Ganesh","year":"2007","unstructured":"Ganesh, V., Dill, D.L.: A Decision Procedure for Bit-Vectors and Arrays. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 519\u2013531. Springer, Heidelberg (2007)"},{"key":"34_CR7","doi-asserted-by":"crossref","unstructured":"Kang, K.C., Cohen, S.G., Hess, J.A., Novak, W.E., Peterson, A.S.: Feature-Oriented Domain Analysis (FODA) feasibility study. Tech. rep., SEI-CMU (1990)","DOI":"10.21236\/ADA235785"},{"key":"34_CR8","unstructured":"Knuth, D.E., Bendix, P.B.: Simple word problems in universal algebra. In: Proc. Conf. on Computational Problems in Abstract Algebra. Pergamon Press (1970)"},{"key":"34_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1007\/978-3-642-27705-4_12","volume-title":"Verified Software: Theories, Tools, Experiments","author":"F. Merz","year":"2012","unstructured":"Merz, F., Falke, S., Sinz, C.: LLBMC: Bounded Model Checking of C and C++ Programs Using a Compiler IR. In: Joshi, R., M\u00fcller, P., Podelski, A. (eds.) VSTTE 2012. LNCS, vol.\u00a07152, pp. 146\u2013161. Springer, Heidelberg (2012)"},{"key":"34_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"122","DOI":"10.1007\/978-3-642-30885-7_9","volume-title":"Abstract State Machines, Alloy, B, VDM, and Z","author":"V. Montaghami","year":"2012","unstructured":"Montaghami, V., Rayside, D.: Extending Alloy with partial instances. In: Derrick, J., Fitzgerald, J., Gnesi, S., Khurshid, S., Leuschel, M., Reeves, S., Riccobene, E. (eds.) ABZ 2012. LNCS, vol.\u00a07316, pp. 122\u2013135. Springer, Heidelberg (2012)"},{"key":"34_CR11","doi-asserted-by":"crossref","unstructured":"Olaechea, R., Stewart, S., Czarnecki, K., Rayside, D.: Modelling and Optimization of Quality Attributes in Variability-Rich Software. In: NFPinDSML Workshop at MODELS Conference (2012)","DOI":"10.1145\/2420942.2420944"},{"key":"34_CR12","doi-asserted-by":"crossref","unstructured":"Pohl, K., B\u00f6ckle, G., van der Linden, F.J.: Software Product Line Engineering: Foundations, Principles and Techniques. Springer (2005)","DOI":"10.1007\/3-540-28901-1"},{"key":"34_CR13","unstructured":"Rayside, D., Estler, H.-C., Jackson, D.: A Guided Improvement Algorithm for Exact, General Purpose, Many-Objective Combinatorial Optimization. Tech. Rep. MIT-CSAIL-TR-2009-033, MIT CSAIL (2009)"},{"key":"34_CR14","doi-asserted-by":"crossref","unstructured":"Siegmund, N., Kolesnikov, S., Kastner, C., Appel, S., Batory, D., Rosenmuller, M., Saake, G.: Predicting performance via automated feature-interaction detection. In: Murphy, G., Pezze, M. (eds.) Proc. 34th ICSE, Zurich, Switzerland (2012)","DOI":"10.1109\/ICSE.2012.6227196"},{"key":"34_CR15","doi-asserted-by":"crossref","unstructured":"Siegmund, N., Rosenmuller, M., Kastner, C., Giarrusso, P.G., Apel, S., Kolesnikov, S.S.: Scalable prediction of non-functional properties in software product lines. In: Schaefer, I., John, I., Schmid, K. (eds.) SPLC Workshops. ACM (2011)","DOI":"10.1109\/SPLC.2011.20"},{"issue":"3","key":"34_CR16","first-page":"1","volume":"1","author":"N. Siegmund","year":"2011","unstructured":"Siegmund, N., Rosenmuller, M., Kuhlemann, M., Kastner, C., Apel, S., Saake, G.: SPL Conqueror: Toward optimization of non-functional properties in software product lines. Software Quality Journal\u00a01(3), 1\u201331 (2011)","journal-title":"Software Quality Journal"},{"issue":"1","key":"34_CR17","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/s10703-012-0156-2","volume":"42","author":"C. Wintersteiger","year":"2013","unstructured":"Wintersteiger, C., Hamadi, Y., de Moura, L.: Efficiently solving quantified bit-vector formulas. Formal Methods in System Design\u00a042(1), 3\u201323 (2013)","journal-title":"Formal Methods in System Design"}],"container-title":["Lecture Notes in Computer Science","Abstract State Machines, Alloy, B, TLA, VDM, and Z"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-43652-3_34","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,26]],"date-time":"2019-05-26T23:05:45Z","timestamp":1558911945000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-43652-3_34"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783662436516","9783662436523"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-43652-3_34","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014]]}}}