{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T09:23:06Z","timestamp":1743067386689,"version":"3.40.3"},"publisher-location":"Cham","reference-count":36,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319180076"},{"type":"electronic","value":"9783319180083"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"vor","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":[[2015]]},"DOI":"10.1007\/978-3-319-18008-3_26","type":"book-chapter","created":{"date-parts":[[2015,4,15]],"date-time":"2015-04-15T07:32:51Z","timestamp":1429083171000},"page":"375-392","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":9,"title":["Constraint Solving on Bounded String Variables"],"prefix":"10.1007","author":[{"given":"Joseph D.","family":"Scott","sequence":"first","affiliation":[]},{"given":"Pierre","family":"Flener","sequence":"additional","affiliation":[]},{"given":"Justin","family":"Pearson","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,4,16]]},"reference":[{"key":"26_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"150","DOI":"10.1007\/978-3-319-08867-9_10","volume-title":"Computer Aided Verification","author":"PA Abdulla","year":"2014","unstructured":"Abdulla, P.A., Atig, M.F., Chen, Y.-F., Hol\u00edk, L., Rezine, A., R\u00fcmmer, P., Stenman, J.: String constraints for verification. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 150\u2013166. Springer, Heidelberg (2014)"},{"issue":"7","key":"26_CR2","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/390013.808479","volume":"5","author":"FE Allen","year":"1970","unstructured":"Allen, F.E.: Control flow analysis. ACM Sigplan Notices 5(7), 1\u201319 (1970)","journal-title":"ACM Sigplan Notices"},{"issue":"1","key":"26_CR3","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1023\/A:1021805623454","volume":"118","author":"R Bart\u00e1k","year":"2003","unstructured":"Bart\u00e1k, R.: Dynamic global constraints in backtracking based environments. Annals of Operations Research 118(1), 101\u2013119 (2003)","journal-title":"Annals of Operations Research"},{"key":"26_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1007\/978-3-540-30201-8_11","volume-title":"Principles and Practice of Constraint Programming \u2013 CP 2004","author":"N Beldiceanu","year":"2004","unstructured":"Beldiceanu, N., Carlsson, M., Petit, T.: Deriving filtering algorithms from constraint checkers. In: Wallace, M. (ed.) CP 2004. LNCS, vol. 3258, pp. 107\u2013122. Springer, Heidelberg (2004)"},{"key":"26_CR5","doi-asserted-by":"crossref","unstructured":"Bisht, P., Hinrichs, T., Skrupsky, N., Venkatakrishnan, V.N.: WAPTEC: whitebox analysis of web applications for parameter tampering exploit construction. In: Chen, Y., Danezis, G., Shmatikov, V. (eds.) Computer and Communications Security (CCS 2011), pp. 575\u2013586. ACM (2011)","DOI":"10.1145\/2046707.2046774"},{"key":"26_CR6","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)"},{"issue":"3","key":"26_CR7","doi-asserted-by":"publisher","first-page":"215","DOI":"10.1109\/TSE.1976.233817","volume":"2","author":"LA Clarke","year":"1976","unstructured":"Clarke, L.A.: A system to generate test data and symbolically execute programs. IEEE Transactions on Software Engineering 2(3), 215\u2013222 (1976)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"26_CR8","doi-asserted-by":"crossref","unstructured":"Emmi, M., Majumdar, R., Sen, K.: Dynamic test input generation for database applications. In: Rosenblum, D.S., Elbaum, S.G. (eds.) Software Testing and Analysis (ISSTA 2007), pp. 151\u2013162. ACM (2007)","DOI":"10.1145\/1273463.1273484"},{"key":"26_CR9","doi-asserted-by":"publisher","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.C.: Simple linear string constraints. Formal Aspects of Computing 25, 847\u2013891 (2013). sushi is available from http:\/\/people.hofstra.edu\/Xiang_Fu\/XiangFu\/projects\/SAFELI\/SUSHI.php","journal-title":"Formal Aspects of Computing"},{"key":"26_CR10","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. 4590, pp. 519\u2013531. Springer, Heidelberg (2007). stp is available from https:\/\/sites.google.com\/site\/stpfastprover\/"},{"key":"26_CR11","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)"},{"key":"26_CR12","unstructured":"Gecode Team: Gecode: A generic constraint development environment (2006). http:\/\/www.gecode.org"},{"key":"26_CR13","doi-asserted-by":"crossref","unstructured":"Gervet, C.: Constraints over structured domains. In: Rossi, F., van Beek, P., Walsh, T. (eds.) Handbook of Constraint Programming, chap. 17, pp. 605\u2013638. Elsevier (2006)","DOI":"10.1016\/S1574-6526(06)80021-0"},{"key":"26_CR14","doi-asserted-by":"crossref","unstructured":"Ghosh, I., Shafiei, N., Li, G., Chiang, W.F.: JST: an automatic test generation tool for industrial Java applications with strings. In: Notkin, D., Cheng, B.H.C., Pohl, K. (eds.) International Conference on Software Engineering (ICSE 2013), pp. 992\u20131001. IEEE \/ ACM (2013)","DOI":"10.1109\/ICSE.2013.6606649"},{"key":"26_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"377","DOI":"10.1007\/978-3-540-45193-8_26","volume-title":"Principles and Practice of Constraint Programming \u2013 CP 2003","author":"K Golden","year":"2003","unstructured":"Golden, K., Pang, W.: Constraint reasoning over strings. In: Rossi, F. (ed.) CP 2003. LNCS, vol. 2833, pp. 377\u2013391. Springer, Heidelberg (2003)"},{"key":"26_CR16","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)"},{"key":"26_CR17","doi-asserted-by":"crossref","unstructured":"Hooimeijer, P., Weimer, W.: A decision procedure for subset constraints over regular languages. In: Hind, M., Diwan, A. (eds.) Programming Language Design and Implementation (PLDI 2009), pp. 188\u2013198. ACM (2009)","DOI":"10.1145\/1543135.1542498"},{"issue":"4","key":"26_CR18","doi-asserted-by":"publisher","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. Automated Software Engineering 19(4), 531\u2013559 (2012)","journal-title":"Automated Software Engineering"},{"key":"26_CR19","unstructured":"Kie\u017cun, A., Ganesh, V., Guo, P.J., Hooimeijer, P., Ernst, M.D.: HAMPI: a solver for string constraints. In: Rothermel, G., Dillon, L.K. (eds.) International Symposium on Software Testing and Analysis (ISSTA 2009), pp. 105\u2013116. ACM (2009). hampi is available from http:\/\/people.csail.mit.edu\/akiezun\/hampi\/"},{"issue":"7","key":"26_CR20","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1145\/360248.360252","volume":"19","author":"JC King","year":"1976","unstructured":"King, J.C.: Symbolic execution and program testing. Commun. ACM 19(7), 385\u2013394 (1976)","journal-title":"Commun. ACM"},{"key":"26_CR21","doi-asserted-by":"crossref","unstructured":"Lothaire, M.: Combinatorics on words. Cambridge Mathematical Library, Cambridge University Press (1997)","DOI":"10.1017\/CBO9780511566097"},{"key":"26_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"163","DOI":"10.1007\/978-3-642-01929-6_13","volume-title":"Integration of AI and OR Techniques in Constraint Programming for Combinatorial Optimization Problems","author":"MJ Maher","year":"2009","unstructured":"Maher, M.J.: Open constraints in a boundable world. In: van Hoeve, W.-J., Hooker, J.N. (eds.) CPAIOR 2009. LNCS, vol. 5547, pp. 163\u2013177. Springer, Heidelberg (2009)"},{"issue":"2","key":"26_CR23","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1070\/SM1977v032n02ABEH002376","volume":"32","author":"G Makanin","year":"1977","unstructured":"Makanin, G.: The problem of solvability of equations in a free semigroup. Sbornik: Mathematics 32(2), 129\u2013198 (1977)","journal-title":"Sbornik: Mathematics"},{"key":"26_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"527","DOI":"10.1007\/978-3-642-33558-7_39","volume-title":"Principles and Practice of Constraint Programming","author":"LD Michel","year":"2012","unstructured":"Michel, L.D., Van Hentenryck, P.: Constraint satisfaction over bit-vectors. In: Milano, M. (ed.) CP 2012. LNCS, vol. 7514, pp. 527\u2013543. Springer, Heidelberg (2012)"},{"key":"26_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"544","DOI":"10.1007\/978-3-642-33558-7_40","volume-title":"Principles and Practice of Constraint Programming","author":"J-N Monette","year":"2012","unstructured":"Monette, J.-N., Flener, P., Pearson, J.: Towards solver-independent propagators. In: Milano, M. (ed.) CP 2012. LNCS, vol. 7514, pp. 544\u2013560. Springer, Heidelberg (2012). the indexical compiler is available from http:\/\/www.it.uu.se\/research\/group\/astra\/software#indexicals"},{"key":"26_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"482","DOI":"10.1007\/978-3-540-30201-8_36","volume-title":"Principles and Practice of Constraint Programming \u2013 CP 2004","author":"G Pesant","year":"2004","unstructured":"Pesant, G.: A regular language membership constraint for finite sequences of variables. In: Wallace, M. (ed.) CP 2004. LNCS, vol. 3258, pp. 482\u2013495. Springer, Heidelberg (2004)"},{"key":"26_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"751","DOI":"10.1007\/11889205_64","volume-title":"Principles and Practice of Constraint Programming - CP 2006","author":"C-G Quimper","year":"2006","unstructured":"Quimper, C.-G., Walsh, T.: Global grammar constraints. In: Benhamou, F. (ed.) CP 2006. LNCS, vol. 4204, pp. 751\u2013755. Springer, Heidelberg (2006)"},{"key":"26_CR28","doi-asserted-by":"crossref","unstructured":"Redelinghuys, G., Visser, W., Geldenhuys, J.: Symbolic execution of programs with strings. In: Kroeze, J.H., de Villiers, R. (eds.) South African Institute of Computer Scientists and Information Technologists Conference (SAICSIT 2012), pp. 139\u2013148. ACM (2012)","DOI":"10.1145\/2389836.2389853"},{"key":"26_CR29","unstructured":"Saxena, P., Akhawe, D., Hanna, S., Mao, F., McCamant, S., Song, D.: A symbolic execution framework for JavaScript. In: Security and Privacy (S&P 2010), pp. 513\u2013528. IEEE Computer Society (2010). kaluza is available from http:\/\/webblaze.cs.berkeley.edu\/2010\/kaluza\/"},{"key":"26_CR30","unstructured":"Scott, J.D.: Rapid prototyping of a structured domain through indexical compilation. In: Schaus, P., Monette, J.N. (eds.) Domain Specific Languages in Combinatorial Optimization (CoSpeL workshop at CP 2013) (2013). http:\/\/cp2013.a4cp.org\/workshops\/cospel"},{"key":"26_CR31","doi-asserted-by":"crossref","unstructured":"Scott, J.D., Flener, P., Pearson, J.: Bounded strings for constraint programming. In: Tools with Artificial Intelligence (ICTAI 2013), pp. 1036\u20131043. IEEE Computer Society (2013)","DOI":"10.1109\/ICTAI.2013.155"},{"key":"26_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"530","DOI":"10.1007\/11889205_38","volume-title":"Principles and Practice of Constraint Programming - CP 2006","author":"M Sellmann","year":"2006","unstructured":"Sellmann, M.: The theory of grammar constraints. In: Benhamou, F. (ed.) CP 2006. LNCS, vol. 4204, pp. 530\u2013544. Springer, Heidelberg (2006)"},{"key":"26_CR33","doi-asserted-by":"crossref","unstructured":"Trinh, M.T., Chu, D.H., Jaffar, J.: S3: A symbolic string solver for vulnerability detection in web applications. In: Computer and Communications Security (CCS 2014) (2014)","DOI":"10.1145\/2660267.2660372"},{"key":"26_CR34","doi-asserted-by":"crossref","unstructured":"Van Hentenryck, P., Saraswat, V.A., Deville, Y.: Design, implementation, and evaluation of the constraint language cc(FD). techreport CS-93-02, Brown University, Providence, USA (January 1993), revised version: Journal of Logic Programming 37(1\u20133), 293\u2013316 (1998)","DOI":"10.1016\/S0743-1066(98)10006-7"},{"key":"26_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"322","DOI":"10.1007\/978-3-642-00768-2_28","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"F Yu","year":"2009","unstructured":"Yu, F., Bultan, T., Ibarra, O.H.: Symbolic string verification: combining string analysis and size analysis. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 322\u2013336. Springer, Heidelberg (2009)"},{"key":"26_CR36","doi-asserted-by":"crossref","unstructured":"Zheng, Y., Zhang, X., Ganesh, V.: Z3-str: A Z3-based string solver for web application analysis. In: Meyer, B., Baresi, L., Mezini, M. (eds.) Foundations of Software Engineering (FSE 2013), pp. 114\u2013124. ACM (2013)","DOI":"10.1145\/2491411.2491456"}],"container-title":["Lecture Notes in Computer Science","Integration of AI and OR Techniques in Constraint Programming"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-18008-3_26","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,12,30]],"date-time":"2020-12-30T20:08:12Z","timestamp":1609358892000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-18008-3_26"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319180076","9783319180083"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-18008-3_26","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"16 April 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}