{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T19:08:26Z","timestamp":1760123306911,"version":"3.41.0"},"reference-count":74,"publisher":"Association for Computing Machinery (ACM)","issue":"PLDI","license":[{"start":{"date-parts":[[2024,6,20]],"date-time":"2024-06-20T00:00:00Z","timestamp":1718841600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-sa\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000001","name":"NSF","doi-asserted-by":"publisher","award":["2114627, 2237440"],"award-info":[{"award-number":["2114627, 2237440"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000185","name":"Defense Advanced Research Projects Agency","doi-asserted-by":"publisher","award":["N66001-21-C-4024"],"award-info":[{"award-number":["N66001-21-C-4024"]}],"id":[{"id":"10.13039\/100000185","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2024,6,20]]},"abstract":"<jats:p>SMT solvers are foundational tools for reasoning about constraints in practical problems both within and outside program analysis. Faster SMT solving improves the performance of practical tools and expands the set of tractable problems. Existing approaches to improving solver performance either focus on general algorithms applied below the level of individual theories, or focus on optimizations within a single theory. Unbounded constraints in which the number of possible variable values is infinite, such as real numbers and integers, pose a particularly difficult challenge for solvers. Bounded constraints in which the set of possible values is finite such as bitvectors and floating-point numbers, on the other hand, are decidable and have been the subject of extensive performance improvement efforts.<\/jats:p>\n          <jats:p>\n            This paper introduces a theory arbitrage: we transform unbounded constraints, which are often expensive to solve, into bounded constraints, which are typically cheaper to solve. By converting unbounded problems into bounded ones, theory arbitrage takes advantage of better performance on bounded constraints and unlocks optimization techniques that only apply to bounded theories. The transformation is achieved by harnessing a novel abstract interpretation strategy to infer bounds. The bounded transformed constraint is then an underapproximation of the semantics of the unbounded original. We realize our method for the theories of integers and real numbers with a practical tool (STAUB). Our evaluation demonstrates that theory arbitrage alone can speed up individual constraints by orders of magnitude and achieve up to a\n            <jats:inline-formula>\n              <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\" display=\"inline\">\n                <mml:mn>1.4<\/mml:mn>\n                <mml:mo>\u00d7<\/mml:mo>\n              <\/mml:math>\n            <\/jats:inline-formula>\n            speedup on average across nonlinear integer benchmarks. Furthermore, it enables the use of the recent compiler optimization-based technique SLOT for unbounded SMT theories, unlocking a further speedup of up to\n            <jats:inline-formula>\n              <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\" display=\"inline\">\n                <mml:mn>3<\/mml:mn>\n                <mml:mo>\u00d7<\/mml:mo>\n              <\/mml:math>\n            <\/jats:inline-formula>\n            . Finally, we incorporate STAUB into a practical termination proving tool and observe an overall\n            <jats:inline-formula>\n              <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\" display=\"inline\">\n                <mml:mn>9<\/mml:mn>\n                <mml:mo>%<\/mml:mo>\n              <\/mml:math>\n            <\/jats:inline-formula>\n            improvement in performance.\n          <\/jats:p>","DOI":"10.1145\/3656387","type":"journal-article","created":{"date-parts":[[2024,6,20]],"date-time":"2024-06-20T16:27:20Z","timestamp":1718900840000},"page":"246-271","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["SMT Theory Arbitrage: Approximating Unbounded Constraints using Bounded Theories"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4195-8464","authenticated-orcid":false,"given":"Benjamin","family":"Mikek","sequence":"first","affiliation":[{"name":"Georgia Institute of Technology, Atlanta, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5367-9377","authenticated-orcid":false,"given":"Qirun","family":"Zhang","sequence":"additional","affiliation":[{"name":"Georgia Institute of Technology, Atlanta, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2024,6,20]]},"reference":[{"key":"e_1_3_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-94583-1_2"},{"key":"e_1_3_1_3_1","first-page":"10338","article-title":"Learning to solve SMT formulas","author":"Balunovi\u0107 Mislav","year":"2018","unstructured":"Mislav Balunovi\u0107, Pavol Bielik, and Martin Vechev. 2018. Learning to solve SMT formulas. In Proceedings of the 32nd International Conference on Neural Information Processing Systems (Montr\u00e9al, Canada) (NIPS\u201918). Curran Associates Inc., Red Hook, NY, USA, 10338-10349.","journal-title":"In Proceedings of the 32nd International Conference on Neural Information Processing Systems (Montr\u00e9al, Canada) (NIPS\u201918)"},{"key":"e_1_3_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99524-9_24"},{"key":"e_1_3_1_5_1","volume-title":"The SMT-LIB Standard","author":"Barrett Clark","year":"2017","unstructured":"Clark Barrett, Pascal Fontaine, and Cesare Tinelli. 2017. The SMT-LIB Standard: Version 2.6. Technical Report Department of Computer Science, The University of Iowa. Available at www.SMT-LIB.org."},{"key":"e_1_3_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10575-8"},{"key":"e_1_3_1_7_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2022.12.009"},{"key":"e_1_3_1_8_1","first-page":"55","article-title":"Z3str3: a string solver with theory-aware heuristics","author":"Berzish Murphy","year":"2017","unstructured":"Murphy Berzish, Vijay Ganesh, and Yunhui Zheng. 2017. Z3str3: a string solver with theory-aware heuristics. In Proceedings of the 17th Conference on Formal Methods in Computer-Aided Design (Vienna, Austria) (FMCAD \u201817). FMCAD Inc, Austin, Texas, 55-59.","journal-title":"In Proceedings of the 17th Conference on Formal Methods in Computer-Aided Design (Vienna, Austria) (FMCAD \u201817)"},{"key":"e_1_3_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81688-9_14"},{"key":"e_1_3_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99527-0_20"},{"key":"e_1_3_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-017-9432-6"},{"key":"e_1_3_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-38499-8_3"},{"key":"e_1_3_1_13_1","first-page":"643","volume-title":"In 26th USENIX Security Symposium (USENIX Security 17)","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 17). USENIX Association, Vancouver, BC 643-659."},{"key":"e_1_3_1_14_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.cie.2020.106777"},{"key":"e_1_3_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17462-0_5"},{"key":"e_1_3_1_16_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511921698"},{"key":"e_1_3_1_17_1","first-page":"209","article-title":"KLEE: unassisted and automatic generation of high-coverage tests for complex systems programs","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 (San Diego, California) (OSDI\u201908). USENIX Association, USA, 209-224.","journal-title":"In Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation (San Diego, California) (OSDI\u201908)"},{"key":"e_1_3_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009846"},{"key":"e_1_3_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-36742-7_7"},{"key":"e_1_3_1_20_1","first-page":"187","volume-title":"Formal Methods in Computer-Aided Design, FMCAD 2012","author":"Cimatti Alessandro","year":"2012","unstructured":"Alessandro Cimatti, Sergio Mover, and Stefano Tonetta. 2012. A quantifier-free SMT encoding of non-linear hybrid automata. In Formal Methods in Computer-Aided Design, FMCAD 2012. IEEE, 187-195."},{"key":"e_1_3_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/567752.567778"},{"key":"e_1_3_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-77505-8_23"},{"key":"e_1_3_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3589250.3596144"},{"key":"e_1_3_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535874"},{"key":"e_1_3_1_25_1","first-page":"323","article-title":"Hilbert\u2019s tenth problem: Diophantine equations: positive aspects of a negative solution","author":"Davis Martin","year":"1976","unstructured":"Martin Davis, Yuri Matijasevi\u010d, and Julia Robinson. 1976. Hilbert\u2019s tenth problem: Diophantine equations: positive aspects of a negative solution. In Mathematical developments arising from Hilbert problems (Proceedings of Symposia in Pure Mathematics, Vol. XXVIII). American Mathematical Society, Providence, RI, 323-378. (loose erratum).","journal-title":"In Mathematical developments arising from Hilbert problems (Proceedings of Symposia in Pure Mathematics, Vol. XXVIII)"},{"key":"e_1_3_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_3_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22438-6_18"},{"key":"e_1_3_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-44245-2_10"},{"key":"e_1_3_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_49"},{"key":"e_1_3_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/11817963_11"},{"key":"e_1_3_1_31_1","unstructured":"Pascal Fontaine. 2022. SMT-LIB Google Group: FixedSizeBitVectors QF_BV overflows. https:\/\/groups.google.com\/u\/0\/"},{"key":"e_1_3_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38574-2_14"},{"key":"e_1_3_1_33_1","doi-asserted-by":"publisher","unstructured":"Khalil Ghorbal Eric Goubault and Sylvie Putot. 2010. A Logical Product Approach to Zonotope Intersection. (2010) 212-226. https:\/\/doi.org\/10.1007\/978-3-642-14295-6_22 10.1007\/978-3-642-14295-6_22","DOI":"10.1007\/978-3-642-14295-6_22"},{"key":"e_1_3_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38856-9_1"},{"key":"e_1_3_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/11823230_3"},{"key":"e_1_3_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-18275-4_17"},{"key":"e_1_3_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-30820-8_39"},{"key":"e_1_3_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99527-0_21"},{"key":"e_1_3_1_39_1","first-page":"1","volume-title":"Institute of Electrical and Electronics Engineers Standard for Floating-Point Arithmetic","author":"IEEE","year":"2019","unstructured":"IEEE. 2019. Institute of Electrical and Electronics Engineers Standard for Floating-Point Arithmetic. IEEE Std 754-2019 (Revision of IEEE 754-2008) (2019), 1-84."},{"key":"e_1_3_1_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-57288-8_15"},{"key":"e_1_3_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/1806799.1806833"},{"key":"e_1_3_1_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-02508-3_15"},{"key":"e_1_3_1_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-51825-7_27"},{"key":"e_1_3_1_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31365-3_27"},{"key":"e_1_3_1_45_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74105-3"},{"key":"e_1_3_1_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81688-9_35"},{"key":"e_1_3_1_47_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89963-3_16"},{"key":"e_1_3_1_48_1","first-page":"601","article-title":"Floatingpoint symbolic execution: a case study in n-version programming","author":"Liew Daniel","year":"2017","unstructured":"Daniel Liew, Daniel Schemmel, Cristian Cadar, Alastair F. Donaldson, Rafael Z\u00e4hl, and Klaus Wehrle. 2017. Floatingpoint symbolic execution: a case study in n-version programming. In Proceedings of the 32nd IEEE\/ACM International Conference on Automated Software Engineering (Urbana-Champaign, IL, USA) (ASE \u201917). IEEE Press, 601-612.","journal-title":"In Proceedings of the 32nd IEEE\/ACM International Conference on Automated Software Engineering (Urbana-Champaign, IL, USA) (ASE \u201917)"},{"key":"e_1_3_1_49_1","unstructured":"Nuno P. Lopes Levent Aksoy Vasco M. Manquinho and Jos\u00e9 Monteiro. 2010. Optimally Solving the MCM Problem Using Pseudo-Boolean Satisfiability. CoRR abs\/1011.2685 (2010). arXiv:1011.2685 http:\/\/arxiv.org\/abs\/1011.2685"},{"key":"e_1_3_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454030"},{"key":"e_1_3_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/3611643.3616357"},{"key":"e_1_3_1_52_1","doi-asserted-by":"publisher","unstructured":"Benjamin Mikek and Qirun Zhang. 2024. STAUB: PLDI Artifact Evaluation. https:\/\/doi.org\/10.5281\/zenodo.10895770 10.5281\/zenodo.10895770","DOI":"10.5281\/zenodo.10895770"},{"key":"e_1_3_1_53_1","volume-title":"Department of Computer Science","author":"M\u00f8ller Anders","year":"2018","unstructured":"Anders M\u00f8ller and Michael I. Schwartzbach. 2018. Static Program Analysis. Department of Computer Science, Aarhus University, http:\/\/cs.au.dk\/~amoeller\/spa\/."},{"key":"e_1_3_1_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/3563332"},{"key":"e_1_3_1_55_1","doi-asserted-by":"publisher","unstructured":"Casey B Mulligan. 2016. Automated Economic Reasoning with Quantifier Elimination. Working Paper 22922. National Bureau of Economic Research. https:\/\/doi.org\/10.3386\/w22922 10.3386\/w22922","DOI":"10.3386\/w22922"},{"key":"e_1_3_1_56_1","unstructured":"Aina Niemetz and Mathias Preiner. 2020. Bitwuzla at the SMT-COMP 2020. CoRR abs\/2006.01621 (2020). arXiv:2006.01621"},{"key":"e_1_3_1_57_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-72013-1_8"},{"key":"e_1_3_1_58_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-24258-9_20"},{"key":"e_1_3_1_59_1","first-page":"71","article-title":"CalCS: SMT Solving for Non-Linear Convex Constraints","author":"Nuzzo Pierluigi","year":"2010","unstructured":"Pierluigi Nuzzo, Alberto Puggelli, Sanjit A. Seshia, and Alberto Sangiovanni-Vincentelli. 2010. CalCS: SMT Solving for Non-Linear Convex Constraints. In Proceedings of the 2010 Conference on Formal Methods in Computer-Aided Design (Lugano, Switzerland) (FMCAD \u201810). FMCAD Inc, Austin, Texas, 71-80.","journal-title":"In Proceedings of the 2010 Conference on Formal Methods in Computer-Aided Design (Lugano, Switzerland) (FMCAD \u201810)"},{"key":"e_1_3_1_60_1","doi-asserted-by":"publisher","unstructured":"Christos H. Papadimitriou. 1981. On the complexity of integer programming. F. ACM 28 4 (Oct 1981) 765-768 https:\/\/doi.org\/10.1145\/322276.322287 10.1145\/322276.322287","DOI":"10.1145\/322276.322287"},{"key":"e_1_3_1_61_1","first-page":"153","article-title":"Integrating Proxy Theories and Numeric Model Lifting for Floating Point Arithmetic","author":"Ramachandran Jaideep","year":"2016","unstructured":"Jaideep Ramachandran and Thomas Wahl. 2016. Integrating Proxy Theories and Numeric Model Lifting for Floating Point Arithmetic. In Proceedings of the 16th Conference on Formal Methods in Computer-Aided Design (Mountain View, California) (FMCAD \u201816). FMCAD Inc, Austin, Texas, 153-160.","journal-title":"In Proceedings of the 16th Conference on Formal Methods in Computer-Aided Design (Mountain View, California) (FMCAD \u201816)"},{"key":"e_1_3_1_62_1","unstructured":"Andrew Reynolds Haniel Barbosa Cesare Tinelli Aina Niemetz Andres Noetzli Mathias Preiner and Clark Barrett. 2018. Rewrites for SMT Solvers Using Syntax-Guided Enumeration. http:\/\/homepage.divms.uiowa.edu\/ ajreynol\/pressmt2018.pdf"},{"key":"e_1_3_1_63_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21668-3_12"},{"key":"e_1_3_1_64_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25543-5_2"},{"key":"e_1_3_1_65_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-023-00696-0"},{"key":"e_1_3_1_66_1","first-page":"67","article-title":"SMT-Based Constraint Answer Set Solver EZSMT+ for Non-Tight Programs","author":"Shen Da","year":"2018","unstructured":"Da Shen and Yuliya Lierler. 2018. SMT-Based Constraint Answer Set Solver EZSMT+ for Non-Tight Programs. In Principles of Knowledge Representation and Reasoning: Proceedings of the Sixteenth International Conference, KR 2018, Tempe, Arizona, 30 October - 2 November 2018. AAAI Press, 67-71.","journal-title":"In Principles of Knowledge Representation and Reasoning: Proceedings of the Sixteenth International Conference, KR 2018"},{"key":"e_1_3_1_67_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-7091-9459-1_3"},{"key":"e_1_3_1_68_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3385985"},{"key":"e_1_3_1_69_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02658-4_60"},{"key":"e_1_3_1_70_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454068"},{"key":"e_1_3_1_71_1","doi-asserted-by":"publisher","DOI":"10.1145\/3395363.3397378"},{"key":"e_1_3_1_72_1","doi-asserted-by":"publisher","DOI":"10.1145\/3591288"},{"key":"e_1_3_1_73_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-94205-6_17"},{"key":"e_1_3_1_74_1","doi-asserted-by":"publisher","unstructured":"Aleksandar Zeljic Christoph M. Wintersteiger and Philipp R\u00fcmmer. 2017. An Approximation Framework for Solvers and Decision Procedures. 7. Autom. Reason. 58 1 (2017) 127-147. https:\/\/doi.org\/10.1007\/S10817-016-9393-1 10.1007\/S10817-016-9393-1","DOI":"10.1007\/S10817-016-9393-1"},{"key":"e_1_3_1_75_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-94583-1_24"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3656387","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3656387","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:44:25Z","timestamp":1751661865000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3656387"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,6,20]]},"references-count":74,"journal-issue":{"issue":"PLDI","published-print":{"date-parts":[[2024,6,20]]}},"alternative-id":["10.1145\/3656387"],"URL":"https:\/\/doi.org\/10.1145\/3656387","relation":{},"ISSN":["2475-1421"],"issn-type":[{"type":"electronic","value":"2475-1421"}],"subject":[],"published":{"date-parts":[[2024,6,20]]},"assertion":[{"value":"2024-06-20","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}