{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,14]],"date-time":"2026-02-14T00:56:37Z","timestamp":1771030597786,"version":"3.50.1"},"publisher-location":"Cham","reference-count":43,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319631387","type":"print"},{"value":"9783319631394","type":"electronic"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"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":[[2017]]},"DOI":"10.1007\/978-3-319-63139-4_4","type":"book-chapter","created":{"date-parts":[[2017,7,23]],"date-time":"2017-07-23T23:22:55Z","timestamp":1500852175000},"page":"59-75","source":"Crossref","is-referenced-by-count":9,"title":["MiniZinc with Strings"],"prefix":"10.1007","author":[{"given":"Roberto","family":"Amadini","sequence":"first","affiliation":[]},{"given":"Pierre","family":"Flener","sequence":"additional","affiliation":[]},{"given":"Justin","family":"Pearson","sequence":"additional","affiliation":[]},{"given":"Joseph D.","family":"Scott","sequence":"additional","affiliation":[]},{"given":"Peter J.","family":"Stuckey","sequence":"additional","affiliation":[]},{"given":"Guido","family":"Tack","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,7,25]]},"reference":[{"key":"4_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"462","DOI":"10.1007\/978-3-319-21690-4_29","volume-title":"Computer Aided Verification","author":"PA Abdulla","year":"2015","unstructured":"Abdulla, P.A., Atig, M.F., Chen, Y.-F., Hol\u00edk, L., Rezine, A., R\u00fcmmer, P., Stenman, J.: Norn: an SMT solver for string constraints. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 462\u2013469. Springer, Cham (2015). doi: 10.1007\/978-3-319-21690-4_29"},{"key":"4_CR2","unstructured":"Amadini, R., Gabbrielli, M., Mauro, J.: A multicore tool for constraint solving. In: IJCAI, pp. 232\u2013238. AAAI Press (2015)"},{"key":"4_CR3","doi-asserted-by":"crossref","unstructured":"Beldiceanu, N., Carlsson, M., Demassey, S., Petit, T.: Global constraint catalogue: past, present and future. Constraints 12(1), 21\u201362 (2007). http:\/\/sofdem.github.io\/gccat\/","DOI":"10.1007\/s10601-006-9010-8"},{"key":"4_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1007\/978-3-319-44953-1_4","volume-title":"Principles and Practice of Constraint Programming","author":"G Belov","year":"2016","unstructured":"Belov, G., Stuckey, P.J., Tack, G., Wallace, M.: Improved linearization of constraint programming models. In: Rueher, M. (ed.) CP 2016. LNCS, vol. 9892, pp. 49\u201365. Springer, Cham (2016). doi: 10.1007\/978-3-319-44953-1_4"},{"key":"4_CR5","doi-asserted-by":"crossref","unstructured":"Bisht, P., Hinrichs, T.L., Skrupsky, N., Venkatakrishnan, V.N.: WAPTEC: whitebox analysis of web applications for parameter tampering exploit construction. In: CCS, pp. 575\u2013586. ACM (2011)","DOI":"10.1145\/2046707.2046774"},{"key":"4_CR6","unstructured":"Bj\u00f6rdal, G.: String variables for constraint-based local search. Master\u2019s thesis, Department of Information Technology, Uppsala University, Sweden, August 2016. http:\/\/urn.kb.se\/resolve?urn=urn:nbn:se:uu:diva-301501"},{"issue":"3","key":"4_CR7","doi-asserted-by":"crossref","first-page":"325","DOI":"10.1007\/s10601-015-9184-z","volume":"20","author":"G Bj\u00f6rdal","year":"2015","unstructured":"Bj\u00f6rdal, G., Monette, J.-N., Flener, P., Pearson, J.: A constraint-based local search backend for MiniZinc. Constraints 20(3), 325\u2013345 (2015)","journal-title":"Constraints"},{"key":"4_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1007\/978-3-642-00768-2_27","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"N Bj\u00f8rner","year":"2009","unstructured":"Bj\u00f8rner, N., Tillmann, N., Voronkov, A.: Path feasibility analysis for string-manipulating programs. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 307\u2013321. Springer, Heidelberg (2009). doi: 10.1007\/978-3-642-00768-2_27"},{"key":"4_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"300","DOI":"10.1007\/978-3-642-14186-7_25","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2010","author":"M Bofill","year":"2010","unstructured":"Bofill, M., Suy, J., Villaret, M.: A system for solving constraint satisfaction problems with SMT. In: Strichman, O., Szeider, S. (eds.) SAT 2010. LNCS, vol. 6175, pp. 300\u2013305. Springer, Heidelberg (2010). doi: 10.1007\/978-3-642-14186-7_25"},{"key":"4_CR10","unstructured":"Chu, G.: Improving Combinatorial Optimization. Ph.D. thesis, Department of Computing and Information Systems, University of Melbourne, Australia (2011)"},{"issue":"2","key":"4_CR11","doi-asserted-by":"crossref","first-page":"245","DOI":"10.1002\/spe.2218","volume":"45","author":"G Costantini","year":"2015","unstructured":"Costantini, G., Ferrara, P., Cortesi, A.: A suite of abstract domains for static analysis of string values. Softw. Pract. Exp. 45(2), 245\u2013287 (2015)","journal-title":"Softw. Pract. Exp."},{"key":"4_CR12","unstructured":"De Landtsheer, R., Ponsard, C.: OscaR.cbls: an open source framework for constraint-based local search. In: ORBEL-27, the 27th Annual Conference of the Belgian Operational Research Society (2013). http:\/\/www.orbel.be\/orbel27\/pdf\/abstract293.pdf ; The OscaR.cbls solver https:\/\/bitbucket.org\/oscarlib\/oscar\/wiki\/CBLS"},{"key":"4_CR13","doi-asserted-by":"crossref","unstructured":"Emmi, M., Majumdar, R., Sen, K.: Dynamic test input generation for database applications. In: ISSTA, pp. 151\u2013162. ACM (2007)","DOI":"10.1145\/1273463.1273484"},{"issue":"6","key":"4_CR14","doi-asserted-by":"crossref","first-page":"847","DOI":"10.1007\/s00165-011-0214-3","volume":"25","author":"X Fu","year":"2013","unstructured":"Fu, X., Powell, M.C., Bantegui, M., Li, C.: Simple linear string constraints. Formal Aspects Comput. 25(6), 847\u2013891 (2013)","journal-title":"Formal Aspects Comput."},{"key":"4_CR15","unstructured":"Fujiwara, T.: iZplus description (2016). http:\/\/www.minizinc.org\/challenge2016\/description_izplus.txt"},{"key":"4_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1007\/978-3-642-39611-3_21","volume-title":"Hardware and Software: Verification and Testing","author":"V Ganesh","year":"2013","unstructured":"Ganesh, V., Minnes, M., Solar-Lezama, A., Rinard, M.: Word equations with length constraints: what\u2019s decidable? In: Biere, A., Nahir, A., Vos, T. (eds.) HVC 2012. LNCS, vol. 7857, pp. 209\u2013226. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-39611-3_21"},{"key":"4_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"277","DOI":"10.1007\/978-3-642-36742-7_20","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"G Gange","year":"2013","unstructured":"Gange, G., Navas, J.A., Stuckey, P.J., S\u00f8ndergaard, H., Schachte, P.: Unbounded model-checking with interpolation for regular language constraints. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 277\u2013291. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-36742-7_20"},{"key":"4_CR18","unstructured":"Gecode Team. Gecode: generic constraint development environment (2016). http:\/\/www.gecode.org"},{"key":"4_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1007\/978-3-319-21215-9_9","volume-title":"Tests and Proofs","author":"O Grinchtein","year":"2015","unstructured":"Grinchtein, O., Carlsson, M., Pearson, J.: A constraint optimisation model for analysis of telecommunication protocol logs. In: Blanchette, J.C., Kosmatov, N. (eds.) TAP 2015. LNCS, vol. 9154, pp. 137\u2013154. Springer, Cham (2015). doi: 10.1007\/978-3-319-21215-9_9"},{"key":"4_CR20","unstructured":"Gurobi Optimization, Inc., Gurobi Optimizer Reference Manual (2016). http:\/\/www.gurobi.com"},{"key":"4_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"381","DOI":"10.1007\/978-3-642-40627-0_31","volume-title":"Principles and Practice of Constraint Programming","author":"J He","year":"2013","unstructured":"He, J., Flener, P., Pearson, J., Zhang, W.M.: Solving string constraints: the case for constraint programming. In: Schulte, C. (ed.) CP 2013. LNCS, vol. 8124, pp. 381\u2013397. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-40627-0_31"},{"issue":"4","key":"4_CR22","doi-asserted-by":"crossref","first-page":"531","DOI":"10.1007\/s10515-012-0111-x","volume":"19","author":"P Hooimeijer","year":"2012","unstructured":"Hooimeijer, P., Weimer, W.: StrSolve: solving string constraints lazily. Autom. Softw. Eng. 19(4), 531\u2013559 (2012)","journal-title":"Autom. Softw. Eng."},{"issue":"4","key":"4_CR23","doi-asserted-by":"crossref","first-page":"25","DOI":"10.1145\/2377656.2377662","volume":"21","author":"A Kiezun","year":"2012","unstructured":"Kiezun, A., Ganesh, V., Artzi, S., Guo, P.J., Hooimeijer, P., Ernst, M.D.: HAMPI: a solver for word equations over strings, regular expressions, and context-free grammars. ACM Trans. Softw. Eng. Methodol. 21(4), 25 (2012)","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"key":"4_CR24","doi-asserted-by":"crossref","unstructured":"Kie\u017cun, A., Ganesh, V., Guo, P.J., Hooimeijer, P., Ernst, M.D.: HAMPI: a solver for string constraints. In: ISSTA 2009, pp. 105\u2013116. ACM (2009)","DOI":"10.1145\/1572272.1572286"},{"key":"4_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"372","DOI":"10.1007\/978-3-319-12736-1_20","volume-title":"Programming Languages and Systems","author":"S-W Kim","year":"2014","unstructured":"Kim, S.-W., Chin, W., Park, J., Kim, J., Ryu, S.: Inferring grammatical summaries of string values. In: Garrigue, J. (ed.) APLAS 2014. LNCS, vol. 8858, pp. 372\u2013391. Springer, Cham (2014). doi: 10.1007\/978-3-319-12736-1_20"},{"key":"4_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1007\/978-3-319-03077-7_2","volume-title":"Hardware and Software: Verification and Testing","author":"G Li","year":"2013","unstructured":"Li, G., Ghosh, I.: PASS: string solving with parameterized array and interval automaton. In: Bertacco, V., Legay, A. (eds.) HVC 2013. LNCS, vol. 8244, pp. 15\u201331. Springer, Cham (2013). doi: 10.1007\/978-3-319-03077-7_2"},{"key":"4_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"646","DOI":"10.1007\/978-3-319-08867-9_43","volume-title":"Computer Aided Verification","author":"T Liang","year":"2014","unstructured":"Liang, T., Reynolds, A., Tinelli, C., Barrett, C., Deters, M.: A DPLL(T) theory solver for a theory of strings and regular expressions. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 646\u2013662. Springer, Cham (2014). doi: 10.1007\/978-3-319-08867-9_43"},{"key":"4_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"197","DOI":"10.1007\/978-3-642-54807-9_12","volume-title":"Compiler Construction","author":"M Madsen","year":"2014","unstructured":"Madsen, M., Andreasen, E.: String analysis for dynamic field access. In: Cohen, A. (ed.) CC 2014. LNCS, vol. 8409, pp. 197\u2013217. Springer, Heidelberg (2014). doi: 10.1007\/978-3-642-54807-9_12"},{"key":"4_CR29","doi-asserted-by":"publisher","unstructured":"Michel, L.D., Van Hentenryck, P.: Constraint satisfaction over bit-vectors. In: Milano, M. (ed.) CP 2012. LNCS, pp. 527\u2013543. Springer, Heidelberg (2012). doi: 10.1007\/978-3-642-33558-7_39","DOI":"10.1007\/978-3-642-33558-7_39"},{"key":"4_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"529","DOI":"10.1007\/978-3-540-74970-7_38","volume-title":"Principles and Practice of Constraint Programming \u2013 CP 2007","author":"N Nethercote","year":"2007","unstructured":"Nethercote, N., Stuckey, P.J., Becket, R., Brand, S., Duck, G.J., Tack, G.: MiniZinc: towards a standard CP modelling language. In: Bessi\u00e8re, C. (ed.) CP 2007. LNCS, vol. 4741, pp. 529\u2013543. Springer, Heidelberg (2007). doi: 10.1007\/978-3-540-74970-7_38"},{"issue":"3","key":"4_CR31","doi-asserted-by":"crossref","first-page":"357","DOI":"10.1007\/s10601-008-9064-x","volume":"14","author":"O Ohrimenko","year":"2009","unstructured":"Ohrimenko, O., Stuckey, P.J., Codish, M.: Propagation via lazy clause generation. Constraints 14(3), 357\u2013391 (2009)","journal-title":"Constraints"},{"key":"4_CR32","doi-asserted-by":"crossref","unstructured":"Saxena, P., Akhawe, D., Hanna, S., Mao, F., McCamant, S., Song, D.: A symbolic execution framework for JavaScript. In: S&P, pp. 513\u2013528. IEEE Computer Society (2010)","DOI":"10.1109\/SP.2010.38"},{"key":"4_CR33","unstructured":"Scott, J.D.: Other Things Besides Number: Abstraction, Constraint Propagation, and String Variable Types. Ph.D. thesis, Department of Information Technology, Uppsala University, Sweden (2016). http:\/\/urn.kb.se\/resolve?urn=urn:nbn:se:uu:diva-273311"},{"key":"4_CR34","doi-asserted-by":"crossref","unstructured":"Scott, J.D., Flener, P., Pearson, J.: Bounded strings for constraint programming. In: ICTAI, pp. 1036\u20131043. IEEE Computer Society (2013)","DOI":"10.1109\/ICTAI.2013.155"},{"key":"4_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"375","DOI":"10.1007\/978-3-319-18008-3_26","volume-title":"Integration of AI and OR Techniques in Constraint Programming","author":"JD Scott","year":"2015","unstructured":"Scott, J.D., Flener, P., Pearson, J.: Constraint solving on bounded string variables. In: Michel, L. (ed.) CPAIOR 2015. LNCS, vol. 9075, pp. 375\u2013392. Springer, Cham (2015). doi: 10.1007\/978-3-319-18008-3_26"},{"key":"4_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1007\/978-3-319-59776-8_5","volume-title":"Integration of AI and OR Techniques in Constraint Programming","author":"JD Scott","year":"2017","unstructured":"Scott, J.D., Flener, P., Pearson, J., Schulte, C.: Design and implementation of bounded-length sequence variables. In: Salvagnin, D., Lombardi, M. (eds.) CPAIOR 2017. LNCS, vol. 10335, pp. 51\u201367. Springer, Cham (2017). doi: 10.1007\/978-3-319-59776-8_5"},{"key":"4_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"268","DOI":"10.1007\/978-3-642-38171-3_18","volume-title":"Integration of AI and OR Techniques in Constraint Programming for Combinatorial Optimization Problems","author":"PJ Stuckey","year":"2013","unstructured":"Stuckey, P.J., Tack, G.: MiniZinc with functions. In: Gomes, C., Sellmann, M. (eds.) CPAIOR 2013. LNCS, vol. 7874, pp. 268\u2013283. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-38171-3_18"},{"key":"4_CR38","doi-asserted-by":"crossref","unstructured":"Subramanian, S., Berzish, M., Zheng, Y., Tripp, O., Ganesh, V.: A solver for a theory of strings and bit-vectors. CoRR, abs\/1605.09446 (2016)","DOI":"10.1109\/ICSE-C.2017.73"},{"key":"4_CR39","doi-asserted-by":"crossref","unstructured":"Trinh, M., Chu, D., Jaffar, J.: S3: a symbolic string solver for vulnerability detection in web applications. In: SIGSAC, pp. 1232\u20131243. ACM (2014)","DOI":"10.1145\/2660267.2660372"},{"key":"4_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/978-3-642-12002-2_13","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"F Yu","year":"2010","unstructured":"Yu, F., Alkhalaf, M., Bultan, T.: Stranger: an automata-based string analysis tool for PHP. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 154\u2013157. Springer, Heidelberg (2010). doi: 10.1007\/978-3-642-12002-2_13"},{"key":"4_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1007\/978-3-319-21690-4_14","volume-title":"Computer Aided Verification","author":"Y Zheng","year":"2015","unstructured":"Zheng, Y., Ganesh, V., Subramanian, S., Tripp, O., Dolby, J., Zhang, X.: Effective search-space pruning for solvers of string equations, regular expressions and length constraints. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 235\u2013254. Springer, Cham (2015). doi: 10.1007\/978-3-319-21690-4_14"},{"key":"4_CR42","doi-asserted-by":"crossref","unstructured":"Zheng, Y., Zhang, X., Ganesh, V.: Z3-str: a Z3-based string solver for web application analysis. In: SIGSOFT, pp. 114\u2013124. ACM (2013)","DOI":"10.1145\/2491411.2491456"},{"key":"4_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"48","DOI":"10.1007\/978-3-319-28228-2_4","volume-title":"Practical Aspects of Declarative Languages","author":"N-F Zhou","year":"2016","unstructured":"Zhou, N.-F., Kjellerstrand, H.: The Picat-SAT compiler. In: Gavanelli, M., Reppy, J. (eds.) PADL 2016. LNCS, vol. 9585, pp. 48\u201362. Springer, Cham (2016). doi: 10.1007\/978-3-319-28228-2_4"}],"container-title":["Lecture Notes in Computer Science","Logic-Based Program Synthesis and Transformation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-63139-4_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,1]],"date-time":"2019-10-01T08:33:29Z","timestamp":1569918809000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-63139-4_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319631387","9783319631394"],"references-count":43,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-63139-4_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017]]}}}