{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T20:01:57Z","timestamp":1762459317180,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":40,"publisher":"ACM","license":[{"start":{"date-parts":[[2015,6,24]],"date-time":"2015-06-24T00:00:00Z","timestamp":1435104000000},"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":[[2015,6,24]]},"DOI":"10.1145\/2755996.2756636","type":"proceedings-article","created":{"date-parts":[[2015,6,25]],"date-time":"2015-06-25T14:43:22Z","timestamp":1435243402000},"page":"1-6","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":18,"title":["Building Bridges between Symbolic Computation and Satisfiability Checking"],"prefix":"10.1145","author":[{"given":"Erika","family":"Abraham","sequence":"first","affiliation":[{"name":"RWTH Aachen University, Aachen, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2015,6,24]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.5555\/2032305.2032319"},{"key":"e_1_3_2_1_3_1","series-title":"Frontiers in Artificial Intelligence and Applications","first-page":"825","volume-title":"Handbook of Satisfiability","author":"Barrett C.","year":"2009","unstructured":"C. Barrett, R. Sebastiani, S. A. Seshia, and C. Tinelli. Satisfiability modulo theories. In Handbook of Satisfiability, volume 185 of Frontiers in Artificial Intelligence and Applications, chapter 26, pages 825--885. IOS Press, 2009."},{"key":"e_1_3_2_1_4_1","volume-title":"The satisfiability modulo theories library (SMT-LIB). www.SMT-LIB.org","author":"Barrett C.","year":"2010","unstructured":"C. Barrett, A. Stump, and C. Tinelli. The satisfiability modulo theories library (SMT-LIB). www.SMT-LIB.org, 2010."},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.5555\/1197095"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.5555\/1550723"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31365-3_8"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02959-2_23"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02959-2_12"},{"key":"e_1_3_2_1_10_1","volume-title":"Linear integer arithmetic revisited. CoRR, abs\/1503.02948","author":"Bromberger M.","year":"2015","unstructured":"M. Bromberger, T. Sturm, and C. Weidenbach. Linear integer arithmetic revisited. CoRR, abs\/1503.02948, 2015. Accepted at CADE-25."},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/968708.968710"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-12002-2_12"},{"key":"e_1_3_2_1_13_1","unstructured":"carl. Project homepage.carlhomepage."},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-36742-7_7"},{"key":"e_1_3_2_1_15_1","series-title":"EPiC Series","first-page":"88","volume-title":"Proc. SMT","author":"Codish M.","year":"2013","unstructured":"M. Codish, Y. Fekete, C. Fuhs, J. Giesl, and J. Waldmann. Exotic semi-ring constraints. In Proc. SMT, volume 20 of EPiC Series, pages 88--97. EasyChair, 2013."},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.5555\/646589.697342"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1109\/SYNASC.2013.29"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.5555\/2034214.2034245"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31612-8_35"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/368273.368557"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/321033.321034"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38574-2_12"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.5555\/2554473.2554475"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792734.1792766"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02658-4_20"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.2307\/1910129"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/261320.261324"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/11817963_11"},{"key":"e_1_3_2_1_29_1","volume-title":"Efficient solving of large non-linear arithmetic constraint systems with complex Boolean structure. Journal on Satisfiability, Boolean Modeling and Computation, 1(3--4):209--236","author":"Fr\u00e4nzle M.","year":"2007","unstructured":"M. Fr\u00e4nzle, C. Herde, T. Teige, S. Ratschan, and T. Schubert. Efficient solving of large non-linear arithmetic constraint systems with complex Boolean structure. Journal on Satisfiability, Boolean Modeling and Computation, 1(3--4):209--236, 2007."},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.5555\/1998496.1998514"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31365-3_27"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-40663-8_18"},{"key":"e_1_3_2_1_34_1","first-page":"1093","article-title":"Polynomial algorithm for linear programming","volume":"244","author":"Khaciyan L. C.","year":"1979","unstructured":"L. C. Khaciyan. Polynomial algorithm for linear programming. Soviet Doklady, 244:1093--1096, 1979. Typed translation.","journal-title":"Soviet Doklady"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.5555\/1391237"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38574-2_13"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1109\/12.769433"},{"key":"e_1_3_2_1_38_1","first-page":"4","article-title":"The Omega test: A fast and practical integer programming algorithm for dependence analysis","volume":"8","author":"Pugh W.","year":"1992","unstructured":"W. Pugh. The Omega test: A fast and practical integer programming algorithm for dependence analysis. Communications of the ACM, 8:4--13, 1992.","journal-title":"Communications of the ACM"},{"key":"e_1_3_2_1_39_1","first-page":"231","volume-title":"Proc. MBMV","author":"Scheibler K.","year":"2013","unstructured":"K. Scheibler, S. Kupferschmid, and B. Becker. Recent improvements in the SMT solver iSAT. In Proc. MBMV, pages 231--241. Institut f\u00fcr Angewandte Mikroelektronik und Datentechnik, Fakult\u00e4t f\u00fcr Informatik und Elektrotechnik, Universit\u00e4t Rostock, 2013."},{"issue":"2","key":"e_1_3_2_1_40_1","first-page":"85","article-title":"Quantifier elimination for real algebra -- The quadratic case and beyond. Applicable Algebra in Engineering","volume":"8","author":"Weispfenning V.","year":"1997","unstructured":"V. Weispfenning. Quantifier elimination for real algebra -- The quadratic case and beyond. Applicable Algebra in Engineering, Communication and Computing, 8(2):85--101, 1997.","journal-title":"Communication and Computing"},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-7091-9459-1_20"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.5555\/1939141.1939168"}],"event":{"name":"ISSAC'15: International Symposium on Symbolic and Algebraic Computation","sponsor":["SIGSAM ACM Special Interest Group on Symbolic and Algebraic Manipulation"],"location":"Bath United Kingdom","acronym":"ISSAC'15"},"container-title":["Proceedings of the 2015 ACM International Symposium on Symbolic and Algebraic Computation"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2755996.2756636","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2755996.2756636","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T07:00:31Z","timestamp":1750230031000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2755996.2756636"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,6,24]]},"references-count":40,"alternative-id":["10.1145\/2755996.2756636","10.1145\/2755996"],"URL":"https:\/\/doi.org\/10.1145\/2755996.2756636","relation":{},"subject":[],"published":{"date-parts":[[2015,6,24]]},"assertion":[{"value":"2015-06-24","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}