{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,8]],"date-time":"2026-10-08T11:59:08Z","timestamp":1791460748518,"version":"4.3.4"},"reference-count":61,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA2","license":[{"start":{"date-parts":[[2022,10,31]],"date-time":"2022-10-31T00:00:00Z","timestamp":1667174400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2022,10,31]]},"abstract":"<jats:p>\n            Programming languages and software engineering tools routinely encounter components that are difficult to reason on via formal techniques or whose formal semantics are not even available\u2014third-party libraries, inline assembly code, SIMD instructions, system calls, calls to machine learning models, etc. However, often access to these components is available as input-output oracles\u2014interfaces are available to query these components on certain inputs to receive the respective outputs. We refer to such functions as\n            <jats:italic>closed-box functions<\/jats:italic>\n            . Regular SMT solvers are unable to handle such closed-box functions.\n          <\/jats:p>\n          <jats:p>\n            We propose S\u0101dhak, a solver for SMT theories modulo closed-box functions. Our core idea is to use a synergistic combination of a fuzzer to reason on closed-box functions and an SMT engine to solve the constraints pertaining to the SMT theories. The fuzz and the SMT engines attempt to converge to a model by exchanging a rich set of\n            <jats:italic>interface constraints<\/jats:italic>\n            that are relevant and interpretable by them. Our implementation, S\u0101dhak, demonstrates a significant advantage over the only other solver that is capable of handling such closed-box constraints: S\u0101dhak solves 36.45% more benchmarks than the best-performing mode of this state-of-the-art solver and has 5.72x better PAR-2 score; on the benchmarks that are solved by both tools, S\u0101dhak is (on an average) 14.62x faster.\n          <\/jats:p>","DOI":"10.1145\/3563332","type":"journal-article","created":{"date-parts":[[2022,10,31]],"date-time":"2022-10-31T20:23:35Z","timestamp":1667247815000},"page":"1236-1263","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":16,"title":["Satisfiability modulo fuzzing: a synergistic combination of SMT solving and fuzzing"],"prefix":"10.1145","volume":"6","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-3506-6742","authenticated-orcid":false,"given":"Sujit Kumar","family":"Muduli","sequence":"first","affiliation":[{"name":"IIT Kanpur, India"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3394-023X","authenticated-orcid":false,"given":"Subhajit","family":"Roy","sequence":"additional","affiliation":[{"name":"IIT Kanpur, India"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2022,10,31]]},"reference":[{"key":"e_1_2_1_1_1","unstructured":"2015. SMTCOMP SMTLib2 benchmarks.. https:\/\/smtlib.cs.uiowa.edu\/benchmarks.shtml \t\t\t\t  2015. SMTCOMP SMTLib2 benchmarks.. https:\/\/smtlib.cs.uiowa.edu\/benchmarks.shtml"},{"key":"e_1_2_1_2_1","unstructured":"2019. Benchmarks for SyGuS Competition. SyGuS-Comp https:\/\/github.com\/SyGuS-Org\/benchmarks \t\t\t\t  2019. Benchmarks for SyGuS Competition. SyGuS-Comp https:\/\/github.com\/SyGuS-Org\/benchmarks"},{"key":"e_1_2_1_3_1","unstructured":"2021. ESBMC. https:\/\/github.com\/esbmc\/esbmc\/tree\/master\/regression \t\t\t\t  2021. ESBMC. https:\/\/github.com\/esbmc\/esbmc\/tree\/master\/regression"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2013.6679385"},{"key":"e_1_2_1_5_1","volume-title":"Black Box Analysis of Sanitizers and Filters. In IEEE Symposium on Security and Privacy, SP 2016","author":"Argyros George","year":"2016","unstructured":"George Argyros , Ioannis Stais , Aggelos Kiayias , and Angelos D. Keromytis . 2016. Back in Black: Towards Formal , Black Box Analysis of Sanitizers and Filters. In IEEE Symposium on Security and Privacy, SP 2016 , San Jose, CA, USA , May 22-26, 2016 . IEEE Computer Society, 91\u2013109. George Argyros, Ioannis Stais, Aggelos Kiayias, and Angelos D. Keromytis. 2016. Back in Black: Towards Formal, Black Box Analysis of Sanitizers and Filters. In IEEE Symposium on Security and Privacy, SP 2016, San Jose, CA, USA, May 22-26, 2016. IEEE Computer Society, 91\u2013109."},{"key":"e_1_2_1_6_1","volume-title":"Proceedings of SAT Competition 2017 : Solver and Benchmark Descriptions. http:\/\/hdl.handle.net\/10138\/224324","unstructured":"2017. Proceedings of SAT Competition 2017 : Solver and Benchmark Descriptions. http:\/\/hdl.handle.net\/10138\/224324 2017. Proceedings of SAT Competition 2017 : Solver and Benchmark Descriptions. http:\/\/hdl.handle.net\/10138\/224324"},{"key":"e_1_2_1_7_1","volume-title":"Proceedings of the 8th international workshop on satisfiability modulo theories","author":"Barrett Clark","year":"2010","unstructured":"Clark Barrett , Aaron Stump , and Cesare Tinelli . 2010 . The smt-lib standard: Version 2.0 . In Proceedings of the 8th international workshop on satisfiability modulo theories ( Edinburgh, England). 13, 14. Clark Barrett, Aaron Stump, and Cesare Tinelli. 2010. The smt-lib standard: Version 2.0. In Proceedings of the 8th international workshop on satisfiability modulo theories (Edinburgh, England). 13, 14."},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22110-1_14"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE43902.2021.00071"},{"key":"e_1_2_1_10_1","volume-title":"Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation (OSDI\u201908)","author":"Cadar Cristian","year":"2008","unstructured":"Cristian Cadar , Daniel Dunbar , and Dawson 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 (OSDI\u201908) . USENIX Association, USA. Cristian Cadar, Daniel Dunbar, and Dawson 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 (OSDI\u201908). USENIX Association, USA."},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21690-4_19"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-68167-2_2"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2635868.2635889"},{"key":"e_1_2_1_14_1","volume-title":"14th USENIX Workshop on Offensive Technologies (WOOT 20)","author":"Fioraldi Andrea","year":"2020","unstructured":"Andrea Fioraldi , Dominik Maier , Heiko Ei\u00df feldt, and Marc Heuse . 2020 . AFL++: Combining Incremental Steps of Fuzzing Research . In 14th USENIX Workshop on Offensive Technologies (WOOT 20) . USENIX Association. Andrea Fioraldi, Dominik Maier, Heiko Ei\u00df feldt, and Marc Heuse. 2020. AFL++: Combining Incremental Steps of Fuzzing Research. In 14th USENIX Workshop on Offensive Technologies (WOOT 20). USENIX Association."},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-27813-9_14"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-48288-9_7"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993316.1993529"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/1065010.1065036"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-53291-8_31"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.24963\/ijcai.2021\/261"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD51958.2021.9643583"},{"key":"e_1_2_1_22_1","unstructured":"Google Inc.. 2020. HonggFuzz: Security oriented software fuzzer. Supports evolutionary feedback-driven fuzzing based on code coverage (SW and HW based). https:\/\/honggfuzz.dev\/ \t\t\t\t  Google Inc.. 2020. HonggFuzz: Security oriented software fuzzer. Supports evolutionary feedback-driven fuzzing based on code coverage (SW and HW based). https:\/\/honggfuzz.dev\/"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3318162"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993506"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103662"},{"key":"e_1_2_1_26_1","volume-title":"Miriyala Jeevan Kumar, and Subhajit Roy","author":"Kalita Pankaj Kumar","year":"2022","unstructured":"Pankaj Kumar Kalita , Miriyala Jeevan Kumar, and Subhajit Roy . 2022 . Synthesis of Semantic Actions in Attribute Grammars. In Formal Methods in Computer Aided Design (FMCAD \u201922). https:\/\/doi.org\/10.34727\/2021\/isbn.978-3-85448-053-2_37 10.34727\/2021 Pankaj Kumar Kalita, Miriyala Jeevan Kumar, and Subhajit Roy. 2022. Synthesis of Semantic Actions in Attribute Grammars. In Formal Methods in Computer Aided Design (FMCAD \u201922). https:\/\/doi.org\/10.34727\/2021\/isbn.978-3-85448-053-2_37"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54862-8_26"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3240765.3240842"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3533767.3534381"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.34727\/2020\/isbn.978-3-85448-042-6_24"},{"key":"e_1_2_1_31_1","volume-title":"This is boogie 2. manuscript KRML, 178, 131","author":"Leino K Rustan M","year":"2008","unstructured":"K Rustan M Leino . 2008. This is boogie 2. manuscript KRML, 178, 131 ( 2008 ), 9. K Rustan M Leino. 2008. This is boogie 2. manuscript KRML, 178, 131 (2008), 9."},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3213846.3213874"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/2813885.2738002"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3338906.3338921"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236024.3236049"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/2884781.2884807"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.7066264"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/3400302.3415709"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/357073.357079"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/1217856.1217859"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2019.00034"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360600"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/3293882.3330554"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-94583-1_13"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908093"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290385"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/2001420.2001425"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38856-9_9"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP40001.2021.00060"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236024.3236084"},{"key":"e_1_2_1_51_1","unstructured":"K Serebryany. 2015. libFuzzer a library for coverage-guided fuzz testing. LLVM project. \t\t\t\t  K Serebryany. 2015. libFuzzer a library for coverage-guided fuzz testing. LLVM project."},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.29007\/2ndp"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-012-0249-7"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/1065010.1065045"},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99524-9_1"},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/2509578.2509586"},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/3368826.3377910"},{"key":"e_1_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1145\/3106237.3106263"},{"key":"e_1_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-021-00387-z"},{"key":"e_1_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1145\/3460120.3484781"},{"key":"e_1_2_1_61_1","unstructured":"Michal Zalewski. 2019. American Fuzzy Lop. http:\/\/lcamtuf.coredump.cx\/afl \t\t\t\t  Michal Zalewski. 2019. American Fuzzy Lop. http:\/\/lcamtuf.coredump.cx\/afl"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3563332","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3563332","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:38:10Z","timestamp":1750178290000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3563332"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,10,31]]},"references-count":61,"journal-issue":{"issue":"OOPSLA2","published-print":{"date-parts":[[2022,10,31]]}},"alternative-id":["10.1145\/3563332"],"URL":"https:\/\/doi.org\/10.1145\/3563332","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,10,31]]},"assertion":[{"value":"2022-10-31","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}