{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T00:52:10Z","timestamp":1740099130427,"version":"3.37.3"},"publisher-location":"Cham","reference-count":35,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319961446"},{"type":"electronic","value":"9783319961453"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-96145-3_22","type":"book-chapter","created":{"date-parts":[[2018,7,20]],"date-time":"2018-07-20T22:25:55Z","timestamp":1532125555000},"page":"407-426","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":8,"title":["Learning Abstractions for Program Synthesis"],"prefix":"10.1007","author":[{"given":"Xinyu","family":"Wang","sequence":"first","affiliation":[]},{"given":"Greg","family":"Anderson","sequence":"additional","affiliation":[]},{"given":"Isil","family":"Dillig","sequence":"additional","affiliation":[]},{"given":"K. L.","family":"McMillan","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2018,7,18]]},"reference":[{"key":"22_CR1","doi-asserted-by":"crossref","unstructured":"Gulwani, S.: Automating string processing in spreadsheets using input-output examples. In: Proceedings of the 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL, pp. 317\u2013330. ACM (2011)","DOI":"10.1145\/1926385.1926423"},{"key":"22_CR2","doi-asserted-by":"crossref","unstructured":"Singh, R., Gulwani, S.: Transforming spreadsheet data types using examples. In: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL, pp. 343\u2013356. ACM (2016)","DOI":"10.1145\/2837614.2837668"},{"key":"22_CR3","doi-asserted-by":"crossref","unstructured":"Wang, X., Gulwani, S., Singh, R.: FIDEX: filtering spreadsheet data using examples. In: OOPSLA, pp. 195\u2013213. ACM (2016)","DOI":"10.1145\/2983990.2984030"},{"key":"22_CR4","doi-asserted-by":"crossref","unstructured":"Feng, Y., Martins, R., Van Geffen, J., Dillig, I., Chaudhuri, S.: Component-based synthesis of table consolidation and transformation tasks from examples. In: PLDI, pp. 422\u2013436. ACM (2017)","DOI":"10.1145\/3062341.3062351"},{"issue":"OOPSLA","key":"22_CR5","first-page":"62:1","volume":"1","author":"X Wang","year":"2017","unstructured":"Wang, X., Dillig, I., Singh, R.: Synthesis of data completion scripts using finite tree automata. Proc. ACM Program. Lang. 1(OOPSLA), 62:1\u201362:26 (2017)","journal-title":"Proc. ACM Program. Lang."},{"key":"22_CR6","doi-asserted-by":"crossref","unstructured":"Yaghmazadeh, N., Wang, X., Dillig, I.: Automated migration of hierarchical data to relational tables using programming-by-example. In: Proceedings of the VLDB Endowment (2018)","DOI":"10.1145\/3187009.3177735"},{"key":"22_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"86","DOI":"10.1007\/978-3-319-63390-9_5","volume-title":"Computer Aided Verification","author":"A Gasc\u00f3n","year":"2017","unstructured":"Gasc\u00f3n, A., Tiwari, A., Carmer, B., Mathur, U.: Look for the proof to find the program: decorated-component-based program synthesis. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017. LNCS, vol. 10427, pp. 86\u2013103. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63390-9_5"},{"key":"22_CR8","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"482","DOI":"10.1007\/978-3-319-21401-6_33","volume-title":"Automated Deduction - CADE-25","author":"A Tiwari","year":"2015","unstructured":"Tiwari, A., Gasc\u00f3n, A., Dutertre, B.: Program synthesis using dual interpretation. In: Felty, A.P., Middeldorp, A. (eds.) CADE 2015. LNCS (LNAI), vol. 9195, pp. 482\u2013497. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21401-6_33"},{"key":"22_CR9","doi-asserted-by":"crossref","unstructured":"Feng, Y., Martins, R., Wang, Y., Dillig, I., Reps, T.W.: Component-based synthesis for complex APIs. In: POPL, vol. 52, pp. 599\u2013612. ACM (2017)","DOI":"10.1145\/3009837.3009851"},{"key":"22_CR10","doi-asserted-by":"crossref","unstructured":"Gvero, T., Kuncak, V., Kuraj, I., Piskac, R.: Complete completion using types and weights. In: Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI, pp. 27\u201338. ACM (2013)","DOI":"10.1145\/2491956.2462192"},{"key":"22_CR11","doi-asserted-by":"crossref","unstructured":"Mandelin, D., Xu, L., Bod\u00edk, R., Kimelman, D.: Jungloid mining: helping to navigate the API jungle. In: Proceedings of the 26th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI, pp. 48\u201361. ACM (2005)","DOI":"10.1145\/1065010.1065018"},{"key":"22_CR12","doi-asserted-by":"crossref","unstructured":"Feser, J.K., Chaudhuri, S., Dillig, I.: Synthesizing data structure transformations from input-output examples. In: Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI, pp. 229\u2013239. ACM (2015)","DOI":"10.1145\/2737924.2737977"},{"key":"22_CR13","doi-asserted-by":"crossref","unstructured":"Polikarpova, N., Kuraj, I., Solar-Lezama, A.: Program synthesis from polymorphic refinement types. In: Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI, pp. 522\u2013538. ACM (2016)","DOI":"10.1145\/2908080.2908093"},{"key":"22_CR14","doi-asserted-by":"crossref","unstructured":"Wang, X., Dillig, I., Singh, R.: Program synthesis using abstraction refinement, vol. 2, pp. 63:1\u201363:30. ACM (2017)","DOI":"10.1145\/3158151"},{"key":"22_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1007\/978-3-319-66706-5_18","volume-title":"Static Analysis","author":"S So","year":"2017","unstructured":"So, S., Oh, H.: Synthesizing imperative programs from examples guided by static analysis. In: Ranzato, F. (ed.) SAS 2017. LNCS, vol. 10422, pp. 364\u2013381. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-66706-5_18"},{"key":"22_CR16","doi-asserted-by":"crossref","unstructured":"Wang, C., Cheung, A., Bodik, R.: Synthesizing highly expressive SQL queries from input-output examples. In: Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI, pp. 452\u2013466. ACM (2017)","DOI":"10.1145\/3062341.3062365"},{"issue":"10","key":"22_CR17","doi-asserted-by":"crossref","first-page":"816","DOI":"10.14778\/2977797.2977807","volume":"9","author":"R Singh","year":"2016","unstructured":"Singh, R.: BlinkFill: semi-supervised programming by example for syntactic string transformations. Proc. VLDB Endow. 9(10), 816\u2013827 (2016)","journal-title":"Proc. VLDB Endow."},{"key":"22_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/978-3-642-45221-5_13","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"R Blanc","year":"2013","unstructured":"Blanc, R., Gupta, A., Kov\u00e1cs, L., Kragl, B.: Tree interpolation in vampire. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds.) LPAR 2013. LNCS, vol. 8312, pp. 173\u2013181. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-45221-5_13"},{"key":"22_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-31980-1_1","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"KL McMillan","year":"2005","unstructured":"McMillan, K.L.: Applications of craig interpolants in model checking. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 1\u201312. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/978-3-540-31980-1_1"},{"key":"22_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-45069-6_1","volume-title":"Computer Aided Verification","author":"KL McMillan","year":"2003","unstructured":"McMillan, K.L.: Interpolation and SAT-based model checking. In: Hunt, W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 1\u201313. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/978-3-540-45069-6_1"},{"key":"22_CR21","unstructured":"Wang, X., Dillig, I., Singh, R.: Learning Abstractions for Program Synthesis. arXiv preprint arXiv:1804.04152 (2018)"},{"key":"22_CR22","unstructured":"Z3. https:\/\/github.com\/Z3Prover\/z3"},{"key":"22_CR23","unstructured":"Keilhauer, A., Levy, S., Lochbihler, A., \u00d6kmen, S., Thimm, G., W\u00fcrzebesser, C.: JLinAlg: a java-library for linear algebra without rounding errors. Technical report (2003\u20132010). http:\/\/jlinalg.sourceforge.net\/"},{"key":"22_CR24","doi-asserted-by":"crossref","unstructured":"Bloem, R., Egly, U., Klampfl, P., K\u00f6nighofer, R., Lonsing, F.: Sat-based methods for circuit synthesis. In: Formal Methods in Computer-Aided Design, FMCAD 2014, 21\u201324 October 2014, Lausanne, Switzerland, pp. 31\u201334. IEEE (2014)","DOI":"10.1109\/FMCAD.2014.6987592"},{"issue":"POPL","key":"22_CR25","doi-asserted-by":"crossref","first-page":"61","DOI":"10.1145\/3158149","volume":"2","author":"A Farzan","year":"2017","unstructured":"Farzan, A., Kincaid, Z.: Strategy synthesis for linear arithmetic games. Proc. ACM Program. Lang. 2(POPL), 61 (2017)","journal-title":"Proc. ACM Program. Lang."},{"issue":"5\u20136","key":"22_CR26","doi-asserted-by":"crossref","first-page":"505","DOI":"10.1007\/s10009-007-0044-z","volume":"9","author":"D Beyer","year":"2007","unstructured":"Beyer, D., Henzinger, T.A., Jhala, R., Majumdar, R.: The software model checker BLAST. Int. J. Softw. Tools Technol. Transf. 9(5\u20136), 505\u2013525 (2007)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"22_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"672","DOI":"10.1007\/978-3-642-31424-7_48","volume-title":"Computer Aided Verification","author":"A Albarghouthi","year":"2012","unstructured":"Albarghouthi, A., Li, Y., Gurfinkel, A., Chechik, M.: Ufo: a framework for abstraction- and interpolation-based software verification. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 672\u2013678. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31424-7_48"},{"key":"22_CR28","series-title":"IFIP International Federation for Information Processing","doi-asserted-by":"publisher","first-page":"367","DOI":"10.1007\/978-1-4020-8157-6_28","volume-title":"Building the Information Society","author":"T Lev-Ami","year":"2004","unstructured":"Lev-Ami, T., Manevich, R., Sagiv, M.: TVLA: a system for generating abstract interpreters. In: Jacquart, R. (ed.) Building the Information Society. IIFIP, vol. 156, pp. 367\u2013375. Springer, Boston, MA (2004). https:\/\/doi.org\/10.1007\/978-1-4020-8157-6_28"},{"key":"22_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"280","DOI":"10.1007\/978-3-540-45099-3_15","volume-title":"Static Analysis","author":"T Lev-Ami","year":"2000","unstructured":"Lev-Ami, T., Sagiv, M.: TVLA: a system for implementing static analyses. In: Palsberg, J. (ed.) SAS 2000. LNCS, vol. 1824, pp. 280\u2013301. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/978-3-540-45099-3_15"},{"key":"22_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1007\/3-540-45319-9_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Pnueli","year":"2001","unstructured":"Pnueli, A., Ruah, S., Zuck, L.: Automatic deductive verification with invisible invariants. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 82\u201397. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-45319-9_7"},{"key":"22_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"267","DOI":"10.1007\/978-3-540-24622-0_22","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"SK Lahiri","year":"2004","unstructured":"Lahiri, S.K., Bryant, R.E.: Constructing quantified invariants via predicate abstraction. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 267\u2013281. Springer, Heidelberg (2004)"},{"key":"22_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-662-49122-5_1","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"T Reps","year":"2016","unstructured":"Reps, T., Thakur, A.: Automating abstract interpretation. In: Jobstmann, B., Leino, K.R.M. (eds.) VMCAI 2016. LNCS, vol. 9583, pp. 3\u201340. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-49122-5_1"},{"key":"22_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"252","DOI":"10.1007\/978-3-540-24622-0_21","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"T Reps","year":"2004","unstructured":"Reps, T., Sagiv, M., Yorsh, G.: Symbolic implementation of the best transformer. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 252\u2013266. Springer, Heidelberg (2004)"},{"key":"22_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"174","DOI":"10.1007\/978-3-642-31424-7_17","volume-title":"Computer Aided Verification","author":"A Thakur","year":"2012","unstructured":"Thakur, A., Reps, T.: A method for symbolic computation of abstract operations. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 174\u2013192. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31424-7_17"},{"key":"22_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/11513988_6","volume-title":"Computer Aided Verification","author":"R Jhala","year":"2005","unstructured":"Jhala, R., McMillan, K.L.: Interpolant-based transition relation approximation. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 39\u201351. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11513988_6"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-96145-3_22","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,6]],"date-time":"2020-11-06T11:14:40Z","timestamp":1604661280000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-96145-3_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319961446","9783319961453"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-96145-3_22","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]}}}