{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,7]],"date-time":"2026-10-07T22:29:45Z","timestamp":1791412185209,"version":"4.3.3"},"publisher-location":"Cham","reference-count":56,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030532901","type":"print"},{"value":"9783030532918","type":"electronic"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2020,7,14]],"date-time":"2020-07-14T00:00:00Z","timestamp":1594684800000},"content-version":"vor","delay-in-days":195,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2020]]},"DOI":"10.1007\/978-3-030-53291-8_32","type":"book-chapter","created":{"date-parts":[[2020,7,15]],"date-time":"2020-07-15T20:03:35Z","timestamp":1594843415000},"page":"634-657","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":11,"title":["Decidable Synthesis of Programs with Uninterpreted Functions"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-6710-9516","authenticated-orcid":false,"given":"Paul","family":"Krogmeier","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7610-0660","authenticated-orcid":false,"given":"Umang","family":"Mathur","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6311-1467","authenticated-orcid":false,"given":"Adithya","family":"Murali","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"P.","family":"Madhusudan","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Mahesh","family":"Viswanathan","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2020,7,14]]},"reference":[{"key":"32_CR1","unstructured":"Alur, R., et al.: Syntax-guided synthesis. In: Dependable Software Systems Engineering, NATO Science for Peace and Security Series, D: Information and Communication Security, vol. 40, pp. 1\u201325. IOS Press (2015)"},{"key":"32_CR2","doi-asserted-by":"publisher","unstructured":"Alur, R., Madhusudan, P.: Visibly pushdown languages. In: Proceedings of the Thirty-sixth Annual ACM Symposium on Theory of Computing, STOC 2004, pp. 202\u2013211. ACM, New York (2004). \nhttps:\/\/doi.org\/10.1145\/1007352.1007390","DOI":"10.1145\/1007352.1007390"},{"issue":"3","key":"32_CR3","doi-asserted-by":"publisher","first-page":"16:1","DOI":"10.1145\/1516512.1516518","volume":"56","author":"R Alur","year":"2009","unstructured":"Alur, R., Madhusudan, P.: Adding nesting structure to words. J. ACM 56(3), 16:1\u201316:43 (2009). \nhttps:\/\/doi.org\/10.1145\/1516512.1516518","journal-title":"J. ACM"},{"issue":"12","key":"32_CR4","doi-asserted-by":"publisher","first-page":"84","DOI":"10.1145\/3208071","volume":"61","author":"R Alur","year":"2018","unstructured":"Alur, R., Singh, R., Fisman, D., Solar-Lezama, A.: Search-based program synthesis. Commun. ACM 61(12), 84\u201393 (2018). \nhttps:\/\/doi.org\/10.1145\/3208071","journal-title":"Commun. ACM"},{"issue":"1","key":"32_CR5","doi-asserted-by":"publisher","first-page":"341","DOI":"10.2307\/2274974","volume":"55","author":"S Bauer-Mengelberg","year":"1990","unstructured":"Bauer-Mengelberg, S.: \u00fcber die vollst\u00e4ndigkeit des logikkalk\u00fcls. J. Symb. Log. 55(1), 341\u2013342 (1990). \nhttps:\/\/doi.org\/10.2307\/2274974","journal-title":"J. Symb. Log."},{"issue":"4","key":"32_CR6","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/j.entcs.2007.09.004","volume":"190","author":"R Bloem","year":"2007","unstructured":"Bloem, R., Galler, S.J., Jobstmann, B., Piterman, N., Pnueli, A., Weiglhofer, M.: Specify, compile, run: hardware from PSL. Electr. Notes Theor. Comput. Sci. 190(4), 3\u201316 (2007). \nhttps:\/\/doi.org\/10.1016\/j.entcs.2007.09.004","journal-title":"Electr. Notes Theor. Comput. Sci."},{"issue":"3","key":"32_CR7","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. 78(3), 911\u2013938 (2012). \nhttps:\/\/doi.org\/10.1016\/j.jcss.2011.08.007","journal-title":"J. Comput. Syst. Sci."},{"key":"32_CR8","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74113-8","volume-title":"The Calculus of Computation: Decision Procedures with Applications to Verification","author":"AR Bradley","year":"2007","unstructured":"Bradley, A.R., Manna, Z.: The Calculus of Computation: Decision Procedures with Applications to Verification. Springer, Heidelberg (2007). \nhttps:\/\/doi.org\/10.1007\/978-3-540-74113-8"},{"key":"32_CR9","doi-asserted-by":"publisher","first-page":"295","DOI":"10.2307\/1994916","volume":"138","author":"JR Buchi","year":"1969","unstructured":"Buchi, J.R., Landweber, L.H.: Solving sequential conditions by finite-state strategies. Trans. Am. Math. Soc. 138, 295\u2013311 (1969). \nhttps:\/\/doi.org\/10.2307\/1994916","journal-title":"Trans. Am. Math. Soc."},{"key":"32_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1007\/978-3-030-11245-5_17","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"D Bueno","year":"2019","unstructured":"Bueno, D., Sakallah, K.A.: euforia: complete software model checking with uninterpreted functions. In: Enea, C., Piskac, R. (eds.) VMCAI 2019. LNCS, vol. 11388, pp. 363\u2013385. Springer, Cham (2019). \nhttps:\/\/doi.org\/10.1007\/978-3-030-11245-5_17"},{"key":"32_CR11","unstructured":"Caulfield, B., Rabe, M.N., Seshia, S.A., Tripakis, S.: What\u2019s decidable about syntax-guided synthesis? CoRR abs\/1510.08393 (2015)"},{"issue":"1","key":"32_CR12","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1145\/322234.322243","volume":"28","author":"AK Chandra","year":"1981","unstructured":"Chandra, A.K., Kozen, D.C., Stockmeyer, L.J.: Alternation. J. ACM 28(1), 114\u2013133 (1981). \nhttps:\/\/doi.org\/10.1145\/322234.322243","journal-title":"J. ACM"},{"key":"32_CR13","unstructured":"Church, A.: Application of recursive arithmetic to the problem of circuit synthesis. Summaries of talks presented at the Summer Institute for Symbolic Logic Cornell University, 1957, 2nd edn., J. Symb. Log. 28(4), 30\u201350. 3a\u201345a. (1960)"},{"key":"32_CR14","unstructured":"Comon, H., et al.: Tree automata techniques and applications (2007). \nhttps:\/\/tata.gforge.inria.fr\n\n. Accessed 29 Jun 2020"},{"issue":"2","key":"32_CR15","doi-asserted-by":"publisher","first-page":"198","DOI":"10.1109\/TIT.1983.1056650","volume":"29","author":"D Dolev","year":"1983","unstructured":"Dolev, D., Yao, A.: On the security of public key protocols. IEEE Trans. Inf. Theory 29(2), 198\u2013208 (1983). \nhttps:\/\/doi.org\/10.1109\/TIT.1983.1056650","journal-title":"IEEE Trans. Inf. Theory"},{"issue":"2","key":"32_CR16","doi-asserted-by":"publisher","first-page":"247","DOI":"10.3233\/JCS-2004-12203","volume":"12","author":"N Durgin","year":"2004","unstructured":"Durgin, N., Lincoln, P., Mitchell, J., Scedrov, A.: Multiset rewriting and the complexity of bounded security protocols. J. Comput. Secur. 12(2), 247\u2013311 (2004). \nhttps:\/\/doi.org\/10.3233\/JCS-2004-12203","journal-title":"J. Comput. Secur."},{"issue":"POPL","key":"32_CR17","doi-asserted-by":"publisher","first-page":"61:1","DOI":"10.1145\/3158149","volume":"2","author":"A Farzan","year":"2018","unstructured":"Farzan, A., Kincaid, Z.: Strategy synthesis for linear arithmetic games. PACMPL 2(POPL), 61:1\u201361:30 (2018). \nhttps:\/\/doi.org\/10.1145\/3158149","journal-title":"PACMPL"},{"key":"32_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-36387-4","volume-title":"Automata, Logics, and Infinite Games: A Guide to Current Research [outcome of a Dagstuhl seminar, February 2001]","year":"2002","unstructured":"Gr\u00e4del, E., Thomas, W., Wilke, T. (eds.): Automata, Logics, and Infinite Games: A Guide to Current Research [outcome of a Dagstuhl seminar, February 2001]. Lecture Notes in Computer Science, vol. 2500. Springer, Heidelberg (2002). \nhttps:\/\/doi.org\/10.1007\/3-540-36387-4"},{"key":"32_CR19","doi-asserted-by":"publisher","unstructured":"Gulwani, S.: Automating string processing in spreadsheets using input-output examples. In: POPL, pp. 317\u2013330. ACM (2011). \nhttps:\/\/doi.org\/10.1145\/1925844.1926423","DOI":"10.1145\/1925844.1926423"},{"issue":"8","key":"32_CR20","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1145\/2240236.2240260","volume":"55","author":"S Gulwani","year":"2012","unstructured":"Gulwani, S., Harris, W.R., Singh, R.: Spreadsheet data manipulation using examples. Commun. ACM 55(8), 97\u2013105 (2012). \nhttps:\/\/doi.org\/10.1145\/2240236.2240260","journal-title":"Commun. ACM"},{"issue":"11","key":"32_CR21","doi-asserted-by":"publisher","first-page":"90","DOI":"10.1145\/2736282","volume":"58","author":"S Gulwani","year":"2015","unstructured":"Gulwani, S., Hern\u00e1ndez-Orallo, J., Kitzelmann, E., Muggleton, S.H., Schmid, U., Zorn, B.G.: Inductive programming meets the real world. Commun. ACM 58(11), 90\u201399 (2015). \nhttps:\/\/doi.org\/10.1145\/2736282","journal-title":"Commun. ACM"},{"issue":"1\u20132","key":"32_CR22","first-page":"1","volume":"4","author":"S Gulwani","year":"2017","unstructured":"Gulwani, S., Polozov, O., Singh, R.: Program synthesis. Found. Trends Program. Lang. 4(1\u20132), 1\u2013119 (2017)","journal-title":"Found. Trends Program. Lang."},{"key":"32_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"641","DOI":"10.1007\/978-3-642-36742-7_53","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M Heizmann","year":"2013","unstructured":"Heizmann, M., et al.: Ultimate automizer with smtinterpol. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 641\u2013643. Springer, Berlin Heidelberg, Berlin, Heidelberg (2013). \nhttps:\/\/doi.org\/10.1007\/978-3-642-36742-7_53"},{"key":"32_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1007\/978-3-642-03237-0_7","volume-title":"Static Analysis","author":"M Heizmann","year":"2009","unstructured":"Heizmann, M., Hoenicke, J., Podelski, A.: Refinement of trace abstraction. In: Palsberg, J., Su, Z. (eds.) SAS 2009. LNCS, vol. 5673, pp. 69\u201385. Springer, Heidelberg (2009). \nhttps:\/\/doi.org\/10.1007\/978-3-642-03237-0_7"},{"key":"32_CR25","doi-asserted-by":"publisher","unstructured":"Heizmann, M., Hoenicke, J., Podelski, A.: Nested interpolants. In: Proceedings of the 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2010, pp. 471\u2013482. ACM, New York (2010). \nhttps:\/\/doi.org\/10.1145\/1706299.1706353","DOI":"10.1145\/1706299.1706353"},{"key":"32_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"36","DOI":"10.1007\/978-3-642-39799-8_2","volume-title":"Computer Aided Verification","author":"M Heizmann","year":"2013","unstructured":"Heizmann, M., Hoenicke, J., Podelski, A.: Software model checking for people who love automata. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 36\u201352. Springer, Heidelberg (2013). \nhttps:\/\/doi.org\/10.1007\/978-3-642-39799-8_2"},{"key":"32_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"335","DOI":"10.1007\/978-3-030-25540-4_18","volume-title":"Computer Aided Verification","author":"Q Hu","year":"2019","unstructured":"Hu, Q., Breck, J., Cyphert, J., D\u2019Antoni, L., Reps, T.: Proving unrealizability for syntax-guided synthesis. In: Dillig, I., Tasiran, S. (eds.) CAV 2019. LNCS, vol. 11561, pp. 335\u2013352. Springer, Cham (2019). \nhttps:\/\/doi.org\/10.1007\/978-3-030-25540-4_18"},{"issue":"7","key":"32_CR28","doi-asserted-by":"publisher","first-page":"693","DOI":"10.1007\/s00236-017-0294-5","volume":"54","author":"S Jha","year":"2017","unstructured":"Jha, S., Seshia, S.A.: A theory of formal synthesis via inductive learning. Acta Inf. 54(7), 693\u2013726 (2017). \nhttps:\/\/doi.org\/10.1007\/s00236-017-0294-5","journal-title":"Acta Inf."},{"key":"32_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"494","DOI":"10.1007\/978-3-030-01090-4_29","volume-title":"Automated Technology for Verification and Analysis","author":"A Khalimov","year":"2018","unstructured":"Khalimov, A., Maderbacher, B., Bloem, R.: Bounded synthesis of register transducers. In: Lahiri, S.K., Wang, C. (eds.) ATVA 2018. LNCS, vol. 11138, pp. 494\u2013510. Springer, Cham (2018). \nhttps:\/\/doi.org\/10.1007\/978-3-030-01090-4_29"},{"key":"32_CR30","unstructured":"Krogmeier, P., Mathur, U., Murali, A., Madhusudan, P., Viswanathan, M.: Decidable synthesis of programs with uninterpreted functions. CoRR abs\/1910.09744 (2019). \nhttp:\/\/arxiv.org\/abs\/1910.09744"},{"key":"32_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"92","DOI":"10.1007\/3-540-44618-4_9","volume-title":"CONCUR 2000\u2014Concurrency Theory","author":"O Kupferman","year":"2000","unstructured":"Kupferman, O., Madhusudan, P., Thiagarajan, P.S., Vardi, M.Y.: Open systems in reactive environments: control and synthesis. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol. 1877, pp. 92\u2013107. Springer, Heidelberg (2000). \nhttps:\/\/doi.org\/10.1007\/3-540-44618-4_9"},{"key":"32_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"202","DOI":"10.1007\/978-3-642-13754-9_11","volume-title":"Time for Verification","author":"O Kupferman","year":"2010","unstructured":"Kupferman, O., Piterman, N., Vardi, M.Y.: An automata-theoretic approach to infinite-state systems. In: Manna, Z., Peled, D.A. (eds.) Time for Verification. LNCS, vol. 6200, pp. 202\u2013259. Springer, Heidelberg (2010). \nhttps:\/\/doi.org\/10.1007\/978-3-642-13754-9_11"},{"key":"32_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"36","DOI":"10.1007\/10722167_7","volume-title":"Computer Aided Verification","author":"O Kupferman","year":"2000","unstructured":"Kupferman, O., Vardi, M.Y.: An automata-theoretic approach to reasoning about infinite-state systems. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 36\u201352. Springer, Heidelberg (2000). \nhttps:\/\/doi.org\/10.1007\/10722167_7"},{"key":"32_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/978-3-662-49674-9_10","volume-title":"TACAS","author":"C L\u00f6ding","year":"2016","unstructured":"L\u00f6ding, C., Madhusudan, P., Neider, D.: Abstract learning frameworks for synthesis. In: Chechik, M., Raskin, J.F. (eds.) LTACAS 2016. LNCS, vol. 9636, pp. 167\u2013185. Springer, Heidelberg (2016). \nhttps:\/\/doi.org\/10.1007\/978-3-662-49674-9_10"},{"key":"32_CR35","doi-asserted-by":"publisher","unstructured":"Madhusudan, P.: Synthesizing reactive programs. In: CSL. LIPIcs, vol. 12, pp. 428\u2013442. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2011). \nhttps:\/\/doi.org\/10.4230\/LIPIcs.CSL.2011.428","DOI":"10.4230\/LIPIcs.CSL.2011.428"},{"key":"32_CR36","doi-asserted-by":"publisher","unstructured":"Madhusudan, P., Mathur, U., Saha, S., Viswanathan, M.: A decidable fragment of second order logic with applications to synthesis. In: Ghica, D., Jung, A. (eds.) 27th EACSL Annual Conference on Computer Science Logic (CSL 2018). Leibniz International Proceedings in Informatics (LIPIcs), vol. 119, pp. 31:1\u201331:19. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, Dagstuhl (2018). \nhttps:\/\/doi.org\/10.4230\/LIPIcs.CSL.2018.31","DOI":"10.4230\/LIPIcs.CSL.2018.31"},{"key":"32_CR37","doi-asserted-by":"publisher","unstructured":"Madhusudan, P., Parlato, G.: The tree width of auxiliary storage. In: Proceedings of the 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2011, pp. 283\u2013294. ACM, New York (2011). \nhttps:\/\/doi.org\/10.1145\/1926385.1926419","DOI":"10.1145\/1926385.1926419"},{"key":"32_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"396","DOI":"10.1007\/3-540-48224-5_33","volume-title":"Automata, Languages and Programming","author":"P Madhusudan","year":"2001","unstructured":"Madhusudan, P., Thiagarajan, P.S.: Distributed controller synthesis for local specifications. In: Orejas, F., Spirakis, P.G., van Leeuwen, J. (eds.) ICALP 2001. LNCS, vol. 2076, pp. 396\u2013407. Springer, Heidelberg (2001). \nhttps:\/\/doi.org\/10.1007\/3-540-48224-5_33"},{"issue":"POPL","key":"32_CR39","doi-asserted-by":"publisher","first-page":"46:1","DOI":"10.1145\/3290359","volume":"3","author":"U Mathur","year":"2019","unstructured":"Mathur, U., Madhusudan, P., Viswanathan, M.: Decidable verification of uninterpreted programs. Proc. ACM Program. Lang. 3(POPL), 46:1\u201346:29 (2019). \nhttps:\/\/doi.org\/10.1145\/3290359","journal-title":"Proc. ACM Program. Lang."},{"key":"32_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"158","DOI":"10.1007\/978-3-030-45237-7_10","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"U Mathur","year":"2020","unstructured":"Mathur, U., Madhusudan, P., Viswanathan, M.: What\u2019s decidable about program verification modulo axioms? In: Biere, A., Parker, D. (eds.) TACAS 2020. LNCS, vol. 12079, pp. 158\u2013177. Springer, Cham (2020). \nhttps:\/\/doi.org\/10.1007\/978-3-030-45237-7_10"},{"issue":"POPL","key":"32_CR41","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3371103","volume":"4","author":"U Mathur","year":"2019","unstructured":"Mathur, U., Murali, A., Krogmeier, P., Madhusudan, P., Viswanathan, M.: Deciding memory safety for single-pass heap-manipulating programs. Proc. ACM Program. Lang. 4(POPL), 1\u201329 (2019). \nhttps:\/\/doi.org\/10.1145\/3371103","journal-title":"Proc. ACM Program. Lang."},{"key":"32_CR42","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1007\/978-3-540-30579-8_6","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"M M\u00fcller-Olm","year":"2005","unstructured":"M\u00fcller-Olm, M., R\u00fcthing, O., Seidl, H.: Checking herbrand equalities and beyond. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, pp. 79\u201396. Springer, Heidelberg (2005). \nhttps:\/\/doi.org\/10.1007\/978-3-540-30579-8_6"},{"key":"32_CR43","doi-asserted-by":"publisher","unstructured":"Muscholl, A., Walukiewicz, I.: Distributed synthesis for acyclic architectures. In: FSTTCS. LIPIcs, vol. 29, pp. 639\u2013651. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2014). \nhttps:\/\/doi.org\/10.4230\/LIPIcs.FSTTCS.2014.639","DOI":"10.4230\/LIPIcs.FSTTCS.2014.639"},{"key":"32_CR44","doi-asserted-by":"publisher","unstructured":"Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: POPL, pp. 179\u2013190. ACM Press (1989). \nhttps:\/\/doi.org\/10.1145\/75277.75293","DOI":"10.1145\/75277.75293"},{"key":"32_CR45","doi-asserted-by":"publisher","unstructured":"Pnueli, A., Rosner, R.: Distributed reactive systems are hard to synthesize. In: FOCS, pp. 746\u2013757. IEEE Computer Society (1990). \nhttps:\/\/doi.org\/10.1109\/FSCS.1990.89597","DOI":"10.1109\/FSCS.1990.89597"},{"issue":"4","key":"32_CR46","doi-asserted-by":"publisher","first-page":"264","DOI":"10.1090\/S0002-9904-1946-08555-9","volume":"52","author":"EL Post","year":"1946","unstructured":"Post, E.L.: A variant of a recursively unsolvable problem. Bull. Amer. Math. Soc. 52(4), 264\u2013268 (1946). \nhttps:\/\/doi.org\/10.1090\/S0002-9904-1946-08555-9","journal-title":"Bull. Amer. Math. Soc."},{"issue":"OOPSLA","key":"32_CR47","doi-asserted-by":"publisher","first-page":"65:1","DOI":"10.1145\/3133889","volume":"1","author":"X Qiu","year":"2017","unstructured":"Qiu, X., Solar-Lezama, A.: Natural synthesis of provably-correct data-structure manipulations. PACMPL 1(OOPSLA), 65:1\u201365:28 (2017). \nhttps:\/\/doi.org\/10.1145\/3133889","journal-title":"PACMPL"},{"key":"32_CR48","doi-asserted-by":"publisher","DOI":"10.1090\/cbms\/013","volume-title":"Automata on Infinite Objects and Church\u2019s Problem","author":"MO Rabin","year":"1972","unstructured":"Rabin, M.O.: Automata on Infinite Objects and Church\u2019s Problem. American Mathematical Society, Boston (1972)"},{"issue":"6","key":"32_CR49","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1145\/2499370.2462195","volume":"48","author":"R Singh","year":"2013","unstructured":"Singh, R., Gulwani, S., Solar-Lezama, A.: Automated feedback generation for introductory programming assignments. SIGPLAN Not. 48(6), 15\u201326 (2013). \nhttps:\/\/doi.org\/10.1145\/2499370.2462195","journal-title":"SIGPLAN Not."},{"issue":"5","key":"32_CR50","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. Int. J. Softw. Tools Technol. Transf. 15(5), 475\u2013495 (2013). \nhttps:\/\/doi.org\/10.1007\/s10009-012-0249-7","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"32_CR51","doi-asserted-by":"publisher","unstructured":"Solar-Lezama, A., Tancau, L., Bod\u00edk, R., Seshia, S.A., Saraswat, V.A.: Combinatorial sketching for finite programs. In: ASPLOS, pp. 404\u2013415. ACM (2006). \nhttps:\/\/doi.org\/10.1145\/1168857.1168907","DOI":"10.1145\/1168857.1168907"},{"key":"32_CR52","unstructured":"SyGuS: Syntax guided synthesis. \nhttps:\/\/sygus.org\/"},{"key":"32_CR53","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"628","DOI":"10.1007\/BFb0055090","volume-title":"Automata, Languages and Programming","author":"MY Vardi","year":"1998","unstructured":"Vardi, M.Y.: Reasoning about the past with two-way automata. In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) ICALP 1998. LNCS, vol. 1443, pp. 628\u2013641. Springer, Heidelberg (1998). \nhttps:\/\/doi.org\/10.1007\/BFb0055090"},{"issue":"POPL","key":"32_CR54","doi-asserted-by":"publisher","first-page":"63:1","DOI":"10.1145\/3158151","volume":"2","author":"X Wang","year":"2017","unstructured":"Wang, X., Dillig, I., Singh, R.: Program synthesis using abstraction refinement. Proc. ACM Program. Lang. 2(POPL), 63:1\u201363:30 (2017). \nhttps:\/\/doi.org\/10.1145\/3158151","journal-title":"Proc. ACM Program. Lang."},{"key":"32_CR55","doi-asserted-by":"publisher","unstructured":"Wang, X., Gulwani, S., Singh, R.: FIDEX: filtering spreadsheet data using examples. In: Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2016, pp. 195\u2013213. ACM, New York (2016). \nhttps:\/\/doi.org\/10.1145\/2983990.2984030","DOI":"10.1145\/2983990.2984030"},{"issue":"OOPSLA","key":"32_CR56","doi-asserted-by":"publisher","first-page":"155:1","DOI":"10.1145\/3276525","volume":"2","author":"Y Wang","year":"2018","unstructured":"Wang, Y., Wang, X., Dillig, I.: Relational program synthesis. Proc. ACM Program. Lang. 2(OOPSLA), 155:1\u2013155:27 (2018). \nhttps:\/\/doi.org\/10.1145\/3276525","journal-title":"Proc. ACM Program. Lang."}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-53291-8_32","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,7,15]],"date-time":"2020-07-15T20:09:01Z","timestamp":1594843741000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-53291-8_32"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030532901","9783030532918"],"references-count":56,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-53291-8_32","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"14 July 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","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":"2020","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"21 July 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24 July 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"32","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/i-cav.org\/2020\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair.org","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"240","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"43","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"22","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"18% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"4","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"11","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"The conference was held virtually due to the COVID-19 pandemic.","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}