乐胖代购免代理版

{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,10,30]],"date-time":"2024-10-30T22:23:51Z","timestamp":1730327031000,"version":"3.28.0"},"publisher-location":"New York, NY, USA","reference-count":49,"publisher":"ACM","funder":[{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["61972384,62132020"],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100004739","name":"Youth Innovation Promotion Association of the Chinese Academy of Sciences","doi-asserted-by":"publisher","award":["Y202034"],"id":[{"id":"10.13039\/501100004739","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2023,7,12]]},"DOI":"10.1145\/3597926.3598034","type":"proceedings-article","created":{"date-parts":[[2023,7,13]],"date-time":"2023-07-13T20:12:53Z","timestamp":1689279173000},"page":"14-25","update-policy":"http:\/\/dx.doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Improving Bit-Blasting for Nonlinear Integer Constraints"],"prefix":"10.1145","author":[{"given":"Fuqi","family":"Jia","sequence":"first","affiliation":[{"name":"Institute of Software at Chinese Academy of Sciences, China \/ University of Chinese Academy of Sciences, China"}]},{"given":"Rui","family":"Han","sequence":"additional","affiliation":[{"name":"Institute of Software at Chinese Academy of Sciences, China \/ University of Chinese Academy of Sciences, China"}]},{"given":"Pei","family":"Huang","sequence":"additional","affiliation":[{"name":"Stanford University, USA"}]},{"given":"Minghao","family":"Liu","sequence":"additional","affiliation":[{"name":"Institute of Software at Chinese Academy of Sciences, China \/ University of Chinese Academy of Sciences, China"}]},{"given":"Feifei","family":"Ma","sequence":"additional","affiliation":[{"name":"Institute of Software at Chinese Academy of Sciences, China \/ University of Chinese Academy of Sciences, China"}]},{"given":"Jian","family":"Zhang","sequence":"additional","affiliation":[{"name":"Institute of Software at Chinese Academy of Sciences, China \/ University of Chinese Academy of Sciences, China"}]}],"member":"320","published-online":{"date-parts":[[2023,7,13]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1137\/0213054"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3182657"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99524-9_24"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/11513988_4"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.21236\/ADA360973"},{"key":"e_1_3_2_1_7_1","first-page":"51","volume-title":"Proc. of SAT Competition 2020-Solver and Benchmark Descriptions, Tomas Balyo, Nils Froleyks, Marijn Heule, Markus Iser, Matti J\u00e4rvisalo, and Martin Suda (Eds.)","volume":"1","author":"Biere Armin","year":"2020","unstructured":"Armin Biere , Katalin Fazekas , Mathias Fleury , and Maximillian Heisinger . 2020 . CaDiCaL, Kissat, Paracooba, Plingeling and Treengeling Entering the SAT Competition 2020 . In Proc. of SAT Competition 2020-Solver and Benchmark Descriptions, Tomas Balyo, Nils Froleyks, Marijn Heule, Markus Iser, Matti J\u00e4rvisalo, and Martin Suda (Eds.) , Vol. B-2020- 1 . 51 - 53 . Armin Biere, Katalin Fazekas, Mathias Fleury, and Maximillian Heisinger. 2020. CaDiCaL, Kissat, Paracooba, Plingeling and Treengeling Entering the SAT Competition 2020. In Proc. of SAT Competition 2020-Solver and Benchmark Descriptions, Tomas Balyo, Nils Froleyks, Marijn Heule, Markus Iser, Matti J\u00e4rvisalo, and Martin Suda (Eds.), Vol. B-2020-1. 51-53."},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3340923"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02959-2_23"},{"key":"e_1_3_2_1_10_1","first-page":"23","volume-title":"Further Steps Down The Wrong Path: Improving the BitBlasting of Multiplication. In CAV","volume":"2908","author":"Brain Martin","year":"2021","unstructured":"Martin Brain . 2021 . Further Steps Down The Wrong Path: Improving the BitBlasting of Multiplication. In CAV 2021, Alexander Nadel and Aina Niemetz (Eds.) , Vol. 2908 . 23 - 31 . Martin Brain. 2021. Further Steps Down The Wrong Path: Improving the BitBlasting of Multiplication. In CAV 2021, Alexander Nadel and Aina Niemetz (Eds.), Vol. 2908. 23-31."},{"key":"e_1_3_2_1_11_1","first-page":"174","volume-title":"Boolector: An Eficient SMT Solver for Bit-Vectors and Arrays. In TACAS","volume":"5505","author":"Brummayer Robert","year":"2009","unstructured":"Robert Brummayer and Armin Biere . 2009 . Boolector: An Eficient SMT Solver for Bit-Vectors and Arrays. In TACAS 2009, Stefan Kowalewski and Anna Philippou (Eds.) , Vol. 5505 . 174 - 177 . Robert Brummayer and Armin Biere. 2009. Boolector: An Eficient SMT Solver for Bit-Vectors and Arrays. In TACAS 2009, Stefan Kowalewski and Anna Philippou (Eds.), Vol. 5505. 174-177."},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73368-3_54"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54577-5_4"},{"key":"e_1_3_2_1_14_1","first-page":"383","volume-title":"Experimenting on Solving Nonlinear Integer Arithmetic with Incremental Linearization. In SAT","volume":"10929","author":"Cimatti Alessandro","year":"2018","unstructured":"Alessandro Cimatti , Alberto Griggio , Ahmed Irfan , Marco Roveri , and Roberto Sebastiani . 2018 . Experimenting on Solving Nonlinear Integer Arithmetic with Incremental Linearization. In SAT 2018, Olaf Beyersdorf and Christoph M. Wintersteiger (Eds.) , Vol. 10929 . 383 - 398 . Alessandro Cimatti, Alberto Griggio, Ahmed Irfan, Marco Roveri, and Roberto Sebastiani. 2018. Experimenting on Solving Nonlinear Integer Arithmetic with Incremental Linearization. In SAT 2018, Olaf Beyersdorf and Christoph M. Wintersteiger (Eds.), Vol. 10929. 383-398."},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-36742-7_7"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/11513988_30"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-45237-7_24"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_3_2_1_19_1","volume-title":"LPAR 2008 Workshops (CEUR Workshop Proceedings","volume":"418","author":"de Moura Leonardo Mendon\u00e7a","unstructured":"Leonardo Mendon\u00e7a de Moura and Nikolaj S. Bj\u00f8rner . 2008. Proofs and Refutations, and Z3 . In LPAR 2008 Workshops (CEUR Workshop Proceedings , Vol. 418 ), Piotr Rudnicki, Geof Sutclife, Boris Konev, Renate A. Schmidt, and Stephan Schulz (Eds.). CEUR-WS.org. http:\/\/ceur-ws. org\/ Vol-418 \/paper10.pdf Leonardo Mendon\u00e7a de Moura and Nikolaj S. Bj\u00f8rner. 2008. Proofs and Refutations, and Z3. In LPAR 2008 Workshops (CEUR Workshop Proceedings, Vol. 418 ), Piotr Rudnicki, Geof Sutclife, Boris Konev, Renate A. Schmidt, and Stephan Schulz (Eds.). CEUR-WS.org. http:\/\/ceur-ws. org\/ Vol-418 \/paper10.pdf"},{"key":"e_1_3_2_1_20_1","first-page":"15","volume-title":"Maria Paola Bonacina and Mark E. Stickel (Eds.)","volume":"7788","author":"de Moura Leonardo Mendon\u00e7a","year":"2013","unstructured":"Leonardo Mendon\u00e7a de Moura and Grant Olney Passmore . 2013 . The Strategy Challenge in SMT Solving. In Automated Reasoning and Mathematics-Essays in Memory of William W. McCune , Maria Paola Bonacina and Mark E. Stickel (Eds.) , Vol. 7788 . 15 - 44 . Leonardo Mendon\u00e7a de Moura and Grant Olney Passmore. 2013. The Strategy Challenge in SMT Solving. In Automated Reasoning and Mathematics-Essays in Memory of William W. McCune, Maria Paola Bonacina and Mark E. Stickel (Eds.), Vol. 7788. 15-44."},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2642937.2642951"},{"key":"e_1_3_2_1_22_1","volume-title":"ASE","author":"Dustmann Oscar Soria","year":"2018","unstructured":"Oscar Soria Dustmann , Klaus Wehrle , and Cristian Cadar . 2018 . PARTI: a multiinterval theory solver for symbolic execution . In ASE 2018, Marianne Huchard, Christian K\u00e4stner, and Gordon Fraser (Eds.). 430-440. Oscar Soria Dustmann, Klaus Wehrle, and Cristian Cadar. 2018. PARTI: a multiinterval theory solver for symbolic execution. In ASE 2018, Marianne Huchard, Christian K\u00e4stner, and Gordon Fraser (Eds.). 430-440."},{"key":"e_1_3_2_1_23_1","first-page":"737","volume-title":"CAV","volume":"8559","author":"Dutertre Bruno","year":"2014","unstructured":"Bruno Dutertre . 2014 . Yices 2.2 . In CAV 2014, Armin Biere and Roderick Bloem (Eds.) , Vol. 8559 . 737 - 744 . Bruno Dutertre. 2014. Yices 2.2. In CAV 2014, Armin Biere and Roderick Bloem (Eds.), Vol. 8559. 737-744."},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-007-9087-9"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.3233\/sat190012"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-72788-0_33"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25540-4_19"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02846-5_22"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-016-9388-y"},{"key":"e_1_3_2_1_30_1","first-page":"184","volume-title":"Proving Termination of Programs Automatically with AProVE. In IJCAR","volume":"8562","author":"Giesl J\u00fcrgen","year":"2014","unstructured":"J\u00fcrgen Giesl , Marc Brockschmidt , Fabian Emmes , Florian Frohn , Carsten Fuhs , Carsten Otto , Martin Pl\u00fccker , Peter Schneider-Kamp , Thomas Str\u00f6der , Stephanie Swiderski , and Ren\u00e9 Thiemann . 2014 . Proving Termination of Programs Automatically with AProVE. In IJCAR 2014, St\u00e9phane Demri, Deepak Kapur, and Christoph Weidenbach (Eds.) , Vol. 8562 . 184 - 191 . J\u00fcrgen Giesl, Marc Brockschmidt, Fabian Emmes, Florian Frohn, Carsten Fuhs, Carsten Otto, Martin Pl\u00fccker, Peter Schneider-Kamp, Thomas Str\u00f6der, Stephanie Swiderski, and Ren\u00e9 Thiemann. 2014. Proving Termination of Programs Automatically with AProVE. In IJCAR 2014, St\u00e9phane Demri, Deepak Kapur, and Christoph Weidenbach (Eds.), Vol. 8562. 184-191."},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_45"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46681-0_43"},{"key":"e_1_3_2_1_33_1","first-page":"330","volume-title":"Solving Nonlinear Integer Arithmetic with MCSAT. In VMCAI","volume":"10145","author":"Jovanovic Dejan","year":"2017","unstructured":"Dejan Jovanovic . 2017 . Solving Nonlinear Integer Arithmetic with MCSAT. In VMCAI 2017, Ahmed Bouajjani and David Monniaux (Eds.) , Vol. 10145 . 330 - 346 . Dejan Jovanovic. 2017. Solving Nonlinear Integer Arithmetic with MCSAT. In VMCAI 2017, Ahmed Bouajjani and David Monniaux (Eds.), Vol. 10145. 330-346."},{"key":"e_1_3_2_1_34_1","first-page":"339","volume-title":"Solving Non-linear Arithmetic. In IJCAR","volume":"7364","author":"Jovanovic Dejan","year":"2012","unstructured":"Dejan Jovanovic and Leonardo Mendon\u00e7a de Moura . 2012 . Solving Non-linear Arithmetic. In IJCAR 2012, Bernhard Gramlich, Dale Miller, and Uli Sattler (Eds.) , Vol. 7364 . 339 - 354 . Dejan Jovanovic and Leonardo Mendon\u00e7a de Moura. 2012. Solving Non-linear Arithmetic. In IJCAR 2012, Bernhard Gramlich, Dale Miller, and Uli Sattler (Eds.), Vol. 7364. 339-354."},{"key":"e_1_3_2_1_35_1","first-page":"28","volume-title":"CAV","volume":"1889","author":"Jovanovic Dejan","year":"2017","unstructured":"Dejan Jovanovic and Bruno Dutertre . 2017 . LibPoly: A Library for Reasoning about Polynomials . In CAV 2017, Martin Brain and Liana Hadarean (Eds.) , Vol. 1889 . 28 - 39 . Dejan Jovanovic and Bruno Dutertre. 2017. LibPoly: A Library for Reasoning about Polynomials. In CAV 2017, Martin Brain and Liana Hadarean (Eds.), Vol. 1889. 28-39."},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.23919\/DATE48585"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-45641-6_21"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-50497-0_6"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89963-3_16"},{"key":"e_1_3_2_1_40_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 ). \t\t\t\t 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 )."},{"volume-title":"Hilbert's tenth problem","author":"Matiyasevich Y. V.","key":"e_1_3_2_1_41_1","unstructured":"Y. V. Matiyasevich . 1993. Hilbert's tenth problem . MIT press . Y. V. Matiyasevich. 1993. Hilbert's tenth problem. MIT press."},{"key":"e_1_3_2_1_42_1","volume-title":"Bitwuzla at the SMT-COMP","author":"Niemetz Aina","year":"2020","unstructured":"Aina Niemetz and Mathias Preiner . 2020. Bitwuzla at the SMT-COMP 2020 . CoRR abs\/ 2006.01621 ( 2020 ). Aina Niemetz and Mathias Preiner. 2020. Bitwuzla at the SMT-COMP 2020. CoRR abs\/ 2006.01621 ( 2020 )."},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/2001420.2001425"},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-40648-0_8"},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_31"},{"key":"e_1_3_2_1_46_1","volume-title":"Proc. PDPAR'05 144","author":"Singerman Eli","year":"2005","unstructured":"Eli Singerman . 2005 . Challenges in making decision procedures applicable to industry . Proc. PDPAR'05 144 , 2 ( 2005 ). Eli Singerman. 2005. Challenges in making decision procedures applicable to industry. Proc. PDPAR'05 144, 2 ( 2005 )."},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-012-0163-3"},{"volume-title":"SMT@IJCAR 2016 (CEUR Workshop Proceedings","author":"Weber Tjark","key":"e_1_3_2_1_48_1","unstructured":"Tjark Weber . 2016. Scrambling and Descrambling SMT-LIB Benchmarks . In SMT@IJCAR 2016 (CEUR Workshop Proceedings , Vol. 1617 ). CEUR-WS.org, 31-40. http:\/\/ceur-ws. org\/ Vol- 1617 \/paper3.pdf Tjark Weber. 2016. Scrambling and Descrambling SMT-LIB Benchmarks. In SMT@IJCAR 2016 (CEUR Workshop Proceedings, Vol. 1617 ). CEUR-WS.org, 31-40. http:\/\/ceur-ws. org\/ Vol-1617 \/paper3.pdf"},{"key":"e_1_3_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/3395363.3397378"},{"key":"e_1_3_2_1_50_1","first-page":"481","volume-title":"Edmund M. Clarke and Andrei Voronkov (Eds.)","volume":"6355","author":"Zankl Harald","year":"2010","unstructured":"Harald Zankl and Aart Middeldorp . 2010 . Satisfiability of Non-linear (Ir)rational Arithmetic. In Logic for Programming, Artificial Intelligence, and Reasoning-16th International Conference, LPAR-16 , Edmund M. Clarke and Andrei Voronkov (Eds.) , Vol. 6355 . 481 - 500 . Harald Zankl and Aart Middeldorp. 2010. Satisfiability of Non-linear (Ir)rational Arithmetic. In Logic for Programming, Artificial Intelligence, and Reasoning-16th International Conference, LPAR-16, Edmund M. Clarke and Andrei Voronkov (Eds.), Vol. 6355. 481-500."}],"event":{"name":"ISSTA '23: 32nd ACM SIGSOFT International Symposium on Software Testing and Analysis","sponsor":["SIGSOFT ACM Special Interest Group on Software Engineering","AITO"],"location":"Seattle WA USA","acronym":"ISSTA '23"},"container-title":["Proceedings of the 32nd ACM SIGSOFT International Symposium on Software Testing and Analysis"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3597926.3598034","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,11,25]],"date-time":"2023-11-25T19:19:51Z","timestamp":1700939991000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3597926.3598034"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,7,12]]},"references-count":49,"alternative-id":["10.1145\/3597926.3598034","10.1145\/3597926"],"URL":"https:\/\/doi.org\/10.1145\/3597926.3598034","relation":{},"subject":[],"published":{"date-parts":[[2023,7,12]]},"assertion":[{"value":"2023-07-13","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}