{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,12]],"date-time":"2026-09-12T01:59:37Z","timestamp":1789178377306,"version":"build-2803163510"},"publisher-location":"New York, NY, USA","reference-count":67,"publisher":"ACM","license":[{"start":{"date-parts":[[2021,7,11]],"date-time":"2021-07-11T00:00:00Z","timestamp":1625961600000},"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":[[2021,7,11]]},"DOI":"10.1145\/3460319.3464803","type":"proceedings-article","created":{"date-parts":[[2021,7,8]],"date-time":"2021-07-08T22:18:43Z","timestamp":1625782723000},"page":"322-335","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":20,"title":["Fuzzing SMT solvers via two-dimensional input space exploration"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-0342-9518","authenticated-orcid":false,"given":"Peisen","family":"Yao","sequence":"first","affiliation":[{"name":"Hong Kong University of Science and Technology, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Heqing","family":"Huang","sequence":"additional","affiliation":[{"name":"Hong Kong University of Science and Technology, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Wensheng","family":"Tang","sequence":"additional","affiliation":[{"name":"Hong Kong University of Science and Technology, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Qingkai","family":"Shi","sequence":"additional","affiliation":[{"name":"Hong Kong University of Science and Technology, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Rongxin","family":"Wu","sequence":"additional","affiliation":[{"name":"Xiamen University, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Charles","family":"Zhang","sequence":"additional","affiliation":[{"name":"Hong Kong University of Science and Technology, China"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2021,7,11]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-04244-7_14"},{"key":"e_1_3_2_1_2_1","volume-title":"NAUTILUS: Fishing for Deep Bugs with Grammars. In 26th Annual Network and Distributed System Security Symposium, NDSS 2019","author":"Aschermann Cornelius","year":"2019","unstructured":"Cornelius Aschermann , Tommaso Frassetto , Thorsten Holz , Patrick Jauernig , Ahmad-Reza Sadeghi , and Daniel Teuchert . 2019 . NAUTILUS: Fishing for Deep Bugs with Grammars. In 26th Annual Network and Distributed System Security Symposium, NDSS 2019 , San Diego, California, USA , February 24-27, 2019. The Internet Society. https:\/\/www.ndss-symposium.org\/ndss-paper\/nautilus-fishingfor-deep-bugs-with-grammars\/ Cornelius Aschermann, Tommaso Frassetto, Thorsten Holz, Patrick Jauernig, Ahmad-Reza Sadeghi, and Daniel Teuchert. 2019. NAUTILUS: Fishing for Deep Bugs with Grammars. In 26th Annual Network and Distributed System Security Symposium, NDSS 2019, San Diego, California, USA, February 24-27, 2019. The Internet Society. https:\/\/www.ndss-symposium.org\/ndss-paper\/nautilus-fishingfor-deep-bugs-with-grammars\/"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/2568225.2568293"},{"key":"e_1_3_2_1_4_1","volume-title":"Advances in Neural Information Processing Systems 31: Annual Conference on Neural Information Processing Systems 2018","author":"Balunovic Mislav","year":"2018","unstructured":"Mislav Balunovic , Pavol Bielik , and Martin T. Vechev . 2018. Learning to Solve SMT Formulas . In Advances in Neural Information Processing Systems 31: Annual Conference on Neural Information Processing Systems 2018 , NeurIPS 2018 , December 3-8, 2018, Montr\u00e9al, Canada, Samy Bengio, Hanna M. Wallach, Hugo Larochelle, Kristen Grauman, Nicol\u00f2 Cesa-Bianchi, and Roman Garnett (Eds.). 10338-10349. https:\/\/proceedings.neurips.cc\/paper\/2018\/hash\/ 68331f0427b551b68e911eebe35233b-Abstract.html Mislav Balunovic, Pavol Bielik, and Martin T. Vechev. 2018. Learning to Solve SMT Formulas. In Advances in Neural Information Processing Systems 31: Annual Conference on Neural Information Processing Systems 2018, NeurIPS 2018, December 3-8, 2018, Montr\u00e9al, Canada, Samy Bengio, Hanna M. Wallach, Hugo Larochelle, Kristen Grauman, Nicol\u00f2 Cesa-Bianchi, and Roman Garnett (Eds.). 10338-10349. https:\/\/proceedings.neurips.cc\/paper\/2018\/hash\/ 68331f0427b551b68e911eebe35233b-Abstract.html"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3368089.3409744"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.5555\/2032305.2032319"},{"key":"e_1_3_2_1_7_1","unstructured":"Clark Barrett Aaron Stump and Cesare Tinelli. 2010. The satisfiability modulo theories library (SMT-LIB). www. SMT-LIB. org 15 ( 2010 ) 18-52.  Clark Barrett Aaron Stump and Cesare Tinelli. 2010. The satisfiability modulo theories library (SMT-LIB). www. SMT-LIB. org 15 ( 2010 ) 18-52."},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.23919\/FMCAD.2017.8102241"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.SNAPL.2017.1"},{"key":"e_1_3_2_1_10_1","unstructured":"Nikolaj Bj\u00f8rner Vijay Ganesh Rapha\u00ebl Michel and Margus Veanes. 2012. An SMT-LIB format for sequences and regular expressions. SMT 12 ( 2012 ) 76-86.  Nikolaj Bj\u00f8rner Vijay Ganesh Rapha\u00ebl Michel and Margus Veanes. 2012. An SMT-LIB format for sequences and regular expressions. SMT 12 ( 2012 ) 76-86."},{"key":"e_1_3_2_1_11_1","volume-title":"Syntia: Synthesizing the Semantics of Obfuscated Code. In 26th USENIX Security Symposium, USENIX Security 2017","author":"Blazytko Tim","year":"2017","unstructured":"Tim Blazytko , Moritz Contag , Cornelius Aschermann , and Thorsten Holz . 2017 . Syntia: Synthesizing the Semantics of Obfuscated Code. In 26th USENIX Security Symposium, USENIX Security 2017 , Vancouver, BC, Canada , August 16-18, 2017, Engin Kirda and Thomas Ristenpart (Eds.). USENIX Association, 643-659. https:\/\/www.usenix.org\/conference\/usenixsecurity17\/technical-sessions\/ presentation\/blazytko Tim Blazytko, Moritz Contag, Cornelius Aschermann, and Thorsten Holz. 2017. Syntia: Synthesizing the Semantics of Obfuscated Code. In 26th USENIX Security Symposium, USENIX Security 2017, Vancouver, BC, Canada, August 16-18, 2017, Engin Kirda and Thomas Ristenpart (Eds.). USENIX Association, 643-659. https:\/\/www.usenix.org\/conference\/usenixsecurity17\/technical-sessions\/ presentation\/blazytko"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-96142-2_6"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3368089.3409728"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/1670412.1670413"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-12002-2_12"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3377811.3380398"},{"key":"e_1_3_2_1_17_1","first-page":"209","volume-title":"Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation","author":"Cadar Cristian","year":"2008","unstructured":"Cristian Cadar , Daniel Dunbar , Dawson R Engler , 2008 . KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs .. In Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation ( San Diego, California) ( OSDI'08). USENIX Association, Berkeley, CA, USA , 209 - 224 . http:\/\/dl.acm.org\/citation.cfm?id= 1855741. 1855756 Cristian Cadar, Daniel Dunbar, Dawson R Engler, et al. 2008. KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs.. In Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation (San Diego, California) ( OSDI'08). USENIX Association, Berkeley, CA, USA, 209-224. http:\/\/dl.acm.org\/citation.cfm?id= 1855741. 1855756"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2019.00037"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31759-0_19"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/1147249.1147257"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-96145-3_3"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"crossref","unstructured":"Leonardo de Moura and Grant Olney Passmore. 2013. The Strategy Challenge in SMT Solving. ( 2013 ) 15-44.  Leonardo de Moura and Grant Olney Passmore. 2013. The Strategy Challenge in SMT Solving. ( 2013 ) 15-44.","DOI":"10.1007\/978-3-642-36675-8_2"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1504\/IJAISC.2014.059280"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_49"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/11817963_11"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-59762-7_8"},{"key":"e_1_3_2_1_28_1","unstructured":"M Eddington. 2008. Peach fuzzer. URl: http:\/\/www. peachfuzzer. com\/(visited on 06\/21\/ 2017 ) ( 2008 ).  M Eddington. 2008. Peach fuzzer. URl: http:\/\/www. peachfuzzer. com\/(visited on 06\/21\/ 2017 ) ( 2008 )."},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54862-8_5"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73368-3_52"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/1065010.1065036"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/2090147.2094081"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/2338965.2336763"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-41707-8_2"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_45"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10664-018-9635-4"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.14722\/ndss.2019.23263"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/1101908.1101926"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-25566-3_40"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1613\/jair.2861"},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2019.00112"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/3243734.3243804"},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/11754008_2"},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSM.2013.58"},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1109\/DATE.2003.10018"},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/3368089.3409763"},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1109\/52.56422"},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/1883612.1883618"},{"key":"e_1_3_2_1_49_1","volume-title":"Proceedings of the 11th International Workshop on Satisfiability Modulo Theories (SMT'13)","volume":"13","author":"Niemetz Aina","year":"2013","unstructured":"Aina Niemetz and Armin Biere . 2013 . ddSMT: a delta debugger for the SMTLIB v2 format . In Proceedings of the 11th International Workshop on Satisfiability Modulo Theories (SMT'13) , afiliated to SAT, Vol. 13 . 36-45. https:\/\/doi.org\/doi= 10.1.1.380.134 Aina Niemetz and Armin Biere. 2013. ddSMT: a delta debugger for the SMTLIB v2 format. In Proceedings of the 11th International Workshop on Satisfiability Modulo Theories (SMT'13), afiliated to SAT, Vol. 13. 36-45. https:\/\/doi.org\/doi= 10.1.1.380.134"},{"key":"e_1_3_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.3233\/sat190101"},{"key":"e_1_3_2_1_51_1","volume-title":"Proceedings of the 15th International Workshop on Satisfiability Modulo Theories, SMT.","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. 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."},{"key":"e_1_3_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-24258-9_20"},{"key":"e_1_3_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/3106237.3106273"},{"key":"e_1_3_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/3293882.3330576"},{"key":"e_1_3_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41540-6_2"},{"key":"e_1_3_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICST.2019.00032"},{"key":"e_1_3_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54577-5_15"},{"key":"e_1_3_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01932308"},{"key":"e_1_3_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-63618-0_5"},{"key":"e_1_3_2_1_60_1","first-page":"309","volume-title":"AddressSanitizer: A Fast Address Sanity Checker. In 2012 USENIX Annual Technical Conference","author":"Serebryany Konstantin","year":"2012","unstructured":"Konstantin Serebryany , Derek Bruening , Alexander Potapenko , and Dmitriy Vyukov . 2012 . AddressSanitizer: A Fast Address Sanity Checker. In 2012 USENIX Annual Technical Conference , Boston, MA, USA , June 13-15, 2012, Gernot Heiser and Wilson C. Hsieh (Eds.). USENIX Association, 309 - 318 . https:\/\/www.usenix. org\/conference\/atc12\/technical-sessions\/presentation\/serebryany Konstantin Serebryany, Derek Bruening, Alexander Potapenko, and Dmitriy Vyukov. 2012. AddressSanitizer: A Fast Address Sanity Checker. In 2012 USENIX Annual Technical Conference, Boston, MA, USA, June 13-15, 2012, Gernot Heiser and Wilson C. Hsieh (Eds.). USENIX Association, 309-318. https:\/\/www.usenix. org\/conference\/atc12\/technical-sessions\/presentation\/serebryany"},{"key":"e_1_3_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD.1996.569607"},{"key":"e_1_3_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.1145\/331960.331965"},{"key":"e_1_3_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2020.3013716"},{"key":"e_1_3_2_1_64_1","doi-asserted-by":"publisher","DOI":"10.1145\/2580950"},{"key":"e_1_3_2_1_65_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428261"},{"key":"e_1_3_2_1_66_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3385985"},{"key":"e_1_3_2_1_67_1","doi-asserted-by":"publisher","DOI":"10.1145\/2970276.2970335"}],"event":{"name":"ISSTA '21: 30th ACM SIGSOFT International Symposium on Software Testing and Analysis","location":"Virtual Denmark","acronym":"ISSTA '21","sponsor":["SIGSOFT ACM Special Interest Group on Software Engineering"]},"container-title":["Proceedings of the 30th ACM SIGSOFT International Symposium on Software Testing and Analysis"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3460319.3464803","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3460319.3464803","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T20:48:31Z","timestamp":1750193311000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3460319.3464803"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,7,11]]},"references-count":67,"alternative-id":["10.1145\/3460319.3464803","10.1145\/3460319"],"URL":"https:\/\/doi.org\/10.1145\/3460319.3464803","relation":{},"subject":[],"published":{"date-parts":[[2021,7,11]]},"assertion":[{"value":"2021-07-11","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}