{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,2]],"date-time":"2025-08-02T05:08:23Z","timestamp":1754111303378,"version":"3.40.3"},"publisher-location":"Cham","reference-count":47,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319633862"},{"type":"electronic","value":"9783319633879"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-63387-9_13","type":"book-chapter","created":{"date-parts":[[2017,7,12]],"date-time":"2017-07-12T08:53:43Z","timestamp":1499849623000},"page":"254-278","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":13,"title":["Synthesis with Abstract Examples"],"prefix":"10.1007","author":[{"given":"Dana","family":"Drachsler-Cohen","sequence":"first","affiliation":[]},{"given":"Sharon","family":"Shoham","sequence":"additional","affiliation":[]},{"given":"Eran","family":"Yahav","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,7,13]]},"reference":[{"key":"13_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"934","DOI":"10.1007\/978-3-642-39799-8_67","volume-title":"Computer Aided Verification","author":"A Albarghouthi","year":"2013","unstructured":"Albarghouthi, A., Gulwani, S., Kincaid, Z.: Recursive program synthesis. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 934\u2013950. Springer, Heidelberg (2013). doi:10.1007\/978-3-642-39799-8_67"},{"key":"13_CR2","doi-asserted-by":"crossref","unstructured":"Alur, R., Bodik, R., Juniwal, G., Martin, M.M.K., Raghothaman, M., Seshia, S.A., Singh, R., Solar-Lezama, A., Torlak, E., Udupa, A.: Syntax-guided synthesis. In: FMCAD 2013 (2013)","DOI":"10.1109\/FMCAD.2013.6679385"},{"key":"13_CR3","doi-asserted-by":"crossref","unstructured":"Alur, R., Fisman, D., Singh, R., Solar-Lezama, A.: SyGuS-Comp 2016: results and analysis. In: SYNT@CAV 2016 (2016)","DOI":"10.4204\/EPTCS.229.13"},{"issue":"4","key":"13_CR4","first-page":"319","volume":"2","author":"D Angluin","year":"1988","unstructured":"Angluin, D.: Queries and concept learning. Mach. Learn. 2(4), 319\u2013342 (1988)","journal-title":"Mach. Learn."},{"key":"13_CR5","doi-asserted-by":"crossref","unstructured":"Barowy, D.W., Gulwani, S., Hart, T., Zorn, B.: FlashRelate: extracting relational data from semi-structured spreadsheets using examples. In: PLDI 2015 (2015)","DOI":"10.1145\/2737924.2737952"},{"key":"13_CR6","unstructured":"Bex, G.J., Neven, F., Schwentick, T., Tuyls, K.: Inference of concise DTDs from XML data. In: VLDB 2006 (2006)"},{"key":"13_CR7","doi-asserted-by":"crossref","unstructured":"Bornholt, J., Torlak, E., Grossman, D., Ceze, L.: Optimizing synthesis with metasketches. In: POPL 2016 (2016)","DOI":"10.1145\/2837614.2837666"},{"key":"13_CR8","doi-asserted-by":"crossref","unstructured":"Botin\u010dan, M., Babi\u0107, D.: Sigma*: symbolic learning of input-output specifications. In: POPL 2013, pp. 443\u2013456 (2013)","DOI":"10.1145\/2480359.2429123"},{"key":"13_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"76","DOI":"10.1007\/3-540-58520-6_55","volume-title":"Algorithmic Learning Theory","author":"A Br\u0101zma","year":"1994","unstructured":"Br\u0101zma, A., \u010cer\u0101ns, K.: Efficient learning of regular expressions from good examples. In: Arikawa, S., Jantke, K.P. (eds.) AII\/ALT -1994. LNCS, vol. 872, pp. 76\u201390. Springer, Heidelberg (1994). doi:10.1007\/3-540-58520-6_55"},{"key":"13_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1007\/978-3-642-40935-6_4","volume-title":"Algorithmic Learning Theory","author":"NH Bshouty","year":"2013","unstructured":"Bshouty, N.H.: Exact learning from membership queries: some techniques, results and new directions. In: Jain, S., Munos, R., Stephan, F., Zeugmann, T. (eds.) ALT 2013. LNCS, vol. 8139, pp. 33\u201352. Springer, Heidelberg (2013). doi:10.1007\/978-3-642-40935-6_4"},{"key":"13_CR11","doi-asserted-by":"crossref","unstructured":"Cochran, R.A., D\u2019Antoni, L., Livshits, B., Molnar, D., Veanes, M.: Program boosting: program synthesis via crowd-sourcing. In: POPL 2015 (2015)","DOI":"10.1145\/2676726.2676973"},{"key":"13_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"128","DOI":"10.1007\/978-3-642-35873-9_10","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"P Cousot","year":"2013","unstructured":"Cousot, P., Cousot, R., F\u00e4hndrich, M., Logozzo, F.: Automatic inference of necessary preconditions. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) VMCAI 2013. LNCS, vol. 7737, pp. 128\u2013148. Springer, Heidelberg (2013). doi:10.1007\/978-3-642-35873-9_10"},{"key":"13_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"150","DOI":"10.1007\/978-3-642-18275-4_12","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"P Cousot","year":"2011","unstructured":"Cousot, P., Cousot, R., Logozzo, F.: Precondition inference from intermittent assertions and application to contracts on collections. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol. 6538, pp. 150\u2013168. Springer, Heidelberg (2011). doi:10.1007\/978-3-642-18275-4_12"},{"key":"13_CR14","doi-asserted-by":"crossref","unstructured":"Das Sarma, A., Parameswaran, A., Garcia-Molina, H., Widom, J.: Synthesizing view definitions from data. In: ICDT 2010 (2010)","DOI":"10.1145\/1804669.1804683"},{"key":"13_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L De Moura","year":"2008","unstructured":"De Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). doi:10.1007\/978-3-540-78800-3_24"},{"issue":"8","key":"13_CR16","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1145\/360933.360975","volume":"18","author":"EW Dijkstra","year":"1975","unstructured":"Dijkstra, E.W.: Guarded commands, nondeterminacy and formal derivation of programs. Commun. ACM 18(8), 453\u2013457 (1975)","journal-title":"Commun. ACM"},{"key":"13_CR17","doi-asserted-by":"publisher","first-page":"521","DOI":"10.1016\/j.ic.2008.12.008","volume":"207","author":"H Fernau","year":"2009","unstructured":"Fernau, H.: Algorithms for learning regular expressions from positive data. Inf. Comput. 207, 521\u2013541 (2009)","journal-title":"Inf. Comput."},{"key":"13_CR18","doi-asserted-by":"crossref","unstructured":"Feser, J.K., Chaudhuri, S., Dillig, I.: Synthesizing data structure transformations from input-output examples. In: PLDI 2015 (2015)","DOI":"10.1145\/2737924.2737977"},{"key":"13_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1007\/978-3-319-08867-9_5","volume-title":"Computer Aided Verification","author":"P Garg","year":"2014","unstructured":"Garg, P., L\u00f6ding, C., Madhusudan, P., Neider, D.: ICE: a robust framework for learning invariants. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 69\u201387. Springer, Cham (2014). doi:10.1007\/978-3-319-08867-9_5"},{"issue":"5","key":"13_CR20","doi-asserted-by":"publisher","first-page":"447","DOI":"10.1016\/S0019-9958(67)91165-5","volume":"10","author":"EM Gold","year":"1967","unstructured":"Gold, E.M.: Language identification in the limit. Inf. Control 10(5), 447\u2013474 (1967)","journal-title":"Inf. Control"},{"key":"13_CR21","doi-asserted-by":"crossref","unstructured":"Gulwani, S.: Automating string processing in spreadsheets using input-output examples. In: POPL 2011 (2011)","DOI":"10.1145\/1926385.1926423"},{"key":"13_CR22","doi-asserted-by":"crossref","unstructured":"Gulwani, S.: Dimensions in program synthesis. In: PPDP 2010 (2010)","DOI":"10.1145\/1836089.1836091"},{"issue":"8","key":"13_CR23","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)","journal-title":"Commun. ACM"},{"key":"13_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1007\/978-3-540-71316-6_18","volume-title":"Programming Languages and Systems","author":"S Gulwani","year":"2007","unstructured":"Gulwani, S., Tiwari, A.: Computing procedure summaries for interprocedural analysis. In: Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 253\u2013267. Springer, Heidelberg (2007). doi:10.1007\/978-3-540-71316-6_18"},{"key":"13_CR25","doi-asserted-by":"crossref","unstructured":"Harris, W.R., Gulwani, S.: Spreadsheet table transformations from examples. In: PLDI 2011 (2011)","DOI":"10.1145\/1993498.1993536"},{"key":"13_CR26","doi-asserted-by":"crossref","unstructured":"Jha, S., Gulwani, S., Seshia, S.A., Tiwari, A.: Oracle-guided component-based program synthesis. In: ICSE 2010 (2010)","DOI":"10.1145\/1806799.1806833"},{"key":"13_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"94","DOI":"10.1007\/978-3-642-15488-1_9","volume-title":"Grammatical Inference: Theoretical Results and Applications","author":"E Kinber","year":"2010","unstructured":"Kinber, E.: Learning regular expressions from representative examples and membership queries. In: Sempere, J.M., Garc\u00eda, P. (eds.) ICGI 2010. LNCS, vol. 6339, pp. 94\u2013108. Springer, Heidelberg (2010). doi:10.1007\/978-3-642-15488-1_9"},{"key":"13_CR28","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1023\/A:1025671410623","volume":"53","author":"TA Lau","year":"2003","unstructured":"Lau, T.A., Wolfman, S.A., Domingos, P., Weld, D.S.: Programming by demonstration using version space algebra. Mach. Learn. 53, 111\u2013156 (2003)","journal-title":"Mach. Learn."},{"key":"13_CR29","doi-asserted-by":"crossref","unstructured":"Le, V., Gulwani, S.: Flashextract: a framework for data extraction by examples. In: PLDI 2014 (2014)","DOI":"10.1145\/2594291.2594333"},{"key":"13_CR30","unstructured":"Menon, A.K., Tamuz, O., Gulwani, S., Lampson, B.W., Kalai, A.: A machine learning framework for programming by example. In: ICML 2013 (2013)"},{"key":"13_CR31","unstructured":"Muggleton, S., Feng, C.: Efficient induction of logic programs. In: First Conference on Algorithmic Learning Theory, pp. 368\u2013381 (1990)"},{"key":"13_CR32","first-page":"153","volume":"5","author":"GD Plotkin","year":"1970","unstructured":"Plotkin, G.D.: A note on inductive generalization. Mach. Intell. 5, 153\u2013163 (1970)","journal-title":"Mach. Intell."},{"key":"13_CR33","doi-asserted-by":"crossref","unstructured":"Polozov, O., Gulwani, S.: Flashmeta: a framework for inductive program synthesis. In: OOPSLA 2015 (2015)","DOI":"10.1145\/2814270.2814310"},{"key":"13_CR34","doi-asserted-by":"crossref","unstructured":"Raychev, V., Bielik, P., Vechev, M., Krause, A.: Learning programs from noisy data. In: POPL 2016 (2016)","DOI":"10.1145\/2837614.2837671"},{"key":"13_CR35","doi-asserted-by":"crossref","unstructured":"Raza, M., Gulwani, S., Milic-Frayling, N.: Programming by example using least general generalizations. In: AAAI 2014 (2014)","DOI":"10.1609\/aaai.v28i1.8744"},{"key":"13_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"303","DOI":"10.1007\/11547662_21","volume-title":"Static Analysis","author":"X Rival","year":"2005","unstructured":"Rival, X.: Understanding the origin of alarms in Astr\u00e9e. In: Hankin, C., Siveroni, I. (eds.) SAS 2005. LNCS, vol. 3672, pp. 303\u2013319. Springer, Heidelberg (2005). doi:10.1007\/11547662_21"},{"issue":"1","key":"13_CR37","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1016\/S0304-3975(97)00014-5","volume":"185","author":"Y Sakakibara","year":"1997","unstructured":"Sakakibara, Y.: Recent advances of grammatical inference. Theor. Comput. Sci. 185(1), 15\u201345 (1997)","journal-title":"Theor. Comput. Sci."},{"key":"13_CR38","doi-asserted-by":"crossref","unstructured":"Singh, R., Gulwani, S.: Learning semantic string transformations from examples. In: VLDB 2012 (2012)","DOI":"10.14778\/2212351.2212356"},{"key":"13_CR39","doi-asserted-by":"crossref","unstructured":"Singh, R., Gulwani, S.: Transforming spreadsheet data types using examples. In: POPL 2016 (2016)","DOI":"10.1145\/2837614.2837668"},{"key":"13_CR40","doi-asserted-by":"crossref","unstructured":"Singh, R., Solar-Lezama, A.: Synthesizing data structure manipulations from storyboards. In: ESEC\/FSE 2011 (2011)","DOI":"10.1145\/2025113.2025153"},{"key":"13_CR41","volume-title":"Program Synthesis by Sketching","author":"A Solar-Lezama","year":"2008","unstructured":"Solar-Lezama, A.: Program Synthesis by Sketching. ProQuest, Ann Arbor (2008)"},{"key":"13_CR42","doi-asserted-by":"crossref","unstructured":"Solar-Lezama, A., Jones, C.G., Bodik, R.: Sketching concurrent data structures. In: PLDI 2008 (2008)","DOI":"10.1145\/1375581.1375599"},{"issue":"4","key":"13_CR43","doi-asserted-by":"publisher","first-page":"14","DOI":"10.1145\/1985342.1985345","volume":"33","author":"S Tripakis","year":"2011","unstructured":"Tripakis, S., Lickly, B., Henzinger, T.A., Lee, E.A.: A theory of synchronous relational interfaces. ACM Trans. Program. Lang. Syst. 33(4), 14 (2011)","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"11","key":"13_CR44","doi-asserted-by":"publisher","first-page":"1134","DOI":"10.1145\/1968.1972","volume":"27","author":"LG Valiant","year":"1984","unstructured":"Valiant, L.G.: A theory of the learnable. Commun. ACM 27(11), 1134\u20131142 (1984)","journal-title":"Commun. ACM"},{"key":"13_CR45","doi-asserted-by":"crossref","unstructured":"Veanes, M., Hooimeijer, P., Livshits, B., Molnar, D., Bjorner, N.: Symbolic finite state transducers: algorithms and applications. In: POPL 2012 (2012)","DOI":"10.1145\/2103656.2103674"},{"key":"13_CR46","doi-asserted-by":"crossref","unstructured":"Wang, X., Gulwani, S., Singh, R.: Fidex: filtering spreadsheet data using examples. In: OOPSLA 2016 (2016)","DOI":"10.1145\/2983990.2984030"},{"key":"13_CR47","doi-asserted-by":"crossref","unstructured":"Yessenov, K., Tulsiani, S., Menon, A.K., Miller, R.C., Gulwani, S., Lampson, B.W., Kalai, A.: A colorful approach to text processing by example. In: UIST 2013 (2013)","DOI":"10.1145\/2501988.2502040"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-63387-9_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,7,30]],"date-time":"2022-07-30T20:26:08Z","timestamp":1659212768000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-63387-9_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319633862","9783319633879"],"references-count":47,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-63387-9_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]},"assertion":[{"value":"13 July 2017","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":"Heidelberg","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Germany","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2017","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24 July 2017","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28 July 2017","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2017","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/cavconference.org\/2017\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}