{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,20]],"date-time":"2025-07-20T04:21:10Z","timestamp":1752985270610,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":63,"publisher":"ACM","license":[{"start":{"date-parts":[[2020,7,18]],"date-time":"2020-07-18T00:00:00Z","timestamp":1595030400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2020,7,18]]},"DOI":"10.1145\/3395363.3397378","type":"proceedings-article","created":{"date-parts":[[2020,7,13]],"date-time":"2020-07-13T21:44:18Z","timestamp":1594676658000},"page":"38-50","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":11,"title":["Fast bit-vector satisfiability"],"prefix":"10.1145","author":[{"given":"Peisen","family":"Yao","sequence":"first","affiliation":[{"name":"Hong Kong University of Science and Technology, China"}]},{"given":"Qingkai","family":"Shi","sequence":"additional","affiliation":[{"name":"Hong Kong University of Science and Technology, China"}]},{"given":"Heqing","family":"Huang","sequence":"additional","affiliation":[{"name":"Hong Kong University of Science and Technology, China"}]},{"given":"Charles","family":"Zhang","sequence":"additional","affiliation":[{"name":"Hong Kong University of Science and Technology, China"}]}],"member":"320","published-online":{"date-parts":[[2020,7,18]]},"reference":[{"doi-asserted-by":"publisher","key":"e_1_3_2_1_2_1","DOI":"10.5555\/2032305.2032319"},{"unstructured":"Clark Barrett Aaron Stump and Cesare Tinelli. 2010. The satisfiability modulo theories library (SMT-LIB). www. SMT-LIB. org 15 ( 2010 ) 18-52.  Clark Barrett Aaron Stump and Cesare Tinelli. 2010. The satisfiability modulo theories library (SMT-LIB). www. SMT-LIB. org 15 ( 2010 ) 18-52.","key":"e_1_3_2_1_3_1"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_4_1","DOI":"10.1145\/277044.277186"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_5_1","DOI":"10.5555\/647771.734410"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_6_1","DOI":"10.1016\/j.cagd.2010.04.004"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_7_1","DOI":"10.1145\/1595696.1595762"},{"volume-title":"Foundations of Artificial Intelligence.","author":"Benhamou Fr\u00e9d\u00e9ric","key":"e_1_3_2_1_8_1"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_9_1","DOI":"10.5555\/3168451.3168468"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_10_1","DOI":"10.5555\/1789854.1789858"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_11_1","DOI":"10.5555\/1550723"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_12_1","DOI":"10.1007\/978-3-319-24318-4_29"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_13_1","DOI":"10.1145\/3276514"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_14_1","DOI":"10.1109\/ICST.2012.91"},{"volume-title":"The calculus of computation: decision procedures with applications to verification","author":"Bradley Aaron R","key":"e_1_3_2_1_15_1"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_17_1","DOI":"10.1007\/978-3-540-73368-3_54"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_18_1","DOI":"10.5555\/1763507.1763544"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_19_1","DOI":"10.1145\/2786805.2803205"},{"key":"e_1_3_2_1_20_1","first-page":"209","volume-title":"Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation","author":"Cadar Cristian","year":"2008"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_21_1","DOI":"10.1145\/1180405.1180445"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_22_1","DOI":"10.1145\/3238147.3238218"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_23_1","DOI":"10.1007\/978-3-319-59776-8_1"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_24_1","DOI":"10.5555\/520033.858247"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_25_1","DOI":"10.1007\/978-3-642-36742-7_7"},{"volume-title":"Proceedings of the 13th International Conference on Computer Aided Verification (CAV '01)","author":"Copty Fady","first-page":"436","key":"e_1_3_2_1_26_1"},{"key":"e_1_3_2_1_27_1","first-page":"1092","volume-title":"Proceedings of the Twelfth National Conference on Artificial Intelligence (Vol. 2 )","author":"James","year":"1994"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_28_1","DOI":"10.5555\/647766.733602"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_29_1","DOI":"10.1007\/978-3-540-78800-3_24"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_30_1","DOI":"10.1109\/SP.2016.15"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_31_1","DOI":"10.1109\/ISSRE.2015.7381814"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_32_1","DOI":"10.1145\/3238147.3238179"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_33_1","DOI":"10.1007\/978-3-319-08867-9_49"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_35_1","DOI":"10.5555\/2887007.2887165"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_36_1","DOI":"10.1007\/978-3-540-73368-3_52"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_37_1","DOI":"10.1145\/2651360"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_38_1","DOI":"10.1145\/378239.379017"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_39_1","DOI":"10.1007\/978-3-319-08867-9_44"},{"key":"e_1_3_2_1_40_1","first-page":"772","volume-title":"Proceedings of the 2013 International Conference on Software Engineering (San Francisco, CA, USA) ( ICSE '13). IEEE Press","author":"Thien Nguyen Hoang Duong","year":"2013"},{"doi-asserted-by":"crossref","unstructured":"Aina Niemetz Mathias Preiner and Armin Biere. 2014 (published 2015 ). Boolector 2.0 system description. Journal on Satisfiability Boolean Modeling and Computation 9 ( 2014 (published 2015 )) 53-58.  Aina Niemetz Mathias Preiner and Armin Biere. 2014 (published 2015 ). Boolector 2.0 system description. Journal on Satisfiability Boolean Modeling and Computation 9 ( 2014 (published 2015 )) 53-58.","key":"e_1_3_2_1_41_1","DOI":"10.3233\/SAT190101"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_42_1","DOI":"10.1007\/s10703-017-0295-6"},{"volume-title":"Proceedings of DIFTS ( 2015 ), 1-10","year":"2015","author":"Niemetz Aina","key":"e_1_3_2_1_43_1"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_44_1","DOI":"10.1007\/978-3-642-39799-8_3"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_45_1","DOI":"10.1145\/3092703.3092728"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_46_1","DOI":"10.5555\/1782734.1782760"},{"doi-asserted-by":"crossref","unstructured":"Daniele Pretolani. 1996. Eficiency and stability of hypergraph SAT algorithms. DIMACS Series in Discrete Mathematics and Theoretical Computer Science 26 ( 1996 ) 479-498.  Daniele Pretolani. 1996. Eficiency and stability of hypergraph SAT algorithms. DIMACS Series in Discrete Mathematics and Theoretical Computer Science 26 ( 1996 ) 479-498.","key":"e_1_3_2_1_47_1","DOI":"10.1090\/dimacs\/026\/23"},{"volume-title":"SMT Workshop.","year":"2018","author":"Reynolds Andrew","key":"e_1_3_2_1_48_1"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_49_1","DOI":"10.1007\/978-3-319-63390-9_24"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_51_1","DOI":"10.1007\/11823230_2"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_52_1","DOI":"10.5555\/882506.885138"},{"doi-asserted-by":"crossref","unstructured":"Roberto Sebastiani. 2007. Lazy satisfiability modulo theories. Journal on Satisfiability Boolean Modeling and Computation 3 ( 2007 ) 141-224.  Roberto Sebastiani. 2007. Lazy satisfiability modulo theories. Journal on Satisfiability Boolean Modeling and Computation 3 ( 2007 ) 141-224.","key":"e_1_3_2_1_53_1","DOI":"10.3233\/SAT190034"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_54_1","DOI":"10.1145\/1081706.1081750"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_55_1","DOI":"10.1145\/3192366.3192418"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_56_1","DOI":"10.1109\/SP.2016.17"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_57_1","DOI":"10.1007\/10722167_36"},{"volume-title":"Proceedings of the 1996 IEEE\/ACM International Conference on Computer-aided Design (San Jose, California, USA) ( ICCAD '96). IEEE Computer Society","author":"Jo\u00e3o","first-page":"220","key":"e_1_3_2_1_58_1"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_59_1","DOI":"10.1109\/FMCAD.2016.7886678"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_60_1","DOI":"10.14722\/ndss.2016.23368"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_61_1","DOI":"10.1145\/2393596.2393665"},{"volume-title":"Overify: Optimizing Programs for Fast Verification. In 14th Workshop on Hot Topics in Operating Systems (HotOS XIV).","year":"2013","author":"Wagner Jonas","key":"e_1_3_2_1_62_1"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_63_1","DOI":"10.1145\/996566.996713"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_64_1","DOI":"10.1145\/1040305.1040334"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_65_1","DOI":"10.1109\/TASE.2013.11"},{"key":"e_1_3_2_1_66_1","first-page":"745","volume-title":"Proceedings of the 27th USENIX Conference on Security Symposium (Baltimore, MD, USA) ( SEC'18). USENIX Association","author":"Yun Insu","year":"2018"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_67_1","DOI":"10.1007\/978-3-319-40970-2_16"}],"event":{"sponsor":["SIGSOFT ACM Special Interest Group on Software Engineering"],"acronym":"ISSTA '20","name":"ISSTA '20: 29th ACM SIGSOFT International Symposium on Software Testing and Analysis","location":"Virtual Event USA"},"container-title":["Proceedings of the 29th ACM SIGSOFT International Symposium on Software Testing and Analysis"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3395363.3397378","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3395363.3397378","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T22:38:45Z","timestamp":1750199925000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3395363.3397378"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,7,18]]},"references-count":63,"alternative-id":["10.1145\/3395363.3397378","10.1145\/3395363"],"URL":"https:\/\/doi.org\/10.1145\/3395363.3397378","relation":{},"subject":[],"published":{"date-parts":[[2020,7,18]]},"assertion":[{"value":"2020-07-18","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}