{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,13]],"date-time":"2026-05-13T02:37:01Z","timestamp":1778639821955,"version":"3.51.4"},"publisher-location":"Cham","reference-count":20,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030010898","type":"print"},{"value":"9783030010904","type":"electronic"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-030-01090-4_26","type":"book-chapter","created":{"date-parts":[[2018,9,29]],"date-time":"2018-09-29T11:23:23Z","timestamp":1538220203000},"page":"441-457","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["Bounded Synthesis of Reactive Programs"],"prefix":"10.1007","author":[{"given":"Carsten","family":"Gerstacker","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Felix","family":"Klein","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bernd","family":"Finkbeiner","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,9,30]]},"reference":[{"issue":"4","key":"26_CR1","doi-asserted-by":"publisher","first-page":"289","DOI":"10.2307\/2271310","volume":"28","author":"A Church","year":"1963","unstructured":"Church, A.: Application of recursive arithmetic to the problem of circuit synthesis. J. Symb. Log. 28(4), 289\u2013290 (1963)","journal-title":"J. Symb. Log."},{"key":"26_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"258","DOI":"10.1007\/978-3-540-73368-3_29","volume-title":"Computer Aided Verification","author":"B Jobstmann","year":"2007","unstructured":"Jobstmann, B., Galler, S., Weiglhofer, M., Bloem, R.: Anzu: a tool for property synthesis. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 258\u2013262. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-73368-3_29"},{"key":"26_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"272","DOI":"10.1007\/978-3-642-19835-9_25","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R Ehlers","year":"2011","unstructured":"Ehlers, R.: Unbeast: symbolic bounded synthesis. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 272\u2013275. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-19835-9_25"},{"key":"26_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"652","DOI":"10.1007\/978-3-642-31424-7_45","volume-title":"Computer Aided Verification","author":"A Bohy","year":"2012","unstructured":"Bohy, A., Bruy\u00e8re, V., Filiot, E., Jin, N., Raskin, J.-F.: Acacia+, a tool for LTL synthesis. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 652\u2013657. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31424-7_45"},{"key":"26_CR5","doi-asserted-by":"crossref","unstructured":"Faymonville, P., Finkbeiner, B., Tentrup, L.: BoSy: an experimentation framework for bounded synthesis. [20] 325\u2013332","DOI":"10.1007\/978-3-319-63390-9_17"},{"key":"26_CR6","doi-asserted-by":"crossref","unstructured":"Bloem, R., Galler, S.J., Jobstmann, B., Piterman, N., Pnueli, A., Weiglhofer, M., et al.: Interactive presentation: automatic hardware synthesis from specifications: a case study. In: Lauwereins, R., Madsen, J. (eds.) DATE, pp. 1188\u20131193. Nice, France, EDA Consortium, San Jose, CA, USA (2007)","DOI":"10.1109\/DATE.2007.364456"},{"issue":"5\u20136","key":"26_CR7","doi-asserted-by":"publisher","first-page":"519","DOI":"10.1007\/s10009-012-0228-z","volume":"15","author":"B Finkbeiner","year":"2013","unstructured":"Finkbeiner, B., Schewe, S.: Bounded synthesis. STTT 15(5\u20136), 519\u2013539 (2013)","journal-title":"STTT"},{"key":"26_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"118","DOI":"10.1007\/978-3-319-41528-4_7","volume-title":"Computer Aided Verification","author":"B Finkbeiner","year":"2016","unstructured":"Finkbeiner, B., Klein, F.: Bounded cycle synthesis. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9779, pp. 118\u2013135. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-41528-4_7"},{"key":"26_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"354","DOI":"10.1007\/978-3-662-54577-5_20","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"P Faymonville","year":"2017","unstructured":"Faymonville, P., Finkbeiner, B., Rabe, M.N., Tentrup, L.: Encodings of bounded synthesis. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10205, pp. 354\u2013370. Springer, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-662-54577-5_20"},{"key":"26_CR10","unstructured":"Alur, R., et al.: Syntax-guided synthesis. In: FMCAD, pp. 1\u20138. Portland, OR, USA, IEEE (2013)"},{"key":"26_CR11","doi-asserted-by":"crossref","unstructured":"Gulwani, S.: Automating string processing in spreadsheets using input-output examples. In: Ball, T., Sagiv, M. (eds.) POPL, pp. 317\u2013330. Austin, TX, USA, ACM (2011)","DOI":"10.1145\/1925844.1926423"},{"key":"26_CR12","doi-asserted-by":"crossref","unstructured":"Osera, P., Zdancewic, S.: Type-and-example-directed program synthesis. In: Grove, D., Blackburn, S. (eds.) PLDI, pp. 619\u2013630. Portland, OR, USA, ACM (2015)","DOI":"10.1145\/2813885.2738007"},{"issue":"5\u20136","key":"26_CR13","doi-asserted-by":"publisher","first-page":"475","DOI":"10.1007\/s10009-012-0249-7","volume":"15","author":"A Solar-Lezama","year":"2013","unstructured":"Solar-Lezama, A.: Program sketching. STTT 15(5\u20136), 475\u2013495 (2013)","journal-title":"STTT"},{"issue":"5\u20136","key":"26_CR14","doi-asserted-by":"publisher","first-page":"413","DOI":"10.1007\/s10009-012-0232-3","volume":"15","author":"MT Vechev","year":"2013","unstructured":"Vechev, M.T., Yahav, E., Yorsh, G.: Abstraction-guided synthesis of synchronization. STTT 15(5\u20136), 413\u2013431 (2013)","journal-title":"STTT"},{"key":"26_CR15","unstructured":"Madhusudan, P.: Synthesizing reactive programs. In: Bezem, M., (ed.) CSL, Bergen, Norway. Volume 12 of LIPIcs, pp. 428\u2013442. Schloss Dagstuhl (2011)"},{"issue":"1","key":"26_CR16","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1006\/inco.1994.1092","volume":"115","author":"MY Vardi","year":"1994","unstructured":"Vardi, M.Y., Wolper, P.: Reasoning about infinite computations. Inf. Comput. 115(1), 1\u201337 (1994)","journal-title":"Inf. Comput."},{"key":"26_CR17","doi-asserted-by":"crossref","unstructured":"Gerstacker, C.: Bounded Synthesis of Reactive Programs, Bachelor\u2019s Thesis (2017)","DOI":"10.1007\/978-3-030-01090-4_26"},{"key":"26_CR18","doi-asserted-by":"crossref","unstructured":"Gerstacker, C., Klein, F., Finkbeiner, B.: Bounded synthesis of reactive programs. CoRR 1807.09047 (2018)","DOI":"10.1007\/978-3-030-01090-4_26"},{"key":"26_CR19","doi-asserted-by":"crossref","unstructured":"Khalimov, A., Bloem, R.: Bounded Synthesis for Streett, Rabin, and CTL$$^{*}$$\u2217. [20] 333\u2013352","DOI":"10.1007\/978-3-319-63390-9_18"},{"key":"26_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63390-9","volume-title":"Computer Aided Verification","year":"2017","unstructured":"Majumdar, R., Kun\u010dak, V. (eds.): CAV 2017. LNCS, vol. 10427. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63390-9"}],"container-title":["Lecture Notes in Computer Science","Automated Technology for Verification and Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-01090-4_26","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,11]],"date-time":"2020-11-11T06:35:32Z","timestamp":1605076532000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-01090-4_26"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783030010898","9783030010904"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-01090-4_26","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018]]},"assertion":[{"value":"ATVA","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Automated Technology for Verification and Analysis","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Los Angeles, CA","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"USA","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2018","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7 October 2018","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"10 October 2018","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"16","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"atva2018","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/atva-conference.org\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}