{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T02:08:44Z","timestamp":1776305324875,"version":"3.50.1"},"publisher-location":"Cham","reference-count":33,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030510732","type":"print"},{"value":"9783030510749","type":"electronic"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2020]]},"DOI":"10.1007\/978-3-030-51074-9_13","type":"book-chapter","created":{"date-parts":[[2020,6,29]],"date-time":"2020-06-29T22:02:47Z","timestamp":1593468167000},"page":"218-237","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["A Decision Procedure for String to Code Point Conversion"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-3529-8682","authenticated-orcid":false,"given":"Andrew","family":"Reynolds","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8669-0011","authenticated-orcid":false,"given":"Andres","family":"N\u00f6tzli","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9522-3084","authenticated-orcid":false,"given":"Clark","family":"Barrett","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6726-775X","authenticated-orcid":false,"given":"Cesare","family":"Tinelli","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2020,6,24]]},"reference":[{"key":"13_CR1","unstructured":"$$\\rm str\\_int\\_benchmarks$$ (2019). https:\/\/github.com\/plfm-iis\/str_int_benchmarks"},{"key":"13_CR2","unstructured":"z3-Trau (2020). https:\/\/github.com\/guluchen\/z3\/releases\/tag\/z3-trau"},{"key":"13_CR3","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., et al.: Flatten and conquer: a framework for efficient analysis of string constraints. In: Cohen and Vechev [15], pp. 602\u2013617 (2017)","DOI":"10.1145\/3140587.3062384"},{"key":"13_CR4","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., et al.: String constraints for verification. In: Biere and Bloem [12], pp. 150\u2013166 (2014)","DOI":"10.1007\/978-3-319-08867-9_10"},{"key":"13_CR5","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., et al.: 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). https:\/\/doi.org\/10.1007\/978-3-319-21690-4_29"},{"key":"13_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"277","DOI":"10.1007\/978-3-030-31784-3_16","volume-title":"Automated Technology for Verification and Analysis","author":"PA Abdulla","year":"2019","unstructured":"Abdulla, P.A., Atig, M.F., Diep, B.P., Hol\u00edk, L., Jank\u016f, P.: Chain-free string constraints. In: Chen, Y.-F., Cheng, C.-H., Esparza, J. (eds.) ATVA 2019. LNCS, vol. 11781, pp. 277\u2013293. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-31784-3_16"},{"key":"13_CR7","doi-asserted-by":"crossref","unstructured":"Backes, J., et al.: Semantic-based automated reasoning for AWS access policies using SMT. In: Bj\u00f8rner, N., Gurfinkel, A. (eds.) 2018 Formal Methods in Computer Aided Design, FMCAD 2018, Austin, TX, USA, 30 October\u20132 November 2018, pp. 1\u20139. IEEE (2018)","DOI":"10.23919\/FMCAD.2018.8602994"},{"key":"13_CR8","unstructured":"Ball, T., Daniel, J.: Deconstructing dynamic symbolic execution. In: Irlbeck, M., Peled, D.A., Pretschner, A. (eds.) Dependable Software Systems Engineering, volume 40 of NATO Science for Peace and Security Series, D: Information and Communication Security, pp. 26\u201341. IOS Press (2015)"},{"key":"13_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/978-3-642-22110-1_14","volume-title":"Computer Aided Verification","author":"C Barrett","year":"2011","unstructured":"Barrett, C., et al.: CVC4. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 171\u2013177. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_14"},{"key":"13_CR10","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"512","DOI":"10.1007\/11916277_35","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"C Barrett","year":"2006","unstructured":"Barrett, C., Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Splitting on demand in SAT modulo theories. In: Hermann, M., Voronkov, A. (eds.) LPAR 2006. LNCS (LNAI), vol. 4246, pp. 512\u2013526. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11916277_35"},{"key":"13_CR11","doi-asserted-by":"crossref","unstructured":"Berzish, M., Ganesh, V., Zheng, Y.: Z3str3: a string solver with theory-aware heuristics. In: Stewart, D., Weissenbacher, G. (eds.) 2017 Formal Methods in Computer Aided Design, FMCAD 2017, Vienna, Austria, 2\u20136 October 2017, pp. 55\u201359. IEEE (2017)","DOI":"10.23919\/FMCAD.2017.8102241"},{"key":"13_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9","volume-title":"Computer Aided Verification","year":"2014","unstructured":"Biere, A., Bloem, R. (eds.): CAV 2014. LNCS, vol. 8559. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9"},{"key":"13_CR13","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). https:\/\/doi.org\/10.1007\/978-3-642-00768-2_27"},{"issue":"4","key":"13_CR14","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1002\/malq.19880340410","volume":"34","author":"JR B\u00fcchi","year":"1988","unstructured":"B\u00fcchi, J.R., Senger, S.: Definability in the existential theory of concatenation and undecidable extensions of this theory. Math. Log. Q. 34(4), 337\u2013342 (1988)","journal-title":"Math. Log. Q."},{"key":"13_CR15","unstructured":"Cohen, A., Vechev, M.T. (eds.): Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2017, Barcelona, Spain, 18\u201323 June 2017. ACM (2017)"},{"key":"13_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L de Moura","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"13_CR17","doi-asserted-by":"crossref","unstructured":"Enderton, H.B.: A mathematical Introduction to Logic, 2nd edn. Academic Press (2001)","DOI":"10.1016\/B978-0-08-049646-7.50005-9"},{"key":"13_CR18","unstructured":"Ganesh, V., Berzish, M.: Undecidability of a theory of strings, linear arithmetic over length, and string-number conversion. CoRR, abs\/1605.09442 (2016)"},{"key":"13_CR19","doi-asserted-by":"crossref","unstructured":"Hu, Q., D\u2019Antoni, L.: Automatic program inversion using symbolic transducers. In: Cohen and Vechev [15], pp. 376\u2013389 (2017)","DOI":"10.1145\/3140587.3062345"},{"issue":"4","key":"13_CR20","doi-asserted-by":"publisher","first-page":"25:1","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:1\u201325:28 (2012)","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"key":"13_CR21","doi-asserted-by":"crossref","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 and Bloem [12], pp. 646\u2013662 (2014)","DOI":"10.1007\/978-3-319-08867-9_43"},{"key":"13_CR22","doi-asserted-by":"crossref","unstructured":"Lin, A.W., Barcel\u00f3, P.: String solving with word equations and transducers: towards a logic for analysing mutation XSS. In: Bod\u00edk, R., Majumdar, R. (eds.) Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, 20\u201322 January 2016, pp. 123\u2013136. ACM (2016)","DOI":"10.1145\/2837614.2837641"},{"issue":"2","key":"13_CR23","first-page":"147","volume":"145","author":"GS Makanin","year":"1977","unstructured":"Makanin, G.S.: The problem of solvability of equations in a free semigroup. Matematicheskii Sbornik 145(2), 147\u2013236 (1977)","journal-title":"Matematicheskii Sbornik"},{"issue":"6","key":"13_CR24","doi-asserted-by":"publisher","first-page":"937","DOI":"10.1145\/1217856.1217859","volume":"53","author":"R Nieuwenhuis","year":"2006","unstructured":"Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Solving SAT and SAT modulo theories: from an abstract Davis-Putnam-Logemann-Loveland Procedure to DPLL(T). J. ACM 53(6), 937\u2013977 (2006)","journal-title":"J. ACM"},{"issue":"4","key":"13_CR25","doi-asserted-by":"publisher","first-page":"105","DOI":"10.2307\/2268308","volume":"11","author":"WVO Quine","year":"1946","unstructured":"Quine, W.V.O.: Concatenation as a basis for arithmetic. J. Symb. Log. 11(4), 105\u2013114 (1946)","journal-title":"J. Symb. Log."},{"key":"13_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1007\/978-3-319-63390-9_24","volume-title":"Computer Aided Verification","author":"A Reynolds","year":"2017","unstructured":"Reynolds, A., Woo, M., Barrett, C., Brumley, D., Liang, T., Tinelli, C.: Scaling up DPLL(T) string solvers using context-dependent simplification. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017. LNCS, vol. 10427, pp. 453\u2013474. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63390-9_24"},{"key":"13_CR27","doi-asserted-by":"crossref","unstructured":"Saxena, P., Akhawe, D., Hanna, S., Mao, F., McCamant, S., Song, D.: A symbolic execution framework for Javascript. In: 31st IEEE Symposium on Security and Privacy, S&P 2010, 16\u201319 May 2010, Berleley\/Oakland, California, USA, pp. 513\u2013528. IEEE Computer Society (2010)","DOI":"10.1109\/SP.2010.38"},{"key":"13_CR28","unstructured":"The Unicode Consortium. The Unicode Standard, Version 12.1.0 (2019). http:\/\/www.unicode.org\/versions\/Unicode12.1.0\/"},{"key":"13_CR29","unstructured":"Tinelli, C., Barrett, C., Fontaine, P.: Unicode Strings (2020). http:\/\/smtlib.cs.uiowa.edu\/theories-UnicodeStrings.shtml"},{"key":"13_CR30","doi-asserted-by":"crossref","unstructured":"Trinh, M., Chu, D., Jaffar, J.: S3: a symbolic string solver for vulnerability detection in web applications. In: Ahn, G., Yung, M., Li, N. (eds.) Proceedings of the 2014 ACM SIGSAC Conference on Computer and Communications Security, Scottsdale, AZ, USA, 3\u20137 November 2014, pp. 1232\u20131243. ACM (2014)","DOI":"10.1145\/2660267.2660372"},{"key":"13_CR31","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"425","DOI":"10.1007\/978-3-642-17511-4_24","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"M Veanes","year":"2010","unstructured":"Veanes, M., Tillmann, N., de Halleux, J.: Qex: symbolic SQL query explorer. In: Clarke, E.M., Voronkov, A. (eds.) LPAR 2010. LNCS (LNAI), vol. 6355, pp. 425\u2013446. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-17511-4_24"},{"key":"13_CR32","unstructured":"Wu, W.-C.: Py-Conbyte (2019). https:\/\/github.com\/spencerwuwu\/py-conbyte"},{"key":"13_CR33","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). https:\/\/doi.org\/10.1007\/978-3-642-12002-2_13"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-51074-9_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,7,2]],"date-time":"2022-07-02T21:33:21Z","timestamp":1656797601000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-51074-9_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030510732","9783030510749"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-51074-9_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"24 June 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"IJCAR","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Joint Conference on Automated Reasoning","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Paris","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2020","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"1 July 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"4 July 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"10","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"ijcar2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/ijcar2020.org\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"150","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"46","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"5","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"31% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3.03","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"7.38","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"No","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"11 system descriptions are also included. The conference was held virtually due to the COVID-19 pandemic.","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}