{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,13]],"date-time":"2026-02-13T23:10:31Z","timestamp":1771024231887,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":24,"publisher":"ACM","license":[{"start":{"date-parts":[[2020,10,7]],"date-time":"2020-10-07T00:00:00Z","timestamp":1602028800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2020,10,7]]},"DOI":"10.1145\/3387903.3389317","type":"proceedings-article","created":{"date-parts":[[2020,9,12]],"date-time":"2020-09-12T20:02:18Z","timestamp":1599940938000},"page":"85-88","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":10,"title":["The Power of String Solving"],"prefix":"10.1145","author":[{"given":"Mitja","family":"Kulczynski","sequence":"first","affiliation":[{"name":"Department of Computer Science, Kiel University, Kiel, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Florin","family":"Manea","sequence":"additional","affiliation":[{"name":"Department of Computer Science, University of G\u00f6ttingen, G\u00f6ttingen, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Dirk","family":"Nowotka","sequence":"additional","affiliation":[{"name":"Department of Computer Science, Kiel University, Kiel, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Danny B\u00f8gsted","family":"Poulsen","sequence":"additional","affiliation":[{"name":"Department of Computer Science, Aalborg University Aalborg, Denmark"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2020,10,7]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"[n.d.]. IBM AppScan Source web site. https:\/\/www.ibm.com\/dk-da\/security\/application-security\/appscan.  [n.d.]. IBM AppScan Source web site. https:\/\/www.ibm.com\/dk-da\/security\/application-security\/appscan."},{"key":"e_1_3_2_1_2_1","volume-title":"Trau: SMT solver for string constraints. In Proc","author":"Abdulla P. A.","year":"2018","unstructured":"P. A. Abdulla , M. F.i Atig , Y. Chen , B. P. Diep , L. Hol\u00edk , A. Rezine , and P. R\u00fcmmer . 2018 . Trau: SMT solver for string constraints. In Proc . FMCAD. IEEE , 1--5. P. A. Abdulla, M. F.i Atig, Y. Chen, B. P. Diep, L. Hol\u00edk, A. Rezine, and P. R\u00fcmmer. 2018. Trau: SMT solver for string constraints. In Proc. FMCAD. IEEE, 1--5."},{"key":"e_1_3_2_1_3_1","volume-title":"Proc. CAV. Springer, 150--166","author":"Abdulla P. A.","unstructured":"P. A. Abdulla , M. F. Atig , Y. Chen , L. Hol\u00edk , A. Rezine , P. R\u00fcmmer , and J. Stenman . 2014. String constraints for verification . In Proc. CAV. Springer, 150--166 . P. A. Abdulla, M. F. Atig, Y. Chen, L. Hol\u00edk, A. Rezine, P. R\u00fcmmer, and J. Stenman. 2014. String constraints for verification. In Proc. CAV. Springer, 150--166."},{"key":"e_1_3_2_1_4_1","volume-title":"Proc. CAV, Part 1 (LNCS)","volume":"9206","author":"Abdulla P. A.","unstructured":"P. A. Abdulla , M. F. Atig , Y. Chen , L. Hol\u00edk , A. Rezine , P. R\u00fcmmer , and J. Stenman . 2015. Norn: An SMT Solver for String Constraints . In Proc. CAV, Part 1 (LNCS) , Vol. 9206 . 462--469. P. A. Abdulla, M. F. Atig, Y. Chen, L. Hol\u00edk, A. Rezine, P. R\u00fcmmer, and J. Stenman. 2015. Norn: An SMT Solver for String Constraints. In Proc. CAV, Part 1 (LNCS), Vol. 9206. 462--469."},{"key":"e_1_3_2_1_5_1","volume-title":"Proc. Marktoberdorf Summer School on Dependable Software Systems Engineering","author":"Ball T.","year":"2014","unstructured":"T. Ball and J. Daniel . 2014. Deconstructing Dynamic Symbolic Execution . Proc. Marktoberdorf Summer School on Dependable Software Systems Engineering ( 2014 ). T. Ball and J. Daniel. 2014. Deconstructing Dynamic Symbolic Execution. Proc. Marktoberdorf Summer School on Dependable Software Systems Engineering (2014)."},{"key":"e_1_3_2_1_6_1","first-page":"171","article-title":"CVC4","volume":"6806","author":"Barrett C. W.","year":"2011","unstructured":"C. W. Barrett , C. L. Conway , M. Deters , L. Hadarean , D. Jovanovic , T. King , A. Reynolds , and C. Tinelli . 2011 . CVC4 . In Proc. CAV (LNCS) , Vol. 6806. 171 -- 177 . C. W. Barrett, C. L. Conway, M. Deters, L. Hadarean, D. Jovanovic, T. King, A. Reynolds, and C. Tinelli. 2011. CVC4. In Proc. CAV (LNCS), Vol. 6806. 171--177.","journal-title":"Proc. CAV (LNCS)"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.23919\/FMCAD.2017.8102241"},{"key":"e_1_3_2_1_8_1","volume-title":"Stringfuzz: A fuzzer for string solvers. In Proc","author":"Blotsky D.","year":"2018","unstructured":"D. Blotsky , F. Mora , M. Berzish , Y. Zheng , I. Kabir , and V. Ganesh . 2018 . Stringfuzz: A fuzzer for string solvers. In Proc . CAV. Springer , 45--51. D. Blotsky, F. Mora, M. Berzish, Y. Zheng, I. Kabir, and V. Ganesh. 2018. Stringfuzz: A fuzzer for string solvers. In Proc. CAV. Springer, 45--51."},{"key":"e_1_3_2_1_9_1","volume-title":"Proc. 11th Joint Meeting on Foundations of Software Engineering. ACM, 535--546","author":"Brennan T.","unstructured":"T. Brennan , N. Tsiskaridze , N. Rosner , A.i Aydin, and T. Bultan . 2017. Constraint normalization and parameterized caching for quantitative program analysis . In Proc. 11th Joint Meeting on Foundations of Software Engineering. ACM, 535--546 . T. Brennan, N. Tsiskaridze, N. Rosner, A.i Aydin, and T. Bultan. 2017. Constraint normalization and parameterized caching for quantitative program analysis. In Proc. 11th Joint Meeting on Foundations of Software Engineering. ACM, 535--546."},{"key":"e_1_3_2_1_10_1","volume-title":"On Solving Word Equations Using SAT. In Proc. RP (LNCS)","volume":"11674","author":"Day J. D.","unstructured":"J. D. Day , T. Ehlers , M. Kulczynski , F. Manea , D. Nowotka , and D. B. Poulsen . 2019 . On Solving Word Equations Using SAT. In Proc. RP (LNCS) , Vol. 11674 . Springer, 93--106. J. D. Day, T. Ehlers, M. Kulczynski, F. Manea, D. Nowotka, and D. B. Poulsen. 2019. On Solving Word Equations Using SAT. In Proc. RP (LNCS), Vol. 11674. Springer, 93--106."},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3372020.3391556"},{"key":"e_1_3_2_1_12_1","first-page":"15","article-title":"The Satisfiability of Word Equations: Decidable and Undecidable Theories","volume":"11123","author":"Day J. D.","year":"2018","unstructured":"J. D. Day , V. Ganesh , P. He , F. Manea , and D. Nowotka . 2018 . The Satisfiability of Word Equations: Decidable and Undecidable Theories . In Proc. RP (LNCS) , Vol. 11123. 15 -- 29 . J. D. Day, V.Ganesh, P. He, F. Manea, and D. Nowotka. 2018. The Satisfiability of Word Equations: Decidable and Undecidable Theories. In Proc. RP (LNCS), Vol. 11123. 15--29.","journal-title":"Proc. RP (LNCS)"},{"key":"e_1_3_2_1_13_1","volume-title":"Proc. ASE - IEEE\/ACM. ACM, 259--270","author":"Kausler S.","unstructured":"S. Kausler and E. Sherman . 2014. Evaluation of string constraint solvers in the context of symbolic execution . In Proc. ASE - IEEE\/ACM. ACM, 259--270 . S. Kausler and E. Sherman. 2014. Evaluation of string constraint solvers in the context of symbolic execution. In Proc. ASE - IEEE\/ACM. ACM, 259--270."},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-016-0247-6"},{"key":"e_1_3_2_1_15_1","volume-title":"ACM SIGPLAN Notices","volume":"49","author":"Luu L.","unstructured":"L. Luu , S. Shinde , P. Saxena , and B. Demsky . 2014. A model counter for constraints over unbounded strings . In ACM SIGPLAN Notices , Vol. 49 . ACM, 565--576. L. Luu, S. Shinde, P. Saxena, and B. Demsky. 2014. A model counter for constraints over unbounded strings. In ACM SIGPLAN Notices, Vol. 49. ACM, 565--576."},{"key":"e_1_3_2_1_16_1","first-page":"129","article-title":"The problem of solvability of equations in a free semigroup. Sbornik","volume":"32","author":"Makanin G. S.","year":"1977","unstructured":"G. S. Makanin . 1977 . The problem of solvability of equations in a free semigroup. Sbornik : Mathematics 32 , 2 (1977), 129 -- 198 . G. S. Makanin. 1977. The problem of solvability of equations in a free semigroup. Sbornik: Mathematics 32, 2 (1977), 129--198.","journal-title":"Mathematics"},{"key":"e_1_3_2_1_17_1","volume-title":"Proc. CAV. Springer, 453--474","author":"Reynolds A.","unstructured":"A. Reynolds , M. Woo , C. Barrett , D. Brumley , T. Liang , and C. Tinelli . 2017. Scaling up DPLL (T) string solvers using context-dependent simplification . In Proc. CAV. Springer, 453--474 . A. Reynolds, M. Woo, C. Barrett, D. Brumley, T. Liang, and C. Tinelli. 2017. Scaling up DPLL (T) string solvers using context-dependent simplification. In Proc. CAV. Springer, 453--474."},{"key":"e_1_3_2_1_18_1","unstructured":"P. Saxena D. Akhawe S. Hanna F. Mao S. McCamant and D. Song. [n.d.]. Kaluza web site. webblaze.cs.berkeley.edu\/2010\/kaluza\/. Accessed: 2020-01-01.  P. Saxena D. Akhawe S. Hanna F. Mao S. McCamant and D. Song. [n.d.]. Kaluza web site. webblaze.cs.berkeley.edu\/2010\/kaluza\/. Accessed: 2020-01-01."},{"key":"e_1_3_2_1_19_1","volume-title":"Proc. 31st S&P. 513--528","author":"Saxena P.","unstructured":"P. Saxena , D. Akhawe , S. Hanna , F. Mao , S. McCamant , and D. Song . 2010. A Symbolic Execution Framework for JavaScript . In Proc. 31st S&P. 513--528 . P. Saxena, D. Akhawe, S. Hanna, F. Mao, S. McCamant, and D. Song. 2010. A Symbolic Execution Framework for JavaScript. In Proc. 31st S&P. 513--528."},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2522920.2522926"},{"key":"e_1_3_2_1_21_1","unstructured":"J. Thom\u00e9 L. K. Shar D. Bianculli and L. Briand. 2018. An integrated approach for effective injection vulnerability analysis of web applications through security slicing and hybrid constraint solving. IEEE TSE (2018).  J. Thom\u00e9 L. K. Shar D. Bianculli and L. Briand. 2018. An integrated approach for effective injection vulnerability analysis of web applications through security slicing and hybrid constraint solving. IEEE TSE (2018)."},{"key":"e_1_3_2_1_22_1","volume-title":"STRANGER: An Automata-based String Analysis Tool for PHP. In Proc. TACAS (Paphos, Cyprus) (TACAS'10)","author":"Yu F.","year":"2010","unstructured":"F. Yu , M. Alkhalaf , and T. Bultan . 2010 . STRANGER: An Automata-based String Analysis Tool for PHP. In Proc. TACAS (Paphos, Cyprus) (TACAS'10) . Springer , 154--157. F. Yu, M. Alkhalaf, and T. Bultan. 2010. STRANGER: An Automata-based String Analysis Tool for PHP. In Proc. TACAS (Paphos, Cyprus) (TACAS'10). Springer, 154--157."},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-016-0263-6"},{"key":"e_1_3_2_1_24_1","volume-title":"Proceedings of the 2013 9th Joint Meeting on Foundations of Software Engineering. ACM, 114--124","author":"Zheng Y.","unstructured":"Y. Zheng , X. Zhang , and V. Ganesh . 2013. Z3-str: A z3-based string solver for web application analysis . In Proceedings of the 2013 9th Joint Meeting on Foundations of Software Engineering. ACM, 114--124 . Y. Zheng, X. Zhang, and V. Ganesh. 2013. Z3-str: A z3-based string solver for web application analysis. In Proceedings of the 2013 9th Joint Meeting on Foundations of Software Engineering. ACM, 114--124."}],"event":{"name":"AST '20: IEEE\/ACM 15nd International Conference on Automation of Software Test","location":"Seoul Republic of Korea","acronym":"AST '20","sponsor":["SIGSOFT ACM Special Interest Group on Software Engineering"]},"container-title":["Proceedings of the IEEE\/ACM 1st International Conference on Automation of Software Test"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3387903.3389317","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3387903.3389317","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T22:41:37Z","timestamp":1750200097000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3387903.3389317"}},"subtitle":["Simplicity of Comparison"],"short-title":[],"issued":{"date-parts":[[2020,10,7]]},"references-count":24,"alternative-id":["10.1145\/3387903.3389317","10.1145\/3387903"],"URL":"https:\/\/doi.org\/10.1145\/3387903.3389317","relation":{},"subject":[],"published":{"date-parts":[[2020,10,7]]},"assertion":[{"value":"2020-10-07","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}