{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,20]],"date-time":"2026-01-20T08:43:56Z","timestamp":1768898636822,"version":"3.49.0"},"publisher-location":"New York, NY, USA","reference-count":34,"publisher":"ACM","license":[{"start":{"date-parts":[[2020,6,27]],"date-time":"2020-06-27T00:00:00Z","timestamp":1593216000000},"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,6,27]]},"DOI":"10.1145\/3377811.3380398","type":"proceedings-article","created":{"date-parts":[[2020,10,1]],"date-time":"2020-10-01T18:25:34Z","timestamp":1601576734000},"page":"1459-1470","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":22,"title":["Automatically testing string solvers"],"prefix":"10.1145","author":[{"given":"Alexandra","family":"Bugariu","sequence":"first","affiliation":[{"name":"ETH Zurich, Zurich, Switzerland"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Peter","family":"M\u00fcller","sequence":"additional","affiliation":[{"name":"ETH Zurich, Zurich, Switzerland"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2020,10]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"[n.d.]. CVC4 Documentation for the String Theory. http:\/\/cvc4.cs.stanford.edu\/wiki\/Strings."},{"key":"e_1_3_2_1_2_1","unstructured":"[n.d.]. CVC4 Regression Test Suite. https:\/\/github.com\/CVC4\/CVC4\/tree\/master\/test\/regress."},{"key":"e_1_3_2_1_3_1","unstructured":"[n.d.]. MT-ABC Tested Version. https:\/\/github.com\/vlab-cs-ucsb\/ABC\/commit\/86b00141fddd183de7b9ae5c92c240e19dda1950."},{"key":"e_1_3_2_1_4_1","unstructured":"[n.d.]. SMT-COMP. https:\/\/smt-comp.github.io."},{"key":"e_1_3_2_1_5_1","unstructured":"[n.d.]. SMT-LIB Unicode Strings Theory. http:\/\/smtlib.cs.uiowa.edu\/theories-UnicodeStrings.shtml\/."},{"key":"e_1_3_2_1_6_1","unstructured":"[n.d.]. StringFuzz Test Suite. http:\/\/stringfuzz.dmitryblotsky.com\/problems\/."},{"key":"e_1_3_2_1_7_1","unstructured":"[n.d.]. Z3 SMT Solver. https:\/\/github.com\/Z3Prover\/z3\/."},{"key":"e_1_3_2_1_8_1","unstructured":"[n.d.]. Z3 Test Suite. https:\/\/github.com\/Z3Prover\/z3\/tree\/master\/src\/test."},{"key":"e_1_3_2_1_9_1","volume-title":"Model-Based Testing for Verification Back-Ends","author":"Artho Cyrille","unstructured":"Cyrille Artho, Armin Biere, and Martina Seidl. 2013. Model-Based Testing for Verification Back-Ends. In Tests and Proofs, Margus Veanes and Luca Vigan\u00f2 (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 39--55."},{"key":"e_1_3_2_1_10_1","volume-title":"Automata-Based Model Counting for String Constraints","author":"Aydin Abdulbaki","unstructured":"Abdulbaki Aydin, Lucas Bang, and Tevfik Bultan. 2015. Automata-Based Model Counting for String Constraints. In Computer Aided Verification, Daniel Kroening and Corina S. P\u0103s\u0103reanu (Eds.). Springer International Publishing, Cham, 255--272."},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236024.3236064"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","unstructured":"Murphy Berzish Vijay Ganesh and Yunhui Zheng. 2017. Z3str3: A String Solver with Theory-aware Heuristics. In 2017 Formal Methods in Computer Aided Design (FMCAD). 55--59. 10.23919\/FMCAD.2017.8102241","DOI":"10.23919\/FMCAD.2017.8102241"},{"key":"e_1_3_2_1_14_1","volume-title":"Handbook of Satisfiability","author":"Biere Armin","unstructured":"Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh. 2009. Handbook of Satisfiability: Volume 185 Frontiers in Artificial Intelligence and Applications. IOS Press, Amsterdam, The Netherlands, The Netherlands."},{"key":"e_1_3_2_1_15_1","volume-title":"An SMT-LIB Format for Sequences and Regular Expressions. Strings (01","author":"Bj\u00f8rner Nikolaj","year":"2012","unstructured":"Nikolaj Bj\u00f8rner, Vijay Ganesh, Rapha\u00ebl Michel, and Margus Veanes. 2012. An SMT-LIB Format for Sequences and Regular Expressions. Strings (01 2012)."},{"key":"e_1_3_2_1_16_1","volume-title":"StringFuzz: A Fuzzer for String Solvers","author":"Blotsky Dmitry","unstructured":"Dmitry Blotsky, Federico Mora, Murphy Berzish, Yunhui Zheng, Ifaz Kabir, and Vijay Ganesh. 2018. StringFuzz: A Fuzzer for String Solvers. In Computer Aided Verification, Hana Chockler and Georg Weissenbacher (Eds.). Springer International Publishing, Cham, 45--51."},{"key":"e_1_3_2_1_17_1","volume-title":"Fast LCF-Style Proof Reconstruction for Z3","author":"B\u00f6hme Sascha","unstructured":"Sascha B\u00f6hme and Tjark Weber. 2010. Fast LCF-Style Proof Reconstruction for Z3. In Interactive Theorem Proving, Matt Kaufmann and Lawrence C. Paulson (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 179--194."},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/1670412.1670413"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14186-7_6"},{"key":"e_1_3_2_1_20_1","volume-title":"Automated Deduction - CADE-21","author":"de Moura Leonardo","unstructured":"Leonardo de Moura and Nikolaj Bj\u00f8rner. 2007. Efficient E-Matching for SMT Solvers. In Automated Deduction - CADE-21, Frank Pfenning (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 183--198."},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/1066100.1066102"},{"key":"e_1_3_2_1_22_1","volume-title":"Programming Languages and Systems (ESOP) (Lecture Notes in Computer Science)","author":"Filli\u00e2tre Jean-Christophe","unstructured":"Jean-Christophe Filli\u00e2tre and Andrei Paskevich. 2013. Why3---Where Programs Meet Provers. In Programming Languages and Systems (ESOP) (Lecture Notes in Computer Science), Matthias Felleisen and Philippa Gardner (Eds.), Vol. 7792. Springer, 125--128."},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.5555\/648238.751562"},{"key":"e_1_3_2_1_24_1","volume-title":"In Proceedings of TPHOLs.","author":"Lescuyer St\u00e9phane","year":"2008","unstructured":"St\u00e9phane Lescuyer and Sylvain Conchon. 2008. A Reflexive Formalization of a SAT Solver in Coq. In In Proceedings of TPHOLs."},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-016-0247-6"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/2594291.2594331"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2010.09.014"},{"key":"e_1_3_2_1_28_1","first-page":"100","article-title":"Differential Testing for Software","volume":"10","author":"McKeeman William M.","year":"1998","unstructured":"William M. McKeeman. 1998. Differential Testing for Software. DIGITAL TECHNICAL JOURNAL 10, 1 (1998), 100--107.","journal-title":"DIGITAL TECHNICAL JOURNAL"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1109\/SCAM.2016.25"},{"key":"e_1_3_2_1_30_1","volume-title":"Proceedings of the 15th International Workshop on Satisfiability Modulo Theories, SMT 2017), affiliated with the 29th International Conference on Computer Aided Verification, CAV 2017","author":"Niemetz Aina","year":"2017","unstructured":"Aina Niemetz, Mathias Preiner, and Armin Biere. 2017. Model-Based API Testing for SMT Solvers. In Proceedings of the 15th International Workshop on Satisfiability Modulo Theories, SMT 2017), affiliated with the 29th International Conference on Computer Aided Verification, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Martin Brain and Liana Hadarean (Eds.). 10 pages."},{"key":"e_1_3_2_1_31_1","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Reynolds Andrew","unstructured":"Andrew Reynolds, Haniel Barbosa, and Pascal Fontaine. 2018. Revisiting Enumerative Instantiation. In Tools and Algorithms for the Construction and Analysis of Systems, Dirk Beyer and Marieke Huisman (Eds.). Springer International Publishing, Cham, 112--131."},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-012-0163-3"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.988498"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1109\/DATE.2003.1253717"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491411.2491456"}],"event":{"name":"ICSE '20: 42nd International Conference on Software Engineering","location":"Seoul South Korea","acronym":"ICSE '20","sponsor":["SIGSOFT ACM Special Interest Group on Software Engineering","KIISE Korean Institute of Information Scientists and Engineers","IEEE CS"]},"container-title":["Proceedings of the ACM\/IEEE 42nd International Conference on Software Engineering"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3377811.3380398","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3377811.3380398","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T22:41:39Z","timestamp":1750200099000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3377811.3380398"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,6,27]]},"references-count":34,"alternative-id":["10.1145\/3377811.3380398","10.1145\/3377811"],"URL":"https:\/\/doi.org\/10.1145\/3377811.3380398","relation":{},"subject":[],"published":{"date-parts":[[2020,6,27]]},"assertion":[{"value":"2020-10-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}