{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,29]],"date-time":"2026-01-29T22:10:21Z","timestamp":1769724621958,"version":"3.49.0"},"publisher-location":"New York, NY, USA","reference-count":47,"publisher":"ACM","license":[{"start":{"date-parts":[[2021,6,18]],"date-time":"2021-06-18T00:00:00Z","timestamp":1623974400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000001","name":"NSF (National Science Foundation)","doi-asserted-by":"publisher","award":["CNS-1948489"],"award-info":[{"award-number":["CNS-1948489"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2021,6,19]]},"DOI":"10.1145\/3453483.3454068","type":"proceedings-article","created":{"date-parts":[[2021,6,18]],"date-time":"2021-06-18T13:51:32Z","timestamp":1624024292000},"page":"651-664","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":18,"title":["Boosting SMT solver performance on mixed-bitwise-arithmetic expressions"],"prefix":"10.1145","author":[{"given":"Dongpeng","family":"Xu","sequence":"first","affiliation":[{"name":"University of New Hampshire, USA"}]},{"given":"Binbin","family":"Liu","sequence":"additional","affiliation":[{"name":"University of New Hampshire, USA \/ University of Science and Technology of China, China"}]},{"given":"Weijie","family":"Feng","sequence":"additional","affiliation":[{"name":"University of Science and Technology of China, China"}]},{"given":"Jiang","family":"Ming","sequence":"additional","affiliation":[{"name":"University of Texas at Arlington, USA"}]},{"given":"Qilong","family":"Zheng","sequence":"additional","affiliation":[{"name":"University of Science and Technology of China, China"}]},{"given":"Jing","family":"Li","sequence":"additional","affiliation":[{"name":"University of Science and Technology of China, China"}]},{"given":"Qiaoyan","family":"Yu","sequence":"additional","affiliation":[{"name":"University of New Hampshire, USA"}]}],"member":"320","published-online":{"date-parts":[[2021,6,18]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"crossref","unstructured":"Sebastian Banescu and Alexander Pretschner. 2018. Chapter Five - A Tutorial on Software Obfuscation.  Sebastian Banescu and Alexander Pretschner. 2018. Chapter Five - A Tutorial on Software Obfuscation.","DOI":"10.1016\/bs.adcom.2017.09.004"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2017.36"},{"key":"e_1_3_2_1_3_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 \u2013 Version 2.0 . In Proceedings of the 8th International Workshop on Satisfiability Modulo Theories. Clark Barrett, Aaron Stump, and Cesare Tinelli. 2010. The SMT-LIB Standard \u2013 Version 2.0. In Proceedings of the 8th International Workshop on Satisfiability Modulo Theories."},{"key":"e_1_3_2_1_4_1","unstructured":"Michael Beeler R William Gosper and Richard Schroeppel. 1972. Hakmem. Massachusetts Institute of Technology Artificial Intelligence Laboratory.  Michael Beeler R William Gosper and Richard Schroeppel. 1972. Hakmem. Massachusetts Institute of Technology Artificial Intelligence Laboratory."},{"key":"e_1_3_2_1_5_1","unstructured":"Fabrizio Biondi S\u00e9bastien Josse and Axel Legay. 2016. Bypassing Malware Obfuscation with Dynamic Synthesis. https:\/\/ercim-news.ercim.eu\/en106\/special\/bypassing-malware-obfuscation-with-dynamic-synthesis  Fabrizio Biondi S\u00e9bastien Josse and Axel Legay. 2016. Bypassing Malware Obfuscation with Dynamic Synthesis. https:\/\/ercim-news.ercim.eu\/en106\/special\/bypassing-malware-obfuscation-with-dynamic-synthesis"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3293880.3294103"},{"key":"e_1_3_2_1_7_1","volume-title":"Proceedings of the 26th USENIX Security Symposium (USENIX Security\u201917)","author":"Blazytko Tim","year":"2017","unstructured":"Tim Blazytko , Moritz Contag , Cornelius Aschermann , and Thorsten Holz . 2017 . Syntia: Synthesizing the Semantics of Obfuscated Code . In Proceedings of the 26th USENIX Security Symposium (USENIX Security\u201917) . Tim Blazytko, Moritz Contag, Cornelius Aschermann, and Thorsten Holz. 2017. Syntia: Synthesizing the Semantics of Obfuscated Code. In Proceedings of the 26th USENIX Security Symposium (USENIX Security\u201917)."},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2013.6606558"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00768-2_16"},{"key":"e_1_3_2_1_10_1","volume-title":"Proceedings of the 8th USENIX Symposium 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 Symposium on Operating Systems Design and Implementation (OSDI\u201908) . 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 Symposium on Operating Systems Design and Implementation (OSDI\u201908)."},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3238147.3238218"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2420950.2420997"},{"key":"e_1_3_2_1_13_1","unstructured":"Christian Collberg Sam Martin Jonathan Myers and Bill Zimmerman. [n.d.]. Documentation for Arithmetic Encodings in Tigress. http:\/\/tigress.cs.arizona.edu\/transformPage\/docs\/encodeArithmetic  Christian Collberg Sam Martin Jonathan Myers and Bill Zimmerman. [n.d.]. Documentation for Arithmetic Encodings in Tigress. http:\/\/tigress.cs.arizona.edu\/transformPage\/docs\/encodeArithmetic"},{"key":"e_1_3_2_1_14_1","unstructured":"Christian Collberg Sam Martin Jonathan Myers and Bill Zimmerman. [n.d.]. Documentation for Data Encodings in Tigress. http:\/\/tigress.cs.arizona.edu\/transformPage\/docs\/encodeData  Christian Collberg Sam Martin Jonathan Myers and Bill Zimmerman. [n.d.]. Documentation for Data Encodings in Tigress. http:\/\/tigress.cs.arizona.edu\/transformPage\/docs\/encodeData"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/800157.805047"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"crossref","unstructured":"Leonardo De Moura and Grant Olney Passmore. 2013. The Strategy Challenge in SMT Solving. In Automated Reasoning and Mathematics.  Leonardo De Moura and Grant Olney Passmore. 2013. The Strategy Challenge in SMT Solving. In Automated Reasoning and Mathematics.","DOI":"10.1007\/978-3-642-36675-8_2"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2995306.2995308"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41540-6_11"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73368-3_52"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22110-1_1"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/1065010.1065036"},{"key":"e_1_3_2_1_23_1","volume-title":"Proceedings of the 15th Annual Network and Distributed System Security Symposium (NDSS\u201908)","author":"Godefroid Patrice","year":"2008","unstructured":"Patrice Godefroid , Michael Y. Levin , and David Molnar . 2008 . Automated Whitebox Fuzz Testing . In Proceedings of the 15th Annual Network and Distributed System Security Symposium (NDSS\u201908) . Patrice Godefroid, Michael Y. Levin, and David Molnar. 2008. Automated Whitebox Fuzz Testing. In Proceedings of the 15th Annual Network and Distributed System Security Symposium (NDSS\u201908)."},{"key":"e_1_3_2_1_24_1","unstructured":"Irdeto. 2017. Irdeto Cloaked CA: a secure flexible and cost-effective conditional access system. www.irdeto.com  Irdeto. 2017. Irdeto Cloaked CA: a secure flexible and cost-effective conditional access system. www.irdeto.com"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/2771783.2771806"},{"key":"e_1_3_2_1_26_1","volume-title":"Formal Verification of a Realistic Compiler. Commun. ACM, 52, 7","author":"Leroy Xavier","year":"2009","unstructured":"Xavier Leroy . 2009. Formal Verification of a Realistic Compiler. Commun. ACM, 52, 7 ( 2009 ), July. Xavier Leroy. 2009. Formal Verification of a Realistic Compiler. Commun. ACM, 52, 7 (2009), July."},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/2970276.2970364"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/1375696.1375702"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3338906.3338921"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1109\/TIFS.2019.2908071"},{"key":"e_1_3_2_1_31_1","unstructured":"MapleSoft. 2020. The Essential Tool for Mathematics. https:\/\/www.maplesoft.com\/products\/maple\/  MapleSoft. 2020. The Essential Tool for Mathematics. https:\/\/www.maplesoft.com\/products\/maple\/"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-016-0267-2"},{"key":"e_1_3_2_1_33_1","volume-title":"DRM Obfuscation Versus Auxiliary Attacks. In REcon Conference.","author":"Mougey Camille","year":"2014","unstructured":"Camille Mougey and Francis Gabriel . 2014 . DRM Obfuscation Versus Auxiliary Attacks. In REcon Conference. Camille Mougey and Francis Gabriel. 2014. DRM Obfuscation Versus Auxiliary Attacks. In REcon Conference."},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_3_2_1_35_1","volume-title":"Boolector at the SMT Competition","author":"Niemetz Aina","year":"2017","unstructured":"Aina Niemetz , Mathias Preiner , and Armin Biere . 2016. Boolector at the SMT Competition 2017 . Institute for Formal Models and Verification, Johannes Kepler University . Aina Niemetz, Mathias Preiner, and Armin Biere. 2016. Boolector at the SMT Competition 2017. Institute for Formal Models and Verification, Johannes Kepler University."},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3359789.3359812"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371307.3371309"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/2001420.2001425"},{"key":"e_1_3_2_1_39_1","unstructured":"Quarkslab. 2019. Epona Application Protection v1.5. https:\/\/epona.quarkslab.com  Quarkslab. 2019. Epona Application Protection v1.5. https:\/\/epona.quarkslab.com"},{"key":"e_1_3_2_1_40_1","unstructured":"sagemath. 2020. SageMath. http:\/\/www.sagemath.org\/  sagemath. 2020. SageMath. http:\/\/www.sagemath.org\/"},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/1095430.1081750"},{"key":"e_1_3_2_1_42_1","volume-title":"Proceedings of the 15th Annual Network and Distributed System Security Symposium (NDSS\u201908)","author":"Sharif Monirul","year":"2008","unstructured":"Monirul Sharif , Andrea Lanzi , Jonathon Giffin , and Wenke Lee . 2008 . Impeding Malware Analysis Using Conditional Code Obfuscation . In Proceedings of the 15th Annual Network and Distributed System Security Symposium (NDSS\u201908) . Monirul Sharif, Andrea Lanzi, Jonathon Giffin, and Wenke Lee. 2008. Impeding Malware Analysis Using Conditional Code Obfuscation. In Proceedings of the 15th Annual Network and Distributed System Security Symposium (NDSS\u201908)."},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2017.26"},{"key":"e_1_3_2_1_44_1","unstructured":"H.S. Warren. 2003. Hacker\u2019s Delight. Addison-Wesley.  H.S. Warren. 2003. Hacker\u2019s Delight. Addison-Wesley."},{"key":"e_1_3_2_1_45_1","unstructured":"WOLFRAM. 2020. WOLFRAM MATHEMATICA. http:\/\/www.wolfram.com\/mathematica\/  WOLFRAM. 2020. WOLFRAM MATHEMATICA. http:\/\/www.wolfram.com\/mathematica\/"},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491411.2491456"},{"key":"e_1_3_2_1_47_1","volume-title":"Diversity via Code Transformations: A Solution for NGNA Renewable Security","author":"Zhou Yongxin","unstructured":"Yongxin Zhou and Alec Main . 2006. Diversity via Code Transformations: A Solution for NGNA Renewable Security . The National Cable and Telecommunications Association Show . Yongxin Zhou and Alec Main. 2006. Diversity via Code Transformations: A Solution for NGNA Renewable Security. The National Cable and Telecommunications Association Show."},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-77535-5_5"}],"event":{"name":"PLDI '21: 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation","location":"Virtual Canada","acronym":"PLDI '21","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"]},"container-title":["Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3453483.3454068","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/abs\/10.1145\/3453483.3454068","content-type":"text\/html","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3453483.3454068","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3453483.3454068","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T20:47:47Z","timestamp":1750193267000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3453483.3454068"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,6,18]]},"references-count":47,"alternative-id":["10.1145\/3453483.3454068","10.1145\/3453483"],"URL":"https:\/\/doi.org\/10.1145\/3453483.3454068","relation":{},"subject":[],"published":{"date-parts":[[2021,6,18]]},"assertion":[{"value":"2021-06-18","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}