{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,25]],"date-time":"2026-04-25T14:05:38Z","timestamp":1777125938437,"version":"3.51.4"},"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\/"}],"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>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, Orax, which establishes an oracle mapping information feedback loop between the SMT solver and the oracle handler. In Orax, 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. Orax 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 Orax outperforms existing methods, solving 118.37% and 13.83% more benchmarks than Delphi and Saadhak, respectively. In terms of efficiency, Orax achieves a PAR-2 score of 1.39, significantly exceeding Delphi\u2019s score of 669.13 and Saadhak\u2019s score of 173.31.<\/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, Beijing, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"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, Urbana, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0008-3723-4915","authenticated-orcid":false,"given":"Hanqin","family":"Guan","sequence":"additional","affiliation":[{"name":"Peking University, Beijing, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7558-9137","authenticated-orcid":false,"given":"Ding","family":"Li","sequence":"additional","affiliation":[{"name":"Peking University, Beijing, China"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2025,4,9]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"Verification and Validation. Industrial Practice: 8th International Symposium, ISoLA 2018, Limassol, Cyprus, November 5-9, 2018, Proceedings, Part IV 8. 376\u2013388","author":"Alt Leonardo","year":"2018","unstructured":"Leonardo Alt and Christian Reitwiessner. 2018. SMT-based verification of solidity smart contracts. In Leveraging Applications of Formal Methods, Verification and Validation. Industrial Practice: 8th International Symposium, ISoLA 2018, Limassol, Cyprus, November 5-9, 2018, Proceedings, Part IV 8. 376\u2013388."},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2016.14"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/11691617_9"},{"key":"e_1_2_1_4_1","volume-title":"Proceedings of SAT Competition 2017: Solver and Benchmark Descriptions. https:\/\/api.semanticscholar.org\/CorpusID:215763325","author":"Balyo Tom\u00e1s","year":"2017","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_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22110-1_14"},{"key":"e_1_2_1_6_1","volume-title":"Proceedings of the 8th international workshop on satisfiability modulo theories","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). 13, 14."},{"key":"e_1_2_1_7_1","doi-asserted-by":"crossref","unstructured":"Clark Barrett and Cesare Tinelli. 2018. Satisfiability modulo theories. Handbook of model checking 305\u2013343.","DOI":"10.1007\/978-3-319-10575-8_11"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-017-9432-6"},{"key":"e_1_2_1_9_1","volume-title":"Handbook of satisfiability. 185","author":"Biere Armin","unstructured":"Armin Biere, Marijn Heule, and Hans van Maaren. 2009. Handbook of satisfiability. 185, IOS press."},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE43902.2021.00071"},{"key":"e_1_2_1_11_1","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. 8, 209\u2013224.","journal-title":"OSDI."},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/1985793.1985995"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2408776.2408795"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3597495"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.artint.2013.09.001"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21690-4_19"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/1995376.1995394"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2593735.2593740"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3576915.3623103"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2635868.2635889"},{"key":"e_1_2_1_21_1","unstructured":"ESBMC. 2021. ESBMC. https:\/\/github.com\/esbmc\/esbmc\/tree\/master\/regression"},{"key":"e_1_2_1_22_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)."},{"key":"e_1_2_1_23_1","volume-title":"Cluster analysis of multivariate data: efficiency versus interpretability of classifications. biometrics, 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."},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993529"},{"key":"e_1_2_1_25_1","volume-title":"GNU Scientific Library Reference Manual -","author":"Gough Brian","year":"2078","unstructured":"Brian Gough. 2009. GNU Scientific Library Reference Manual - Third Edition (3rd ed.). Network Theory Ltd.. isbn:0954612078","edition":"3"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993506"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.2307\/2346830"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54862-8_26"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3240765.3240842"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3533767.3534381"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3318162"},{"key":"e_1_2_1_32_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."},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3213846.3213874"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3238147.3238176"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3338906.3338921"},{"key":"e_1_2_1_36_1","volume-title":"The global k-means clustering algorithm. Pattern recognition, 36, 2","author":"Likas Aristidis","year":"2003","unstructured":"Aristidis Likas, Nikos Vlassis, and Jakob J Verbeek. 2003. The global k-means clustering algorithm. Pattern recognition, 36, 2 (2003), 451\u2013461."},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1109\/TIT.1982.1056489"},{"key":"e_1_2_1_38_1","volume-title":"28th USENIX Security Symposium (USENIX Security 19)","author":"Lyu Chenyang","year":"2019","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_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236024.3236049"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/2884781.2884807"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-45641-6_26"},{"key":"e_1_2_1_42_1","volume-title":"Interactive Theorem Proving Modulo Fuzzing. In International Conference on Computer Aided Verification. 480\u2013493","author":"Muduli Sujit Kumar","year":"2024","unstructured":"Sujit Kumar Muduli, Rohan Ravikumar Padulkar, and Subhajit Roy. 2024. Interactive Theorem Proving Modulo Fuzzing. In International Conference on Computer Aided Verification. 480\u2013493."},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/3563332"},{"key":"e_1_2_1_44_1","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_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2019.00034"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-30048-7_34"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/3293882.3330554"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/2001420.2001425"},{"key":"e_1_2_1_49_1","volume-title":"29th USENIX Security Symposium (USENIX Security 20)","author":"Poeplau Sebastian","year":"2020","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_2_1_50_1","unstructured":"Elizabeth Polgreen. 2021. Delphi. https:\/\/github.com\/polgreen\/delphi"},{"key":"e_1_2_1_51_1","volume-title":"VMCAI 2022, Philadelphia, PA, USA, January 16\u201318, 2022, Proceedings 23","author":"Polgreen Elizabeth","year":"2022","unstructured":"Elizabeth Polgreen, Andrew Reynolds, and Sanjit A Seshia. 2022. Satisfiability and synthesis modulo oracles. In Verification, Model Checking, and Abstract Interpretation: 23rd International Conference, VMCAI 2022, Philadelphia, PA, USA, January 16\u201318, 2022, Proceedings 23. 263\u2013284."},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908093"},{"key":"e_1_2_1_53_1","unstructured":"LLVM Project. 2015. libFuzzer a library for coverage-guided fuzz testing. https:\/\/llvm.org\/docs\/LibFuzzer.html"},{"key":"e_1_2_1_54_1","unstructured":"LLVM Project. 2024. LLVM. https:\/\/llvm.org\/"},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1109\/ECBS.2013.15"},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-48989-6_36"},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP46214.2022.9833761"},{"key":"e_1_2_1_58_1","unstructured":"SMTCOMP. 2015. SMTCOMP SMTLib2 benchmarks. https:\/\/smtlib.cs.uiowa.edu\/benchmarks.shtml"},{"key":"e_1_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-012-0249-7"},{"key":"e_1_2_1_60_1","unstructured":"SyGuS. 2019. Benchmarks for SyGuS Competition. https:\/\/github.com\/SyGuS-Org\/benchmarks"},{"key":"e_1_2_1_61_1","first-page":"191","article-title":"Additive versus multiplicative clause weighting for SAT","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. 4, 191\u2013196.","journal-title":"AAAI."},{"key":"e_1_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.1145\/2509578.2509586"},{"key":"e_1_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1002\/apj.2125"},{"key":"e_1_2_1_64_1","doi-asserted-by":"crossref","unstructured":"Jinghan Wang Chengyu Song and Heng Yin. 2021. Reinforcement learning-based hierarchical seed scheduling for greybox fuzzing.","DOI":"10.14722\/ndss.2021.24486"},{"key":"e_1_2_1_65_1","doi-asserted-by":"publisher","DOI":"10.1145\/3576915.3623213"},{"key":"e_1_2_1_66_1","volume-title":"27th USENIX Security Symposium (USENIX Security 18)","author":"Yun Insu","year":"2018","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_2_1_67_1","unstructured":"Micha\u0142 Zalewski. 2021. AFL (American fuzzy lop). https:\/\/github.com\/google\/AFL"},{"key":"e_1_2_1_68_1","doi-asserted-by":"publisher","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":[[2025,10,9]],"date-time":"2025-10-09T17:13:10Z","timestamp":1760029990000},"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"}}]}}