{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,2]],"date-time":"2026-10-02T07:58:20Z","timestamp":1790927900255,"version":"4.1.0"},"reference-count":100,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA","license":[{"start":{"date-parts":[[2021,10,15]],"date-time":"2021-10-15T00:00:00Z","timestamp":1634256000000},"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":[[2021,10,20]]},"abstract":"<jats:p>\n            This paper concerns the scalability challenges of symbolic abstraction: given a formula \u03d5 in a logic\n            <jats:italic>L<\/jats:italic>\n            and an abstract domain\n            <jats:italic>A<\/jats:italic>\n            , find a most precise element in the abstract domain that over-approximates the meaning of \u03d5. Symbolic abstraction is an important point in the space of abstract interpretation, as it allows for automatically synthesizing the best abstract transformers. However, current techniques for symbolic abstraction can have difficulty delivering on its practical strengths, due to performance issues.\n          <\/jats:p>\n          <jats:p>In this work, we introduce two algorithms for the symbolic abstraction of quantifier-free bit-vector formulas, which apply to the bit-vector interval domain and a certain kind of polyhedral domain, respectively. We implement and evaluate the proposed techniques on two machine code analysis clients, namely static memory corruption analysis and constrained random fuzzing. Using a suite of 57,933 queries from the clients, we compare our approach against a diverse group of state-of-the-art algorithms. The experiments show that our algorithms achieve a substantial speedup over existing techniques and illustrate significant precision advantages for the clients. Our work presents strong evidence that symbolic abstraction of numeric domains can be efficient and practical for large and realistic programs.<\/jats:p>","DOI":"10.1145\/3485495","type":"journal-article","created":{"date-parts":[[2021,10,15]],"date-time":"2021-10-15T19:18:28Z","timestamp":1634325508000},"page":"1-32","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":15,"title":["Program analysis via efficient symbolic abstraction"],"prefix":"10.1145","volume":"5","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-0342-9518","authenticated-orcid":false,"given":"Peisen","family":"Yao","sequence":"first","affiliation":[{"name":"Hong Kong University of Science and Technology, China \/ Ant Group, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Qingkai","family":"Shi","sequence":"additional","affiliation":[{"name":"Ant Group, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Heqing","family":"Huang","sequence":"additional","affiliation":[{"name":"Hong Kong University of Science and Technology, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Charles","family":"Zhang","sequence":"additional","affiliation":[{"name":"Hong Kong University of Science and Technology, China"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2021,10,15]]},"reference":[{"key":"e_1_2_2_1_1","unstructured":"2014. AFL: american fuzzy lop. http:\/\/lcamtuf.coredump.cx\/afl\/ Accessed: 2014  2014. AFL: american fuzzy lop. http:\/\/lcamtuf.coredump.cx\/afl\/ Accessed: 2014"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1109\/HLDVT.2009.5340162"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0747-7171(88)80016-6"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/s12532-016-0104-z"},{"key":"e_1_2_2_5_1","volume-title":"FMCAD 2018","author":"Backeman Peter","year":"2018","unstructured":"Peter Backeman , Philipp R\u00fcmmer , and Aleksandar Zeljic . 2018 . Bit-Vector Interpolation and Quantifier Elimination by Lazy Reduction. In 2018 Formal Methods in Computer Aided Design , FMCAD 2018 , Austin, TX, USA, October 30 - November 2, 2018, Nikolaj Bj\u00f8rner and Arie Gurfinkel (Eds.). IEEE, 1\u201310. Peter Backeman, Philipp R\u00fcmmer, and Aleksandar Zeljic. 2018. Bit-Vector Interpolation and Quantifier Elimination by Lazy Reduction. In 2018 Formal Methods in Computer Aided Design, FMCAD 2018, Austin, TX, USA, October 30 - November 2, 2018, Nikolaj Bj\u00f8rner and Arie Gurfinkel (Eds.). IEEE, 1\u201310."},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2017.67"},{"key":"e_1_2_2_7_1","volume-title":"Barrett and Cesare Tinelli","author":"Clark","year":"2018","unstructured":"Clark W. Barrett and Cesare Tinelli . 2018 . Satisfiability Modulo Theories. In Handbook of Model Checking, Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, and Roderick Bloem (Eds.). Springer , 305\u2013343. Clark W. Barrett and Cesare Tinelli. 2018. Satisfiability Modulo Theories. In Handbook of Model Checking, Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, and Roderick Bloem (Eds.). Springer, 305\u2013343."},{"key":"e_1_2_2_8_1","volume-title":"Range and Set Abstraction using SAT. Electron. Notes Theor. Comput. Sci., 267, 1","author":"Barrett Edd","year":"2010","unstructured":"Edd Barrett and Andy King . 2010. Range and Set Abstraction using SAT. Electron. Notes Theor. Comput. Sci., 267, 1 ( 2010 ). Edd Barrett and Andy King. 2010. Range and Set Abstraction using SAT. Electron. Notes Theor. Comput. Sci., 267, 1 (2010)."},{"key":"e_1_2_2_9_1","volume-title":"Gr\u00f6bner bases - a computational approach to commutative algebra (Graduate texts in mathematics","author":"Becker Thomas","unstructured":"Thomas Becker , Volker Weispfenning , and Heinz Kredel . 1993. Gr\u00f6bner bases - a computational approach to commutative algebra (Graduate texts in mathematics , Vol. 141). Springer. isbn:978-3-540-97971- 5 Thomas Becker, Volker Weispfenning, and Heinz Kredel. 1993. Gr\u00f6bner bases - a computational approach to commutative algebra (Graduate texts in mathematics, Vol. 141). Springer. isbn:978-3-540-97971-5"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2009.5351147"},{"key":"e_1_2_2_11_1","volume-title":"VMCAI 2018, Los Angeles, CA, USA, January 7-9, 2018, Proceedings, Isil Dillig and Jens Palsberg (Eds.) (Lecture Notes in Computer Science","volume":"93","author":"Biondi Fabrizio","year":"2018","unstructured":"Fabrizio Biondi , Michael A. Enescu , Annelie Heuser , Axel Legay , Kuldeep S. Meel , and Jean Quilbeuf . 2018 . Scalable Approximation of Quantitative Information Flow in Programs. In Verification, Model Checking, and Abstract Interpretation - 19th International Conference , VMCAI 2018, Los Angeles, CA, USA, January 7-9, 2018, Proceedings, Isil Dillig and Jens Palsberg (Eds.) (Lecture Notes in Computer Science , Vol. 10747). Springer, 71\u2013 93 . Fabrizio Biondi, Michael A. Enescu, Annelie Heuser, Axel Legay, Kuldeep S. Meel, and Jean Quilbeuf. 2018. Scalable Approximation of Quantitative Information Flow in Programs. In Verification, Model Checking, and Abstract Interpretation - 19th International Conference, VMCAI 2018, Los Angeles, CA, USA, January 7-9, 2018, Proceedings, Isil Dillig and Jens Palsberg (Eds.) (Lecture Notes in Computer Science, Vol. 10747). Springer, 71\u201393."},{"key":"e_1_2_2_12_1","volume-title":"Proceedings of the 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems -","volume":"9035","author":"Bj\u00f8rner Nikolaj","year":"2015","unstructured":"Nikolaj Bj\u00f8rner , Anh-Dung Phan , and Lars Fleckenstein . 2015 . \u03bd Z-an optimizing SMT solver . In Proceedings of the 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems - Volume 9035 . Springer-Verlag, Berlin, Heidelberg. 194\u2013199. isbn:978-3-662-46680-3 Nikolaj Bj\u00f8rner, Anh-Dung Phan, and Lars Fleckenstein. 2015. \u03bd Z-an optimizing SMT solver. In Proceedings of the 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems - Volume 9035. Springer-Verlag, Berlin, Heidelberg. 194\u2013199. isbn:978-3-662-46680-3"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/781131.781153"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.5555\/1882094.1882105"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jpaa.2008.11.043"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2012.10.003"},{"key":"e_1_2_2_17_1","first-page":"2375","volume-title":"2018 IEEE Symposium on Security and Privacy (SP). 00","author":"Chen P.","unstructured":"P. Chen and H. Chen . 2018. Angora: Efficient Fuzzing by Principled Search . In 2018 IEEE Symposium on Security and Privacy (SP). 00 , 711\u2013725. issn: 2375 - 1207 P. Chen and H. Chen. 2018. Angora: Efficient Fuzzing by Principled Search. In 2018 IEEE Symposium on Security and Privacy (SP). 00, 711\u2013725. issn:2375-1207"},{"key":"e_1_2_2_18_1","article-title":"Fast MCMC Sampling Algorithms on Polytopes","volume":"19","author":"Chen Yuansi","year":"2018","unstructured":"Yuansi Chen , Raaz Dwivedi , Martin J. Wainwright , and Bin Yu . 2018 . Fast MCMC Sampling Algorithms on Polytopes . J. Mach. Learn. Res. , 19 (2018), 55:1\u201355:86. Yuansi Chen, Raaz Dwivedi, Martin J. Wainwright, and Bin Yu. 2018. Fast MCMC Sampling Algorithms on Polytopes. J. Mach. Learn. Res., 19 (2018), 55:1\u201355:86.","journal-title":"J. Mach. Learn. Res."},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-4076(03)00100-3"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/800022.808314"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/567752.567778"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/512760.512770"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314601"},{"key":"e_1_2_2_24_1","volume-title":"Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence, IJCAI 2017","author":"Dathathri Sumanth","year":"2017","unstructured":"Sumanth Dathathri , Nikos Ar\u00e9chiga , Sicun Gao , and Richard M. Murray . 2017. Learning-Based Abstractions for Nonlinear Constraint Solving . In Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence, IJCAI 2017 , Melbourne, Australia , August 19-25, 2017 , Carles Sierra (Ed.). ijcai.org, 592\u2013599. Sumanth Dathathri, Nikos Ar\u00e9chiga, Sicun Gao, and Richard M. Murray. 2017. Learning-Based Abstractions for Nonlinear Constraint Solving. In Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence, IJCAI 2017, Melbourne, Australia, August 19-25, 2017, Carles Sierra (Ed.). ijcai.org, 592\u2013599."},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792734.1792766"},{"key":"e_1_2_2_26_1","first-page":"2375","volume-title":"LAVA: Large-Scale Automated Vulnerability Addition. In 2016 IEEE Symposium on Security and Privacy (SP). 110\u2013121","author":"Dolan-Gavitt B.","unstructured":"B. Dolan-Gavitt , P. Hulin , E. Kirda , T. Leek , A. Mambretti , W. Robertson , F. Ulrich , and R. Whelan . 2016 . LAVA: Large-Scale Automated Vulnerability Addition. In 2016 IEEE Symposium on Security and Privacy (SP). 110\u2013121 . issn: 2375 - 1207 B. Dolan-Gavitt, P. Hulin, E. Kirda, T. Leek, A. Mambretti, W. Robertson, F. Ulrich, and R. Whelan. 2016. LAVA: Large-Scale Automated Vulnerability Addition. In 2016 IEEE Symposium on Security and Privacy (SP). 110\u2013121. issn:2375-1207"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3180155.3180248"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1137\/0217060"},{"key":"e_1_2_2_29_1","volume-title":"Proceedings of the 30th International Conference on Machine Learning, ICML 2013, Atlanta, GA, USA, 16-21 June 2013 (JMLR Workshop and Conference Proceedings","volume":"342","author":"Ermon Stefano","year":"2013","unstructured":"Stefano Ermon , Carla P. Gomes , Ashish Sabharwal , and Bart Selman . 2013 . Taming the Curse of Dimensionality: Discrete Integration by Hashing and Optimization . In Proceedings of the 30th International Conference on Machine Learning, ICML 2013, Atlanta, GA, USA, 16-21 June 2013 (JMLR Workshop and Conference Proceedings , Vol. 28). JMLR.org, 334\u2013 342 . Stefano Ermon, Carla P. Gomes, Ashish Sabharwal, and Bart Selman. 2013. Taming the Curse of Dimensionality: Discrete Integration by Hashing and Optimization. In Proceedings of the 30th International Conference on Machine Learning, ICML 2013, Atlanta, GA, USA, 16-21 June 2013 (JMLR Workshop and Conference Proceedings, Vol. 28). JMLR.org, 334\u2013342."},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-94205-6_10"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.5555\/1770351.1770421"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/2651360"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.5555\/1770351.1770365"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78739-6_16"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3386016"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/2597809.2597817"},{"key":"e_1_2_2_37_1","volume-title":"Pangolin: Incremental Hybrid Fuzzing with Polyhedral Path Abstraction. In 2020 IEEE Symposium on Security and Privacy, SP 2020","author":"Huang Heqing","year":"2020","unstructured":"Heqing Huang , Peisen Yao , Rongxin Wu , Qingkai Shi , and Charles Zhang . 2020 . Pangolin: Incremental Hybrid Fuzzing with Polyhedral Path Abstraction. In 2020 IEEE Symposium on Security and Privacy, SP 2020 , San Francisco, CA, USA , May 18-21, 2020. IEEE, 1613\u20131627. Heqing Huang, Peisen Yao, Rongxin Wu, Qingkai Shi, and Charles Zhang. 2020. Pangolin: Incremental Hybrid Fuzzing with Polyhedral Path Abstraction. In 2020 IEEE Symposium on Security and Privacy, SP 2020, San Francisco, CA, USA, May 18-21, 2020. IEEE, 1613\u20131627."},{"key":"e_1_2_2_38_1","volume-title":"VMCAI 2017, Paris, France, January 15-17, 2017, Proceedings, Ahmed Bouajjani and David Monniaux (Eds.) (Lecture Notes in Computer Science","volume":"329","author":"Jiang Jiahong","year":"2017","unstructured":"Jiahong Jiang , Liqian Chen , Xueguang Wu , and Ji Wang . 2017 . Block-Wise Abstract Interpretation by Combining Abstract Domains with SMT. In Verification, Model Checking, and Abstract Interpretation - 18th International Conference , VMCAI 2017, Paris, France, January 15-17, 2017, Proceedings, Ahmed Bouajjani and David Monniaux (Eds.) (Lecture Notes in Computer Science , Vol. 10145). Springer, 310\u2013 329 . Jiahong Jiang, Liqian Chen, Xueguang Wu, and Ji Wang. 2017. Block-Wise Abstract Interpretation by Combining Abstract Domains with SMT. In Verification, Model Checking, and Abstract Interpretation - 18th International Conference, VMCAI 2017, Paris, France, January 15-17, 2017, Proceedings, Ahmed Bouajjani and David Monniaux (Eds.) (Lecture Notes in Computer Science, Vol. 10145). Springer, 310\u2013329."},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.5555\/2032305.2032344"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-36742-7_6"},{"key":"e_1_2_2_41_1","volume-title":"Bordeaux","volume":"283","author":"Jon\u00e1s Martin","year":"2016","unstructured":"Martin Jon\u00e1s and Jan Strejcek . 2016 . Solving Quantified Bit-Vector Formulas Using Binary Decision Diagrams. In Theory and Applications of Satisfiability Testing - SAT 2016 - 19th International Conference , Bordeaux , France, July 5-8, 2016, Proceedings, Nadia Creignou and Daniel Le Berre (Eds.) (Lecture Notes in Computer Science , Vol. 9710). Springer, 267\u2013 283 . Martin Jon\u00e1s and Jan Strejcek. 2016. Solving Quantified Bit-Vector Formulas Using Binary Decision Diagrams. In Theory and Applications of Satisfiability Testing - SAT 2016 - 19th International Conference, Bordeaux, France, July 5-8, 2016, Proceedings, Nadia Creignou and Daniel Le Berre (Eds.) (Lecture Notes in Computer Science, Vol. 9710). Springer, 267\u2013283."},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/1536414.1536491"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1287\/moor.1110.0519"},{"key":"e_1_2_2_44_1","volume-title":"Proc. ACM Program. Lang., 2, POPL","author":"Kincaid Zachary","year":"2017","unstructured":"Zachary Kincaid , John Cyphert , Jason Breck , and Thomas Reps . 2017 . Non-Linear Reasoning for Invariant Synthesis . Proc. ACM Program. Lang., 2, POPL (2017), Article 54, Dec., 33 pages. Zachary Kincaid, John Cyphert, Jason Breck, and Thomas Reps. 2017. Non-Linear Reasoning for Invariant Synthesis. Proc. ACM Program. Lang., 2, POPL (2017), Article 54, Dec., 33 pages."},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD.2007.4397275"},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103675"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-016-0249-4"},{"key":"e_1_2_2_48_1","volume-title":"Delta-Decision Procedures for Exists-Forall Problems over the Reals. 10982","author":"Kong Soonho","year":"2018","unstructured":"Soonho Kong , Armando Solar-Lezama , and Sicun Gao . 2018. Delta-Decision Procedures for Exists-Forall Problems over the Reals. 10982 ( 2018 ), 219\u2013235. Soonho Kong, Armando Solar-Lezama, and Sicun Gao. 2018. Delta-Decision Procedures for Exists-Forall Problems over the Reals. 10982 (2018), 219\u2013235."},{"key":"e_1_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.1007\/11817963_39"},{"key":"e_1_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535857"},{"key":"e_1_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/2450136.2450139"},{"key":"e_1_2_2_52_1","first-page":"1","article-title":"On strongest necessary and weakest sufficient conditions","volume":"128","author":"Lin Fangzhen","year":"2001","unstructured":"Fangzhen Lin . 2001 . On strongest necessary and weakest sufficient conditions . Artif. Intell. , 128 , 1 - 2 (2001), 143\u2013159. Fangzhen Lin. 2001. On strongest necessary and weakest sufficient conditions. Artif. Intell., 128, 1-2 (2001), 143\u2013159.","journal-title":"Artif. Intell."},{"key":"e_1_2_2_53_1","volume-title":"Working Notes of AAAI Fall Symposium on Relevance. 154\u2013159","author":"Lin Fangzhen","year":"1994","unstructured":"Fangzhen Lin and Ray Reiter . 1994 . Forget it . In Working Notes of AAAI Fall Symposium on Relevance. 154\u2013159 . Fangzhen Lin and Ray Reiter. 1994. Forget it. In Working Notes of AAAI Fall Symposium on Relevance. 154\u2013159."},{"key":"e_1_2_2_54_1","volume-title":"Proceedings of the 3rd International Workshop on Worst-Case Execution Time Analysis, WCET 2003 - a Satellite Event to ECRTS 2003, Polytechnic Institute of Porto","author":"Lisper Bj\u00f6rn","year":"2003","unstructured":"Bj\u00f6rn Lisper . 2003 . Fully Automatic, Parametric Worst-Case Execution Time Analysis . In Proceedings of the 3rd International Workshop on Worst-Case Execution Time Analysis, WCET 2003 - a Satellite Event to ECRTS 2003, Polytechnic Institute of Porto , Portugal, July 1, 2003, Jan Gustafsson (Ed.). MDH-MRTC-116\/ 2003-1-SE, Department of Computer Science and Engineering, M\u00e4lardalen University, Box 883, 721 23 V\u00e4ster\u00e5s, Sweden, 99\u2013102. Bj\u00f6rn Lisper. 2003. Fully Automatic, Parametric Worst-Case Execution Time Analysis. In Proceedings of the 3rd International Workshop on Worst-Case Execution Time Analysis, WCET 2003 - a Satellite Event to ECRTS 2003, Polytechnic Institute of Porto, Portugal, July 1, 2003, Jan Gustafsson (Ed.). MDH-MRTC-116\/2003-1-SE, Department of Computer Science and Engineering, M\u00e4lardalen University, Box 883, 721 23 V\u00e4ster\u00e5s, Sweden, 99\u2013102."},{"key":"e_1_2_2_55_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78791-4_14"},{"key":"e_1_2_2_56_1","doi-asserted-by":"publisher","DOI":"10.1093\/comjnl\/36.5.450"},{"key":"e_1_2_2_57_1","volume-title":"Proceedings of the 35th Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS \u201920)","author":"Meel Kuldeep S.","unstructured":"Kuldeep S. Meel and S. Akshay . 2020. Sparse Hashing for Scalable Approximate Model Counting: Theory and Practice . In Proceedings of the 35th Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS \u201920) . Association for Computing Machinery, New York, NY, USA. 728\u2013741. isbn:9781450371049 Kuldeep S. Meel and S. Akshay. 2020. Sparse Hashing for Scalable Approximate Model Counting: Theory and Practice. In Proceedings of the 35th Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS \u201920). Association for Computing Machinery, New York, NY, USA. 728\u2013741. isbn:9781450371049"},{"key":"e_1_2_2_58_1","doi-asserted-by":"publisher","DOI":"10.5555\/645774.668110"},{"key":"e_1_2_2_59_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10990-006-8609-1"},{"key":"e_1_2_2_60_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480899"},{"key":"e_1_2_2_61_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14295-6_51"},{"key":"e_1_2_2_62_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49674-9_53"},{"key":"e_1_2_2_63_1","doi-asserted-by":"publisher","DOI":"10.5555\/2892753.2892928"},{"key":"e_1_2_2_64_1","volume-title":"CP 2013, Uppsala, Sweden, September 16-20, 2013. Proceedings, Christian Schulte (Ed.) (Lecture Notes in Computer Science","author":"Naveh Reuven","unstructured":"Reuven Naveh and Amit Metodi . [n. d.]. Beyond Feasibility : CP Usage in Constrained-Random Functional Hardware Verification. In Principles and Practice of Constraint Programming - 19th International Conference , CP 2013, Uppsala, Sweden, September 16-20, 2013. Proceedings, Christian Schulte (Ed.) (Lecture Notes in Computer Science , Vol. 8124). Reuven Naveh and Amit Metodi. [n. d.]. Beyond Feasibility: CP Usage in Constrained-Random Functional Hardware Verification. In Principles and Practice of Constraint Programming - 19th International Conference, CP 2013, Uppsala, Sweden, September 16-20, 2013. Proceedings, Christian Schulte (Ed.) (Lecture Notes in Computer Science, Vol. 8124)."},{"key":"e_1_2_2_65_1","doi-asserted-by":"publisher","DOI":"10.1145\/1250734.1250746"},{"key":"e_1_2_2_66_1","volume-title":"CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, Part II, Hana Chockler and Georg Weissenbacher (Eds.) (Lecture Notes in Computer Science","volume":"255","author":"Niemetz Aina","year":"2018","unstructured":"Aina Niemetz , Mathias Preiner , Andrew Reynolds , Clark W. Barrett , and Cesare Tinelli . 2018 . Solving Quantified Bit-Vectors Using Invertibility Conditions. In Computer Aided Verification - 30th International Conference , CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, Part II, Hana Chockler and Georg Weissenbacher (Eds.) (Lecture Notes in Computer Science , Vol. 10982). Springer, 236\u2013 255 . Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, and Cesare Tinelli. 2018. Solving Quantified Bit-Vectors Using Invertibility Conditions. In Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, Part II, Hana Chockler and Georg Weissenbacher (Eds.) (Lecture Notes in Computer Science, Vol. 10982). Springer, 236\u2013255."},{"key":"e_1_2_2_67_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-72013-1_8"},{"key":"e_1_2_2_68_1","doi-asserted-by":"publisher","DOI":"10.1007\/11814948_18"},{"key":"e_1_2_2_69_1","volume-title":"29th USENIX Security Symposium, USENIX Security 2020, August 12-14","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 2020, August 12-14 , 2020, Srdjan Capkun and Franziska Roesner (Eds.). USENIX Association, 181\u2013198. Sebastian Poeplau and Aur\u00e9lien Francillon. 2020. Symbolic execution with SymCC: Don\u2019t interpret, compile!. In 29th USENIX Security Symposium, USENIX Security 2020, August 12-14, 2020, Srdjan Capkun and Franziska Roesner (Eds.). USENIX Association, 181\u2013198."},{"key":"e_1_2_2_70_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54577-5_15"},{"key":"e_1_2_2_71_1","doi-asserted-by":"publisher","DOI":"10.1145\/1024393.1024410"},{"key":"e_1_2_2_72_1","doi-asserted-by":"publisher","DOI":"10.5555\/1788374.1788377"},{"key":"e_1_2_2_73_1","volume-title":"5th International Conference, VMCAI 2004, Venice, Italy, January 11-13, 2004, Proceedings, Bernhard Steffen and Giorgio Levi (Eds.) (Lecture Notes in Computer Science","volume":"266","author":"Reps Thomas W.","year":"2004","unstructured":"Thomas W. Reps , Shmuel Sagiv , and Greta Yorsh . 2004 . Symbolic Implementation of the Best Transformer. In Verification, Model Checking, and Abstract Interpretation , 5th International Conference, VMCAI 2004, Venice, Italy, January 11-13, 2004, Proceedings, Bernhard Steffen and Giorgio Levi (Eds.) (Lecture Notes in Computer Science , Vol. 2937). Springer, 252\u2013 266 . Thomas W. Reps, Shmuel Sagiv, and Greta Yorsh. 2004. Symbolic Implementation of the Best Transformer. In Verification, Model Checking, and Abstract Interpretation, 5th International Conference, VMCAI 2004, Venice, Italy, January 11-13, 2004, Proceedings, Bernhard Steffen and Giorgio Levi (Eds.) (Lecture Notes in Computer Science, Vol. 2937). Springer, 252\u2013266."},{"key":"e_1_2_2_74_1","volume-title":"VMCAI 2016, St. Petersburg, FL, USA, January 17-19, 2016. Proceedings, Barbara Jobstmann and K. Rustan M. Leino (Eds.) (Lecture Notes in Computer Science","volume":"40","author":"Thomas","unstructured":"Thomas W. Reps and Aditya V. Thakur. 2016. Automating Abstract Interpretation. In Verification, Model Checking, and Abstract Interpretation - 17th International Conference , VMCAI 2016, St. Petersburg, FL, USA, January 17-19, 2016. Proceedings, Barbara Jobstmann and K. Rustan M. Leino (Eds.) (Lecture Notes in Computer Science , Vol. 9583). Springer, 3\u2013 40 . Thomas W. Reps and Aditya V. Thakur. 2016. Automating Abstract Interpretation. In Verification, Model Checking, and Abstract Interpretation - 17th International Conference, VMCAI 2016, St. Petersburg, FL, USA, January 17-19, 2016. Proceedings, Barbara Jobstmann and K. Rustan M. Leino (Eds.) (Lecture Notes in Computer Science, Vol. 9583). Springer, 3\u201340."},{"key":"e_1_2_2_75_1","volume-title":"Compiler Optimizations using Symbolic Abstraction. Ph. D. Dissertation","author":"Ritter Fabian","unstructured":"Fabian Ritter . 2015. Compiler Optimizations using Symbolic Abstraction. Ph. D. Dissertation . Saarland University . Fabian Ritter. 2015. Compiler Optimizations using Symbolic Abstraction. Ph. D. Dissertation. Saarland University."},{"key":"e_1_2_2_76_1","doi-asserted-by":"publisher","DOI":"10.1007\/11823230_2"},{"key":"e_1_2_2_77_1","doi-asserted-by":"publisher","DOI":"10.1145\/2699915"},{"key":"e_1_2_2_78_1","doi-asserted-by":"publisher","DOI":"10.1145\/2699915"},{"key":"e_1_2_2_79_1","volume-title":"CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part I, Daniel Kroening and Corina S. Pasareanu (Eds.) (Lecture Notes in Computer Science","volume":"454","author":"Sebastiani Roberto","year":"2015","unstructured":"Roberto Sebastiani and Patrick Trentin . 2015 . OptiMathSAT: A Tool for Optimization Modulo Theories. In Computer Aided Verification - 27th International Conference , CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part I, Daniel Kroening and Corina S. Pasareanu (Eds.) (Lecture Notes in Computer Science , Vol. 9206). Springer, 447\u2013 454 . Roberto Sebastiani and Patrick Trentin. 2015. OptiMathSAT: A Tool for Optimization Modulo Theories. In Computer Aided Verification - 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part I, Daniel Kroening and Corina S. Pasareanu (Eds.) (Lecture Notes in Computer Science, Vol. 9206). Springer, 447\u2013454."},{"key":"e_1_2_2_80_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46681-0_27"},{"key":"e_1_2_2_81_1","volume-title":"An Abstract Domain for Bit-Vector Inequalities","author":"Sharma Tushar","unstructured":"Tushar Sharma , Thomas Reps , and Aditya Thakur . 2013. An Abstract Domain for Bit-Vector Inequalities . University of Wisconsin-Madison Department of Computer Sciences. Tushar Sharma, Thomas Reps, and Aditya Thakur. 2013. An Abstract Domain for Bit-Vector Inequalities. University of Wisconsin-Madison Department of Computer Sciences."},{"key":"e_1_2_2_82_1","volume-title":"VMCAI 2017, Paris, France, January 15-17, 2017, Proceedings, Ahmed Bouajjani and David Monniaux (Eds.) (Lecture Notes in Computer Science","volume":"520","author":"Sharma Tushar","unstructured":"Tushar Sharma and Thomas W. Reps . 2017. Sound Bit-Precise Numerical Domains. In Verification, Model Checking, and Abstract Interpretation - 18th International Conference , VMCAI 2017, Paris, France, January 15-17, 2017, Proceedings, Ahmed Bouajjani and David Monniaux (Eds.) (Lecture Notes in Computer Science , Vol. 10145). Springer, 500\u2013 520 . Tushar Sharma and Thomas W. Reps. 2017. Sound Bit-Precise Numerical Domains. In Verification, Model Checking, and Abstract Interpretation - 18th International Conference, VMCAI 2017, Paris, France, January 15-17, 2017, Proceedings, Ahmed Bouajjani and David Monniaux (Eds.) (Lecture Notes in Computer Science, Vol. 10145). Springer, 500\u2013520."},{"key":"e_1_2_2_83_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2016.17"},{"key":"e_1_2_2_84_1","volume-title":"14th International Symposium, SAS 2007, Kongens Lyngby, Denmark, August 22-24, 2007, Proceedings, Hanne Riis Nielson and Gilberto Fil\u00e9 (Eds.) (Lecture Notes in Computer Science","volume":"136","author":"Simon Axel","year":"2007","unstructured":"Axel Simon and Andy King . 2007 . Taming the Wrapping of Integer Arithmetic. In Static Analysis , 14th International Symposium, SAS 2007, Kongens Lyngby, Denmark, August 22-24, 2007, Proceedings, Hanne Riis Nielson and Gilberto Fil\u00e9 (Eds.) (Lecture Notes in Computer Science , Vol. 4634). Springer, 121\u2013 136 . Axel Simon and Andy King. 2007. Taming the Wrapping of Integer Arithmetic. In Static Analysis, 14th International Symposium, SAS 2007, Kongens Lyngby, Denmark, August 22-24, 2007, Proceedings, Hanne Riis Nielson and Gilberto Fil\u00e9 (Eds.) (Lecture Notes in Computer Science, Vol. 4634). Springer, 121\u2013136."},{"key":"e_1_2_2_85_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009885"},{"key":"e_1_2_2_86_1","volume-title":"Proc. ACM Program. Lang., 2, POPL","author":"Singh Gagandeep","year":"2017","unstructured":"Gagandeep Singh , Markus P\u00fcschel , and Martin Vechev . 2017 . A Practical Construction for Decomposing Numerical Abstract Domains . Proc. ACM Program. Lang., 2, POPL (2017), Article 55, Dec., 28 pages. issn:2475-1421 Gagandeep Singh, Markus P\u00fcschel, and Martin Vechev. 2017. A Practical Construction for Decomposing Numerical Abstract Domains. Proc. ACM Program. Lang., 2, POPL (2017), Article 55, Dec., 28 pages. issn:2475-1421"},{"key":"e_1_2_2_87_1","volume-title":"Proc. ACM Program. Lang., 2, POPL","author":"Singh Gagandeep","year":"2017","unstructured":"Gagandeep Singh , Markus P\u00fcschel , and Martin Vechev . 2017 . A Practical Construction for Decomposing Numerical Abstract Domains . Proc. ACM Program. Lang., 2, POPL (2017), Article 55, Dec., 28 pages. issn:2475-1421 Gagandeep Singh, Markus P\u00fcschel, and Martin Vechev. 2017. A Practical Construction for Decomposing Numerical Abstract Domains. Proc. ACM Program. Lang., 2, POPL (2017), Article 55, Dec., 28 pages. issn:2475-1421"},{"key":"e_1_2_2_88_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2738000"},{"key":"e_1_2_2_89_1","volume-title":"CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, Part I, Hana Chockler and Georg Weissenbacher (Eds.) (Lecture Notes in Computer Science","volume":"229","author":"Singh Gagandeep","unstructured":"Gagandeep Singh , Markus P\u00fcschel , and Martin T. Vechev . 2018. Fast Numerical Program Analysis with Reinforcement Learning. In Computer Aided Verification - 30th International Conference , CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, Part I, Hana Chockler and Georg Weissenbacher (Eds.) (Lecture Notes in Computer Science , Vol. 10981). Springer, 211\u2013 229 . Gagandeep Singh, Markus P\u00fcschel, and Martin T. Vechev. 2018. Fast Numerical Program Analysis with Reinforcement Learning. In Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, Part I, Hana Chockler and Georg Weissenbacher (Eds.) (Lecture Notes in Computer Science, Vol. 10981). Springer, 211\u2013229."},{"key":"e_1_2_2_90_1","doi-asserted-by":"publisher","DOI":"10.1109\/MSP.2016.14"},{"key":"e_1_2_2_91_1","volume-title":"Driller: Augmenting Fuzzing Through Selective Symbolic Execution. In 23rd Annual Network and Distributed System Security Symposium, NDSS 2016","author":"Stephens Nick","year":"2016","unstructured":"Nick Stephens , John Grosen , Christopher Salls , Andrew Dutcher , Ruoyu Wang , Jacopo Corbetta , Yan Shoshitaishvili , Christopher Kruegel , and Giovanni Vigna . 2016 . Driller: Augmenting Fuzzing Through Selective Symbolic Execution. In 23rd Annual Network and Distributed System Security Symposium, NDSS 2016 , San Diego, California, USA , February 21-24, 2016. The Internet Society. Nick Stephens, John Grosen, Christopher Salls, Andrew Dutcher, Ruoyu Wang, Jacopo Corbetta, Yan Shoshitaishvili, Christopher Kruegel, and Giovanni Vigna. 2016. Driller: Augmenting Fuzzing Through Selective Symbolic Execution. In 23rd Annual Network and Distributed System Security Symposium, NDSS 2016, San Diego, California, USA, February 21-24, 2016. The Internet Society."},{"key":"e_1_2_2_92_1","volume-title":"ICFEM 2019, Shenzhen, China, November 5-9, 2019, Proceedings, Yamine A\u00eft Ameur and Shengchao Qin (Eds.) (Lecture Notes in Computer Science","volume":"352","author":"Sullivan Allison","year":"2019","unstructured":"Allison Sullivan , Darko Marinov , and Sarfraz Khurshid . 2019 . Solution Enumeration Abstraction: A Modeling Idiom to Enhance a Lightweight Formal Method. In Formal Methods and Software Engineering - 21st International Conference on Formal Engineering Methods , ICFEM 2019, Shenzhen, China, November 5-9, 2019, Proceedings, Yamine A\u00eft Ameur and Shengchao Qin (Eds.) (Lecture Notes in Computer Science , Vol. 11852). Springer, 336\u2013 352 . Allison Sullivan, Darko Marinov, and Sarfraz Khurshid. 2019. Solution Enumeration Abstraction: A Modeling Idiom to Enhance a Lightweight Formal Method. In Formal Methods and Software Engineering - 21st International Conference on Formal Engineering Methods, ICFEM 2019, Shenzhen, China, November 5-9, 2019, Proceedings, Yamine A\u00eft Ameur and Shengchao Qin (Eds.) (Lecture Notes in Computer Science, Vol. 11852). Springer, 336\u2013352."},{"key":"e_1_2_2_93_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-33125-1_10"},{"key":"e_1_2_2_94_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2015.02.003"},{"key":"e_1_2_2_95_1","volume-title":"CAV 2012, Berkeley, CA, USA, July 7-13, 2012 Proceedings, P. Madhusudan and Sanjit A. Seshia (Eds.) (Lecture Notes in Computer Science","volume":"192","author":"Aditya","unstructured":"Aditya V. Thakur and Thomas W. Reps. 2012. A Method for Symbolic Computation of Abstract Operations. In Computer Aided Verification - 24th International Conference , CAV 2012, Berkeley, CA, USA, July 7-13, 2012 Proceedings, P. Madhusudan and Sanjit A. Seshia (Eds.) (Lecture Notes in Computer Science , Vol. 7358). Springer, 174\u2013 192 . Aditya V. Thakur and Thomas W. Reps. 2012. A Method for Symbolic Computation of Abstract Operations. In Computer Aided Verification - 24th International Conference, CAV 2012, Berkeley, CA, USA, July 7-13, 2012 Proceedings, P. Madhusudan and Sanjit A. Seshia (Eds.) (Lecture Notes in Computer Science, Vol. 7358). Springer, 174\u2013192."},{"key":"e_1_2_2_96_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89884-1_23"},{"key":"e_1_2_2_97_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-012-0156-2"},{"key":"e_1_2_2_98_1","doi-asserted-by":"publisher","DOI":"10.1145\/2463209.2488880"},{"key":"e_1_2_2_99_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24730-2_39"},{"key":"e_1_2_2_100_1","first-page":"46","volume-title":"Proceedings of the 27th USENIX Conference on Security Symposium (SEC\u201918)","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 Proceedings of the 27th USENIX Conference on Security Symposium (SEC\u201918) . USENIX Association, Berkeley, CA, USA. 745\u2013761. isbn:978-1-93 1971- 46 - 41 Insu Yun, Sangho Lee, Meng Xu, Yeongjin Jang, and Taesoo Kim. 2018. QSYM : A Practical Concolic Execution Engine Tailored for Hybrid Fuzzing. In Proceedings of the 27th USENIX Conference on Security Symposium (SEC\u201918). USENIX Association, Berkeley, CA, USA. 745\u2013761. isbn:978-1-931971-46-1"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3485495","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3485495","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T20:18:40Z","timestamp":1750191520000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3485495"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,10,15]]},"references-count":100,"journal-issue":{"issue":"OOPSLA","published-print":{"date-parts":[[2021,10,20]]}},"alternative-id":["10.1145\/3485495"],"URL":"https:\/\/doi.org\/10.1145\/3485495","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,10,15]]},"assertion":[{"value":"2021-10-15","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}