{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,24]],"date-time":"2026-08-24T17:25:53Z","timestamp":1787592353440,"version":"build-2736575974"},"reference-count":68,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA1","license":[{"start":{"date-parts":[[2025,4,9]],"date-time":"2025-04-09T00:00:00Z","timestamp":1744156800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/legalcode"}],"funder":[{"name":"Beijing Natural Science Foundation","award":["L243010"],"award-info":[{"award-number":["L243010"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,4,9]]},"abstract":"<jats:p>\n                    Recent advancements in Satisfiability Modulo Theory (SMT) solving have significantly improved formula-driven techniques for verification, testing, repair, and synthesis. However, addressing open programs that lack formal specifications, such as those relying on third-party libraries, remains a challenge. The problem of Satisfiability Modulo Theories and Oracles (SMTO) has emerged as a critical issue where oracles, representing components with observable behavior but unknown implementation, hinder SMT solver from reasoning. Existing approaches like Delphi and Saadhak struggle to effectively combine sufficient oracle mapping information that is crucial for feasible solution construction with the reasoning capabilities of the SMT solver, leading to inefficient solving of SMTO problems. In this work, we propose a novel solving framework for SMTO problems,\n                    <jats:sc>Orax<\/jats:sc>\n                    , which establishes an oracle mapping information feedback loop between the SMT solver and the oracle handler. In\n                    <jats:sc>Orax<\/jats:sc>\n                    , the SMT solver analyzes the deficiency in oracle mapping information it has and feeds this back to the oracle handler. The oracle handler then provides the most suitable additional oracle mapping information back to the SMT solver.\n                    <jats:sc>Orax<\/jats:sc>\n                    employs a dual-clustering strategy to select the initial oracle mapping information provided to the SMT solver and a relaxation-based method to analyze the deficiency in the oracle mapping information the SMT solver knows. Experimental results on the benchmark suite demonstrate that\n                    <jats:sc>Orax<\/jats:sc>\n                    outperforms existing methods, solving 118.37% and 13.83% more benchmarks than Delphi and Saadhak, respectively. In terms of efficiency,\n                    <jats:sc>Orax<\/jats:sc>\n                    achieves a PAR-2 score of 1.39, significantly exceeding Delphi\u2019s score of 669.13 and Saadhak\u2019s score of 173.31.\n                  <\/jats:p>","DOI":"10.1145\/3720438","type":"journal-article","created":{"date-parts":[[2025,4,9]],"date-time":"2025-04-09T13:48:26Z","timestamp":1744206506000},"page":"676-703","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Orax: A Feedback-Driven Framework for Efficiently Solving Satisfiability Modulo Theories and Oracles"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0009-0007-2490-5671","authenticated-orcid":false,"given":"Zhineng","family":"Zhong","sequence":"first","affiliation":[{"name":"Peking University, School of Computer Science, Beijing, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8493-0261","authenticated-orcid":false,"given":"Ziqi","family":"Zhang","sequence":"additional","affiliation":[{"name":"University of Illinois at Urbana-Champaign, Department of Computer Science, Urbana, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0008-3723-4915","authenticated-orcid":false,"given":"Hanqin","family":"Guan","sequence":"additional","affiliation":[{"name":"Peking University, School of Computer Science, Beijing, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7558-9137","authenticated-orcid":false,"given":"Ding","family":"Li","sequence":"additional","affiliation":[{"name":"Peking University, School of Computer Science, Beijing, China"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,4,9]]},"reference":[{"key":"e_1_3_1_2_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-03427-6_28"},{"key":"e_1_3_1_3_2","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2016.14"},{"key":"e_1_3_1_4_2","doi-asserted-by":"publisher","DOI":"10.1007\/11691617_9"},{"key":"e_1_3_1_5_2","unstructured":"Tom\u00e1s Balyo Marijn J. H. Heule and Matti J\u00e4rvisalo. 2017. Proceedings of SAT Competition 2017: Solver and Benchmark Descriptions. https:\/\/api.semanticscholar.org\/CorpusID:215763325"},{"key":"e_1_3_1_6_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22110-1_14"},{"key":"e_1_3_1_7_2","first-page":"14","article-title":"The smt-lib standard: Version 2.0","volume":"13","author":"Barrett Clark","year":"2010","unstructured":"Clark Barrett, Aaron Stump, Cesare Tinelli, et al. 2010. The smt-lib standard: Version 2.0. In Proceedings of the 8th international workshop on satisfiability modulo theories (Edinburgh, UK), Vol. 13. 14.","journal-title":"Proceedings of the 8th international workshop on satisfiability modulo theories (Edinburgh, UK)"},{"key":"e_1_3_1_8_2","doi-asserted-by":"crossref","unstructured":"Clark Barrett and Cesare Tinelli. 2018. Satisfiability modulo theories. Handbook of model checking (2018) 305\u2013343.","DOI":"10.1007\/978-3-319-10575-8_11"},{"key":"e_1_3_1_9_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-017-9432-6"},{"key":"e_1_3_1_10_2","doi-asserted-by":"publisher","DOI":"10.5555\/1550723"},{"key":"e_1_3_1_11_2","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE43902.2021.00071"},{"key":"e_1_3_1_12_2","first-page":"209","article-title":"Klee: unassisted and automatic generation of high-coverage tests for complex systems programs.","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\u2013224.","journal-title":"OSDI"},{"key":"e_1_3_1_13_2","doi-asserted-by":"crossref","unstructured":"Cristian Cadar Patrice Godefroid Sarfraz Khurshid Corina S P\u0103s\u0103reanu Koushik Sen Nikolai Tillmann and Willem Visser. 2011. Symbolic execution for software testing in practice: preliminary assessment. In Proceedings of the 33rd International Conference on Software Engineering. 1066\u20131071.","DOI":"10.1145\/1985793.1985995"},{"key":"e_1_3_1_14_2","doi-asserted-by":"publisher","DOI":"10.1145\/2408776.2408795"},{"key":"e_1_3_1_15_2","doi-asserted-by":"publisher","DOI":"10.1145\/3597495"},{"key":"e_1_3_1_16_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.artint.2013.09.001"},{"key":"e_1_3_1_17_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21690-4_19"},{"key":"e_1_3_1_18_2","doi-asserted-by":"publisher","DOI":"10.1145\/1995376.1995394"},{"key":"e_1_3_1_19_2","doi-asserted-by":"crossref","unstructured":"Favio DeMarco Jifeng Xuan Daniel Le Berre and Martin Monperrus. 2014. Automatic repair of buggy if conditions and missing preconditions with smt. In Proceedings of the 6th international workshop on constraints in software testing verification and analysis. 30\u201339.","DOI":"10.1145\/2593735.2593740"},{"key":"e_1_3_1_20_2","doi-asserted-by":"crossref","unstructured":"Peng Deng Zhemin Yang Lei Zhang Guangliang Yang Wenzheng Hong Yuan Zhang and Min Yang. 2023. NestFuzz: Enhancing Fuzzing with Comprehensive Understanding of Input Processing Logic. In Proceedings of the 2023 ACM SIGSAC Conference on Computer and Communications Security. 1272\u20131286.","DOI":"10.1145\/3576915.3623103"},{"key":"e_1_3_1_21_2","doi-asserted-by":"crossref","unstructured":"Peter Dinges and Gul Agha. 2014. Solving complex path conditions through heuristic search on induced polytopes. In Proceedings of the 22nd ACM SIGSOFT International Symposium on Foundations of Software Engineering. 425\u2013436.","DOI":"10.1145\/2635868.2635889"},{"key":"e_1_3_1_22_2","unstructured":"ESBMC. 2021. ESBMC. https:\/\/github.com\/esbmc\/esbmc\/tree\/master\/regression."},{"key":"e_1_3_1_23_2","unstructured":"Andrea Fioraldi Dominik Maier Heiko Ei\u00dffeldt and Marc Heuse. 2020. {AFL++}: Combining incremental steps of fuzzing research. In 14th USENIX Workshop on Offensive Technologies (WOOT 20)."},{"key":"e_1_3_1_24_2","first-page":"768","article-title":"Cluster analysis of multivariate data: efficiency versus interpretability of classifications","volume":"21","author":"Forgy Edward W","year":"1965","unstructured":"Edward W Forgy. 1965. Cluster analysis of multivariate data: efficiency versus interpretability of classifications. biometrics 21 (1965), 768\u2013769.","journal-title":"biometrics"},{"key":"e_1_3_1_25_2","doi-asserted-by":"crossref","unstructured":"Patrice Godefroid. 2011. Higher-order test generation. In Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation. 258\u2013269.","DOI":"10.1145\/1993498.1993529"},{"key":"e_1_3_1_26_2","doi-asserted-by":"publisher","DOI":"10.5555\/1538674"},{"key":"e_1_3_1_27_2","doi-asserted-by":"crossref","unstructured":"Sumit Gulwani Susmit Jha Ashish Tiwari and Ramarathnam Venkatesan. 2011. Synthesis of loop-free programs. In Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation. 62\u201373.","DOI":"10.1145\/1993498.1993506"},{"key":"e_1_3_1_28_2","doi-asserted-by":"publisher","DOI":"10.2307\/2346830"},{"key":"e_1_3_1_29_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54862-8_26"},{"key":"e_1_3_1_30_2","doi-asserted-by":"publisher","DOI":"10.1145\/3240765.3240842"},{"key":"e_1_3_1_31_2","doi-asserted-by":"crossref","unstructured":"Sumit Lahiri and Subhajit Roy. 2022. Almost correct invariants: Synthesizing inductive invariants by fuzzing proofs. In Proceedings of the 31st ACM SIGSOFT International Symposium on Software Testing and Analysis. 352\u2013364.","DOI":"10.1145\/3533767.3534381"},{"key":"e_1_3_1_32_2","doi-asserted-by":"publisher","DOI":"10.1145\/3318162"},{"issue":"131","key":"e_1_3_1_33_2","first-page":"9","article-title":"This is boogie 2","volume":"178","author":"Leino K Rustan M","year":"2008","unstructured":"K Rustan M Leino. 2008. This is boogie 2. manuscript KRML 178, 131 (2008), 9.","journal-title":"manuscript KRML"},{"key":"e_1_3_1_34_2","doi-asserted-by":"crossref","unstructured":"Caroline Lemieux Rohan Padhye Koushik Sen and Dawn Song. 2018. Perffuzz: Automatically generating pathological inputs. In Proceedings of the 27th ACM SIGSOFT International Symposium on Software Testing and Analysis. 254\u2013265.","DOI":"10.1145\/3213846.3213874"},{"key":"e_1_3_1_35_2","doi-asserted-by":"crossref","unstructured":"Caroline Lemieux and Koushik Sen. 2018. Fairfuzz: A targeted mutation strategy for increasing greybox fuzz testing coverage. In Proceedings of the 33rd ACM\/IEEE international conference on automated software engineering. 475\u2013485.","DOI":"10.1145\/3238147.3238176"},{"key":"e_1_3_1_36_2","doi-asserted-by":"crossref","unstructured":"Daniel Liew Cristian Cadar Alastair F Donaldson and J Ryan Stinnett. 2019. Just fuzz it: solving floating-point constraints using coverage-guided fuzzing. In Proceedings of the 2019 27th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering. 521\u2013532.","DOI":"10.1145\/3338906.3338921"},{"key":"e_1_3_1_37_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0031-3203(02)00060-2"},{"key":"e_1_3_1_38_2","doi-asserted-by":"publisher","DOI":"10.1109\/TIT.1982.1056489"},{"key":"e_1_3_1_39_2","unstructured":"Chenyang Lyu Shouling Ji Chao Zhang Yuwei Li Wei-Han Lee Yu Song and Raheem Beyah. 2019. {MOPT}: Optimized mutation scheduling for fuzzers. In 28th USENIX Security Symposium (USENIX Security 19). 1949\u20131966."},{"key":"e_1_3_1_40_2","doi-asserted-by":"crossref","unstructured":"Sergey Mechtaev Alberto Griggio Alessandro Cimatti and Abhik Roychoudhury. 2018. Symbolic execution with existential second-order constraints. In Proceedings of the 2018 26th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering. 389\u2013399.","DOI":"10.1145\/3236024.3236049"},{"key":"e_1_3_1_41_2","doi-asserted-by":"crossref","unstructured":"Sergey Mechtaev Jooyong Yi and Abhik Roychoudhury. 2016. Angelix: Scalable multiline program patch synthesis via symbolic analysis. In Proceedings of the 38th international conference on software engineering. 691\u2013701.","DOI":"10.1145\/2884781.2884807"},{"key":"e_1_3_1_42_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-45641-6_26"},{"key":"e_1_3_1_43_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-65627-9_24"},{"key":"e_1_3_1_44_2","doi-asserted-by":"publisher","DOI":"10.1145\/3563332"},{"key":"e_1_3_1_45_2","doi-asserted-by":"publisher","unstructured":"Sujit Kumar Muduli and Subhajit Roy. 2022. Satisfiability Modulo Fuzzing: A Synergistic Combination of SMT Solving and Fuzzing (Artifact). https:\/\/doi.org\/10.5281\/zenodo.7066264 10.5281\/zenodo.7066264.","DOI":"10.5281\/zenodo.7066264"},{"key":"e_1_3_1_46_2","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2019.00034"},{"key":"e_1_3_1_47_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-30048-7_34"},{"key":"e_1_3_1_48_2","doi-asserted-by":"crossref","unstructured":"Awanish Pandey Phani Raj Goutham Kotcharlakota and Subhajit Roy. 2019. Deferred concretization in symbolic execution via fuzzing. In Proceedings of the 28th ACM SIGSOFT International Symposium on Software Testing and Analysis. 228\u2013238.","DOI":"10.1145\/3293882.3330554"},{"key":"e_1_3_1_49_2","doi-asserted-by":"crossref","unstructured":"Corina S P\u0103s\u0103reanu Neha Rungta and Willem Visser. 2011. Symbolic execution with mixed concrete-symbolic solving. In Proceedings of the 2011 International Symposium on Software Testing and Analysis. 34\u201344.","DOI":"10.1145\/2001420.2001425"},{"key":"e_1_3_1_50_2","unstructured":"Sebastian Poeplau and Aur\u00e9lien Francillon. 2020. Symbolic execution with {SymCC}: Don\u2019t interpret compile!. In 29th USENIX Security Symposium (USENIX Security 20). 181\u2013198."},{"key":"e_1_3_1_51_2","unstructured":"Elizabeth Polgreen. 2021. Delphi. https:\/\/github.com\/polgreen\/delphi."},{"key":"e_1_3_1_52_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-94583-1_13"},{"key":"e_1_3_1_53_2","doi-asserted-by":"crossref","unstructured":"Nadia Polikarpova Ivan Kuraj and Armando Solar-Lezama. 2016. Program synthesis from polymorphic refinement types. In Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation. 522\u2013538.","DOI":"10.1145\/2908080.2908093"},{"key":"e_1_3_1_54_2","unstructured":"LLVM Project. 2015. libFuzzer a library for coverage-guided fuzz testing. https:\/\/llvm.org\/docs\/LibFuzzer.html."},{"key":"e_1_3_1_55_2","unstructured":"LLVM Project. 2024. LLVM. https:\/\/llvm.org\/."},{"key":"e_1_3_1_56_2","doi-asserted-by":"publisher","DOI":"10.1109\/ECBS.2013.15"},{"key":"e_1_3_1_57_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-48989-6_36"},{"key":"e_1_3_1_58_2","doi-asserted-by":"publisher","DOI":"10.1109\/SP46214.2022.9833761"},{"key":"e_1_3_1_59_2","unstructured":"SMTCOMP. 2015. SMTCOMP SMTLib2 benchmarks. https:\/\/smtlib.cs.uiowa.edu\/benchmarks.shtml."},{"key":"e_1_3_1_60_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-012-0249-7"},{"key":"e_1_3_1_61_2","unstructured":"SyGuS. 2019. Benchmarks for SyGuS Competition. https:\/\/github.com\/SyGuS-Org\/benchmarks."},{"key":"e_1_3_1_62_2","first-page":"191","volume":"4","author":"Thornton John","year":"2004","unstructured":"John Thornton, Duc Nghia Pham, Stuart Bain, and Valnir Ferreira Jr. 2004. Additive versus multiplicative clause weighting for SAT. In AAAI, Vol. 4. 191\u2013196.","journal-title":"AAAI"},{"key":"e_1_3_1_63_2","doi-asserted-by":"crossref","unstructured":"Emina Torlak and Rastislav Bodik. 2013. Growing solver-aided languages with rosette. In Proceedings of the 2013 ACM international symposium on New ideas new paradigms and reflections on programming & software. 135\u2013152.","DOI":"10.1145\/2509578.2509586"},{"key":"e_1_3_1_64_2","doi-asserted-by":"publisher","DOI":"10.1002\/apj.2125"},{"key":"e_1_3_1_65_2","doi-asserted-by":"crossref","unstructured":"Jinghan Wang Chengyu Song and Heng Yin. 2021. Reinforcement learning-based hierarchical seed scheduling for greybox fuzzing. (2021).","DOI":"10.14722\/ndss.2021.24486"},{"key":"e_1_3_1_66_2","doi-asserted-by":"crossref","unstructured":"Yuanpeng Wang Ziqi Zhang Ningyu He Zhineng Zhong Shengjian Guo Qinkun Bao Ding Li Yao Guo and Xiangqun Chen. 2023. Symgx: Detecting cross-boundary pointer vulnerabilities of sgx applications via static symbolic execution. In Proceedings of the 2023 ACM SIGSAC Conference on Computer and Communications Security. 2710\u20132724.","DOI":"10.1145\/3576915.3623213"},{"key":"e_1_3_1_67_2","unstructured":"Insu Yun Sangho Lee Meng Xu Yeongjin Jang and Taesoo Kim. 2018. {QSYM}: A practical concolic execution engine tailored for hybrid fuzzing. In 27th USENIX Security Symposium (USENIX Security 18). 745\u2013761."},{"key":"e_1_3_1_68_2","unstructured":"Micha\u0142 Zalewski. 2021. AFL (American fuzzy lop). https:\/\/github.com\/google\/AFL."},{"key":"e_1_3_1_69_2","doi-asserted-by":"publisher","unstructured":"Zhineng Zhong Ziqi Zhang Hanqin Guan and Ding Li. 2025. Orax: A Feedback-Driven Framework for Efficiently Solving Satisfiability Modulo Theories and Oracles (Artifact). https:\/\/doi.org\/10.5281\/zenodo.14904107 10.5281\/zenodo.14904107.","DOI":"10.5281\/zenodo.14904107"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3720438","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3720438","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,8,24]],"date-time":"2026-08-24T16:31:28Z","timestamp":1787589088000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3720438"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,4,9]]},"references-count":68,"journal-issue":{"issue":"OOPSLA1","published-print":{"date-parts":[[2025,4,9]]}},"alternative-id":["10.1145\/3720438"],"URL":"https:\/\/doi.org\/10.1145\/3720438","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,4,9]]},"assertion":[{"value":"2024-10-14","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-02-18","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-04-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}