{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,2]],"date-time":"2026-10-02T07:58:19Z","timestamp":1790927899105,"version":"4.1.0"},"publisher-location":"New York, NY, USA","reference-count":56,"publisher":"ACM","funder":[{"name":"National Natural Science Foundation of China","award":["624B2067"],"award-info":[{"award-number":["624B2067"]}]},{"name":"National Natural Science Foundation of China","award":["62572226"],"award-info":[{"award-number":["62572226"]}]},{"name":"Jiangsu Natural Science Foundation","award":["BK20231402"],"award-info":[{"award-number":["BK20231402"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2026,3,22]]},"DOI":"10.1145\/3779212.3790195","type":"proceedings-article","created":{"date-parts":[[2026,3,10]],"date-time":"2026-03-10T13:55:26Z","timestamp":1773150926000},"page":"1316-1332","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Once4All: Skeleton-Guided SMT Solver Fuzzing with LLM-Synthesized Generators"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-5617-2205","authenticated-orcid":false,"given":"Maolin","family":"Sun","sequence":"first","affiliation":[{"name":"State Key Laboratory for Novel Software Technology, Nanjing University, Nanjing, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1153-2013","authenticated-orcid":false,"given":"Yibiao","family":"Yang","sequence":"additional","affiliation":[{"name":"State Key Laboratory for Novel Software Technology, Nanjing University, Nanjing, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4645-2526","authenticated-orcid":false,"given":"Yuming","family":"Zhou","sequence":"additional","affiliation":[{"name":"State Key Laboratory for Novel Software Technology, Nanjing University, Nanjing, China"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2026,3,22]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"Anthropic. 2025. Introducing Claude Sonnet 4.5. https:\/\/www.anthropic.com\/news\/claude-sonnet-4-5 Accessed: 2025-12-23."},{"key":"e_1_3_2_1_2_1","unstructured":"Clark Barrett Pascal Fontaine and Cesare Tinelli. 2022. The satisfiability modulo theories library (SMT-LIB). Retrieved 2022-08-18 from http:\/\/smtlib.cs.uiowa.edu\/"},{"key":"e_1_3_2_1_3_1","unstructured":"Clark Barrett Pascal Fontaine and Cesare Tinelli. 2025. The SMT-LIB Standard: Version 2.7. Technical Report. Department of Computer Science The University of Iowa. Available at www.SMT-LIB.org."},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10575-8_11"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/1670412.1670413"},{"key":"e_1_3_2_1_6_1","first-page":"209","volume-title":"OSDI","volume":"8","author":"Cadar Cristian","year":"2008","unstructured":"Cristian Cadar, Daniel Dunbar, Dawson R Engler, et al., 2008. Klee: unassisted and automatic generation of high-coverage tests for complex systems programs.. In OSDI, Vol. 8. 209-224."},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/2884781.2884878"},{"key":"e_1_3_2_1_8_1","unstructured":"The International SMT Competition. 2020. SMT-COMP. Retrieved 2020-05-15 from https:\/\/smt-comp.github.io\/2019\/index.html"},{"key":"e_1_3_2_1_9_1","unstructured":"cvc5. 2022. cvc5 fuzzing guidelines. Retrieved 2022-08-18 from https:\/\/github.com\/cvc5\/cvc5\/wiki\/Fuzzing-cvc5 Retrieved 2022-08-18"},{"key":"e_1_3_2_1_10_1","unstructured":"cvc5. 2025. Non-standard or extended theories in cvc5. https:\/\/cvc5.github.io\/docs-ci\/docs-main\/theories\/theories.html#non-standard-or-extended-theories Retrieved 2024-12-1"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792734.1792766"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.48550\/arXiv.2212.14834"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.48550\/arXiv.2304.02014"},{"key":"e_1_3_2_1_14_1","volume-title":"NetComplete: Practical Network-Wide Configuration Synthesis with Autocompletion. In 15th USENIX Symposium on Networked Systems Design and Implementation, NSDI 2018","author":"El-Hassany Ahmed","year":"2018","unstructured":"Ahmed El-Hassany, Petar Tsankov, Laurent Vanbever, and Martin T. Vechev. 2018. NetComplete: Practical Network-Wide Configuration Synthesis with Autocompletion. In 15th USENIX Symposium on Networked Systems Design and Implementation, NSDI 2018, Renton, WA, USA, April 9-11, 2018, Sujata Banerjee and Srinivasan Seshan (Eds.). USENIX Association, 579-594. https:\/\/www.usenix.org\/conference\/nsdi18\/presentation\/el-hassany"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3620666.3651365"},{"key":"e_1_3_2_1_16_1","first-page":"99","volume-title":"14th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2020","author":"Hance Travis","year":"2020","unstructured":"Travis Hance, Andrea Lattuada, Chris Hawblitzel, Jon Howell, Rob Johnson, and Bryan Parno. 2020. Storage Systems are Distributed Systems (So Verify Them That Way!). In 14th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2020, Virtual Event, November 4-6, 2020. USENIX Association, 99-115. https:\/\/www.usenix.org\/conference\/osdi20\/presentation\/hance"},{"key":"e_1_3_2_1_17_1","first-page":"165","volume-title":"11th USENIX Symposium on Operating Systems Design and Implementation, OSDI '14","author":"Hawblitzel Chris","year":"2014","unstructured":"Chris Hawblitzel, Jon Howell, Jacob R. Lorch, Arjun Narayan, Bryan Parno, Danfeng Zhang, and Brian Zill. 2014. Ironclad Apps: End-to-End Security via Automated Full-System Verification. In 11th USENIX Symposium on Operating Systems Design and Implementation, OSDI '14, Broomfield, CO, USA, October 6-8, 2014, Jason Flinn and Hank Levy (Eds.). USENIX Association, 165-181. https:\/\/www.usenix.org\/conference\/osdi14\/technical-sessions\/presentation\/hawblitzel"},{"key":"e_1_3_2_1_18_1","unstructured":"Heqing Huang. 2023. CVE-2020-19725. https:\/\/nvd.nist.gov\/vuln\/detail\/CVE-2020-19725# Retrieved 2023-11-5#"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341301.3359630"},{"key":"e_1_3_2_1_20_1","volume-title":"SCALE: Automatically Finding RFC Compliance Bugs in DNS Nameservers. In 19th USENIX Symposium on Networked Systems Design and Implementation, NSDI 2022","author":"Reddy Kakarla Siva Kesava","year":"2022","unstructured":"Siva Kesava Reddy Kakarla, Ryan Beckett, Todd D. Millstein, and George Varghese. 2022. SCALE: Automatically Finding RFC Compliance Bugs in DNS Nameservers. In 19th USENIX Symposium on Networked Systems Design and Implementation, NSDI 2022, Renton, WA, USA, April 4-6, 2022, Amar Phanishayee and Vyas Sekar (Eds.). USENIX Association, 307-323. https:\/\/www.usenix.org\/conference\/nsdi22\/presentation\/kakarla"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25540-4_12"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE48619.2023.00187"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81688-9_11"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3600006.3613140"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3656386"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535857"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3575693.3575707"},{"key":"e_1_3_2_1_28_1","first-page":"499","volume-title":"Checking Beliefs in Dynamic Networks. In 12th USENIX Symposium on Networked Systems Design and Implementation, NSDI 15","author":"Lopes Nuno P.","year":"2015","unstructured":"Nuno P. Lopes, Nikolaj S. Bj\u00f8rner, Patrice Godefroid, Karthick Jayaraman, and George Varghese. 2015. Checking Beliefs in Dynamic Networks. In 12th USENIX Symposium on Networked Systems Design and Implementation, NSDI 15, Oakland, CA, USA, May 4-6, 2015. USENIX Association, 499-512. https:\/\/www.usenix.org\/conference\/nsdi15\/technical-sessions\/presentation\/lopes"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3368089.3409763"},{"key":"e_1_3_2_1_30_1","unstructured":"MicroSoft. 2025. Z3 Guide. https:\/\/microsoft.github.io\/z3guide\/ Retrieved 2024-12-1 from"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3132747.3132748"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-13188-2_5"},{"key":"e_1_3_2_1_33_1","unstructured":"OpenAI. 2023. GPT-4 Technical Report. CoRR Vol. abs\/2303.08774 (2023). arXiv:2303.08774 doi:10.48550\/ARXIV.2303.08774"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3622781.3674171"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3485529"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/2254064.2254104"},{"key":"e_1_3_2_1_37_1","volume-title":"MESSI: Behavioral Testing of BGP Implementations. In 21st USENIX Symposium on Networked Systems Design and Implementation, NSDI 2024","author":"Singha Rathin","year":"2024","unstructured":"Rathin Singha, Rajdeep Mondal, Ryan Beckett, Siva Kesava Reddy Kakarla, Todd D. Millstein, and George Varghese. 2024. MESSI: Behavioral Testing of BGP Implementations. In 21st USENIX Symposium on Networked Systems Design and Implementation, NSDI 2024, Santa Clara, CA, April 15-17, 2024, Laurent Vanbever and Irene Zhang (Eds.). USENIX Association. https:\/\/www.usenix.org\/conference\/nsdi24\/presentation\/singha"},{"key":"e_1_3_2_1_38_1","unstructured":"SMT-LIB Initiative. 2025. News of SMT-LIB. https:\/\/smt-lib.org\/news.shtml"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASE56229.2023.00180"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE48619.2023.00018"},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/3452296.3472925"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.48550\/ARXIV.2507.06261"},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","unstructured":"Hugo Touvron Louis Martin Kevin Stone Peter Albert Amjad Almahairi Yasmine Babaei Nikolay Bashlykov Soumya Batra Prajjwal Bhargava Shruti Bhosale Dan Bikel Lukas Blecher Cristian Canton-Ferrer Moya Chen Guillem Cucurull David Esiobu Jude Fernandes Jeremy Fu Wenyin Fu Brian Fuller Cynthia Gao Vedanuj Goswami Naman Goyal Anthony Hartshorn Saghar Hosseini Rui Hou Hakan Inan Marcin Kardas Viktor Kerkez Madian Khabsa Isabel Kloumann Artem Korenev Punit Singh Koura Marie-Anne Lachaux Thibaut Lavril Jenya Lee Diana Liskovich Yinghai Lu Yuning Mao Xavier Martinet Todor Mihaylov Pushkar Mishra Igor Molybog Yixin Nie Andrew Poulton Jeremy Reizenstein Rashi Rungta Kalyan Saladi Alan Schelten Ruan Silva Eric Michael Smith Ranjan Subramanian Xiaoqing Ellen Tan Binh Tang Ross Taylor Adina Williams Jian Xiang Kuan Puxin Xu Zheng Yan Iliyan Zarov Yuchen Zhang Angela Fan Melanie Kambadur Sharan Narang Aur\u00e9lien Rodriguez Robert Stojnic Sergey Edunov and Thomas Scialom. 2023. Llama 2: Open Foundation and Fine-Tuned Chat Models. CoRR Vol. abs\/2307.09288 (2023). arXiv:2307.09288 doi:10.48550\/arXiv.2307.09288","DOI":"10.48550\/arXiv.2307.09288"},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.48550\/ARXIV.2507.19275"},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/3510003.3510062"},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASE56229.2023.00120"},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.14722\/ndss.2020.24422"},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/3689795"},{"key":"e_1_3_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428261"},{"key":"e_1_3_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3385985"},{"key":"e_1_3_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/3597503.3639121"},{"key":"e_1_3_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/3647994"},{"key":"e_1_3_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/3468264.3468540"},{"key":"e_1_3_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454054"},{"key":"e_1_3_2_1_55_1","volume-title":"Low-Cost and Comprehensive Non-textual Input Fuzzing with LLM-Synthesized Input Generators. In 34th USENIX Security Symposium, USENIX Security 2025","author":"Zhang Kunpeng","year":"2025","unstructured":"Kunpeng Zhang, Zongjie Li, Daoyuan Wu, Shuai Wang, and Xin Xia. 2025. Low-Cost and Comprehensive Non-textual Input Fuzzing with LLM-Synthesized Input Generators. In 34th USENIX Security Symposium, USENIX Security 2025, Seattle, WA, USA, August 13-15, 2025, Lujo Bauer and Giancarlo Pellegrino (Eds.). USENIX Association, 6999-7018. https:\/\/www.usenix.org\/conference\/usenixsecurity25\/presentation\/zhang-kunpeng"},{"key":"e_1_3_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062379"}],"event":{"name":"ASPLOS '26: 31st ACM International Conference on Architectural Support for Programming Languages and Operating Systems","location":"Pittsburgh PA USA","sponsor":["SIGOPS ACM Special Interest Group on Operating Systems","SIGPLAN ACM Special Interest Group on Programming Languages","SIGARCH ACM Special Interest Group on Computer Architecture","SIGBED ACM Special Interest Group on Embedded Systems"]},"container-title":["Proceedings of the 31st ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 2"],"original-title":[],"deposited":{"date-parts":[[2026,3,15]],"date-time":"2026-03-15T13:59:20Z","timestamp":1773583160000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3779212.3790195"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,3,22]]},"references-count":56,"alternative-id":["10.1145\/3779212.3790195","10.1145\/3779212"],"URL":"https:\/\/doi.org\/10.1145\/3779212.3790195","relation":{},"subject":[],"published":{"date-parts":[[2026,3,22]]},"assertion":[{"value":"2026-03-22","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}