{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T14:29:32Z","timestamp":1725892172920},"publisher-location":"Berlin, Heidelberg","reference-count":12,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642313646"},{"type":"electronic","value":"9783642313653"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-31365-3_39","type":"book-chapter","created":{"date-parts":[[2012,6,21]],"date-time":"2012-06-21T16:35:34Z","timestamp":1340296534000},"page":"499-513","source":"Crossref","is-referenced-by-count":7,"title":["Synthesis for Unbounded Bit-Vector Arithmetic"],"prefix":"10.1007","author":[{"given":"Andrej","family":"Spielmann","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Viktor","family":"Kuncak","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"3","key":"39_CR1","doi-asserted-by":"publisher","first-page":"911","DOI":"10.1016\/j.jcss.2011.08.007","volume":"78","author":"R. Bloem","year":"2012","unstructured":"Bloem, R., Jobstmann, B., Piterman, N., Pnueli, A., Sa\u2019ar, Y.: Synthesis of reactive(1) designs. J. Comput. Syst. Sci.\u00a078(3), 911\u2013938 (2012)","journal-title":"J. Comput. Syst. Sci."},{"issue":"295-311","key":"39_CR2","first-page":"5","volume":"138","author":"J. Buchi","year":"1969","unstructured":"Buchi, J., Landweber, L.: Solving sequential conditions by finite-state strategies. Transactions of the American Mathematical Society\u00a0138(295-311), 5 (1969)","journal-title":"Transactions of the American Mathematical Society"},{"key":"39_CR3","unstructured":"Gupta, A.: Inductive Boolean Function Manipulation: A Hardware Verification Methodology for Automatic Induction. PhD thesis, CMU (1994)"},{"key":"39_CR4","unstructured":"Hamza, J., Jobstmann, B., Kuncak, V.: Synthesis for regular specifications over unbounded domains. In: Formal Methods in Computer-Aided Design (FMCAD), pp. 101\u2013109. IEEE (2010)"},{"key":"39_CR5","doi-asserted-by":"crossref","unstructured":"Jobstmann, B., Bloem, R.: Optimizations for LTL synthesis. In: FMCAD (2006)","DOI":"10.1109\/FMCAD.2006.22"},{"key":"39_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"182","DOI":"10.1007\/3-540-44674-5_15","volume-title":"Implementation and Application of Automata","author":"N. Klarlund","year":"2001","unstructured":"Klarlund, N., M\u00f8ller, A., Schwartzbach, M.I.: MONA Implementation Secrets. In: Yu, S., P\u0103un, A. (eds.) CIAA 2000. LNCS, vol.\u00a02088, pp. 182\u2013194. Springer, Heidelberg (2001)"},{"key":"39_CR7","doi-asserted-by":"crossref","unstructured":"Kuncak, V., Mayer, M., Piskac, R., Suter, P.: Complete functional synthesis. In: ACM SIGPLAN Conf. Programming Language Design and Implementation, PLDI (2010)","DOI":"10.1145\/1806596.1806632"},{"key":"39_CR8","doi-asserted-by":"crossref","unstructured":"Rabin, M.: Automata on infinite objects and Church\u2019s problem. Regional Conference Series in Mathematics, vol.\u00a013. American Mathematical Society (1972)","DOI":"10.1090\/cbms\/013"},{"key":"39_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1007\/978-3-540-70889-6_5","volume-title":"Hardware and Software, Verification and Testing","author":"T. Schuele","year":"2007","unstructured":"Schuele, T., Schneider, K.: Verification of Data Paths Using Unbounded Integers: Automata Strike Back. In: Bin, E., Ziv, A., Ur, S. (eds.) HVC 2006. LNCS, vol.\u00a04383, pp. 65\u201380. Springer, Heidelberg (2007)"},{"key":"39_CR10","doi-asserted-by":"crossref","unstructured":"Spielmann, A., Kuncak, V.: On synthesis for unbounded bit-vector arithmetic. Technical Report EPFL-REPORT-174801, EPFL (2012)","DOI":"10.1007\/978-3-642-31365-3_39"},{"key":"39_CR11","doi-asserted-by":"crossref","unstructured":"Srivastava, S., Gulwani, S., Foster, J.S.: From program verification to program synthesis. In: POPL (2010)","DOI":"10.1145\/1706299.1706337"},{"issue":"6","key":"39_CR12","doi-asserted-by":"publisher","first-page":"753","DOI":"10.1145\/602220.602223","volume":"49","author":"L. Stockmeyer","year":"2002","unstructured":"Stockmeyer, L., Meyer, A.R.: Cosmological lower bound on the circuit complexity of a small problem in logic. J. ACM\u00a049(6), 753\u2013784 (2002)","journal-title":"J. ACM"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-31365-3_39.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,4]],"date-time":"2021-05-04T07:58:30Z","timestamp":1620115110000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-31365-3_39"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642313646","9783642313653"],"references-count":12,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-31365-3_39","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}