{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:48:58Z","timestamp":1750308538083,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":21,"publisher":"ACM","license":[{"start":{"date-parts":[[2015,6,13]],"date-time":"2015-06-13T00:00:00Z","timestamp":1434153600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["IMPRO"],"award-info":[{"award-number":["IMPRO"]}],"id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001711","name":"Schweizerische Nationalfonds zur F\u00f6rderung der Wissenschaftlichen Forschung","doi-asserted-by":"publisher","award":["200020_159949"],"award-info":[{"award-number":["200020_159949"]}],"id":[{"id":"10.13039\/501100001711","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2015,6,13]]},"DOI":"10.1145\/2774975.2774980","type":"proceedings-article","created":{"date-parts":[[2015,6,3]],"date-time":"2015-06-03T15:35:56Z","timestamp":1433345756000},"page":"35-40","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Sound reasoning about integral data types with a reusable SMT solver interface"],"prefix":"10.1145","author":[{"given":"R\u00e9gis","family":"Blanc","sequence":"first","affiliation":[{"name":"EPFL, Switzerland"}]},{"given":"Viktor","family":"Kuncak","sequence":"additional","affiliation":[{"name":"EPFL, Switzerland"}]}],"member":"320","published-online":{"date-parts":[[2015,6,13]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.5555\/2032305.2032319"},{"key":"e_1_3_2_1_2_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 . 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_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/2489837.2489838"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/128861.128862"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00768-2_16"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535874"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792734.1792766"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_8"},{"key":"e_1_3_2_1_10_1","series-title":"Lecture Notes in Computer Science","volume-title":"Computer Aided Verification","author":"Ganzinger H.","year":"2004","unstructured":"H. Ganzinger , G. Hagen , R. Nieuwenhuis , A. Oliveras , and C. Tinelli . DPLL(T): Fast Decision Procedures . In R. Alur and D. Peled, editors, Computer Aided Verification , volume 3114 of Lecture Notes in Computer Science . Springer Berlin Heidelberg , 2004 . H. Ganzinger, G. Hagen, R. Nieuwenhuis, A. Oliveras, and C. Tinelli. DPLL(T): Fast Decision Procedures. In R. Alur and D. Peled, editors, Computer Aided Verification, volume 3114 of Lecture Notes in Computer Science. Springer Berlin Heidelberg, 2004."},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02658-4_53"},{"key":"e_1_3_2_1_12_1","volume-title":"Computer-aided reasoning: an approach","author":"Kaufmann M.","year":"2000","unstructured":"M. Kaufmann , J. S. Moore , and P. Manolios . Computer-aided reasoning: an approach . Kluwer Academic Publishers , 2000 . M. Kaufmann, J. S. Moore, and P. Manolios. Computer-aided reasoning: an approach. Kluwer Academic Publishers, 2000."},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21668-3_13"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2509136.2509555"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-40787-1_1"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.5555\/1939141.1939161"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0030541","volume-title":"Isabelle: A generic theorem prover","author":"Paulson L. C.","year":"1994","unstructured":"L. C. Paulson . Isabelle: A generic theorem prover , volume 828 . Springer Science & amp; Business Media, 1994 . L. C. Paulson. Isabelle: A generic theorem prover, volume 828. Springer Science & Business Media, 1994."},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706325"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.5555\/2041552.2041575"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2774975.2774978"},{"key":"e_1_3_2_1_21_1","volume-title":"Springer","author":"Walther C.","year":"2003","unstructured":"C. Walther and S. Schweitzer . About verifun. In Automated Deduction\u2013CADE-19, pages 322\u2013327 . Springer , 2003 . C. Walther and S. Schweitzer. About verifun. In Automated Deduction\u2013CADE-19, pages 322\u2013327. Springer, 2003."},{"key":"e_1_3_2_1_22_1","volume-title":"Inc.","author":"Warren H. S.","year":"2002","unstructured":"H. S. Warren . Hacker\u2019s Delight . Addison-Wesley Longman Publishing Co ., Inc. , Boston, MA, USA , 2002 . H. S. Warren. Hacker\u2019s Delight. Addison-Wesley Longman Publishing Co., Inc., Boston, MA, USA, 2002."}],"event":{"name":"PLDI '15: ACM SIGPLAN Conference on Programming Language Design and Implementation","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"],"location":"Portland OR USA","acronym":"PLDI '15"},"container-title":["Proceedings of the 6th ACM SIGPLAN Symposium on Scala"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2774975.2774980","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2774975.2774980","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T18:56:05Z","timestamp":1750272965000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2774975.2774980"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,6,13]]},"references-count":21,"alternative-id":["10.1145\/2774975.2774980","10.1145\/2774975"],"URL":"https:\/\/doi.org\/10.1145\/2774975.2774980","relation":{},"subject":[],"published":{"date-parts":[[2015,6,13]]},"assertion":[{"value":"2015-06-13","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}