{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T03:44:20Z","timestamp":1725853460295},"publisher-location":"Berlin, Heidelberg","reference-count":46,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662496732"},{"type":"electronic","value":"9783662496749"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"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":[[2016]]},"DOI":"10.1007\/978-3-662-49674-9_10","type":"book-chapter","created":{"date-parts":[[2016,4,8]],"date-time":"2016-04-08T14:49:00Z","timestamp":1460126940000},"page":"167-185","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":15,"title":["Abstract Learning Frameworks for Synthesis"],"prefix":"10.1007","author":[{"given":"Christof","family":"L\u00f6ding","sequence":"first","affiliation":[]},{"given":"P.","family":"Madhusudan","sequence":"additional","affiliation":[]},{"given":"Daniel","family":"Neider","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,4,9]]},"reference":[{"key":"10_CR1","unstructured":"Alur, R., Bod\u00edk, R., Dallal, E., Fisman, D., Garg, P., Juniwal, G., Kress-Gazit, H., Madhusudan, P., Martin, M.M.K., Raghothaman, M., Saha, S., Seshia, S.A., Singh, R., Solar-Lezama, A., Torlak, E., Udupa, A.: 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":"10_CR2","doi-asserted-by":"crossref","unstructured":"Alur, R., Bod\u00edk, 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, pp. 1\u20138. IEEE (2013)","DOI":"10.1109\/FMCAD.2013.6679385"},{"key":"10_CR3","doi-asserted-by":"crossref","unstructured":"Alur, R., Cern\u00fd, P., Madhusudan, P., Nam, W.: Synthesis of interface specifications for java classes. In: POPL 2005, pp. 98\u2013109. ACM (2005)","DOI":"10.1145\/1047659.1040314"},{"key":"10_CR4","unstructured":"Alur, R., Fisman, D., Singh, R., Solar-Lezama, A.: Results and analysis of sygus-comp 2015. Technical report, University of Pennsylvania (2015). \n                      http:\/\/www.cis.upenn.edu\/ fisman\/documents\/AFSS_SYNT15.pdf"},{"key":"10_CR5","doi-asserted-by":"crossref","unstructured":"Angluin, D.: Computational learning theory: survey and selected bibliography. In: STOC 1992, pp. 351\u2013369. ACM (1992)","DOI":"10.1145\/129712.129746"},{"key":"10_CR6","unstructured":"Baker, A.: Simplicity. In: Zalta, E.N. (ed.) The Stanford Encyclopedia of Philosophy. Fall 2013 edn. (2013). \n                      http:\/\/plato.stanford.edu\/archives\/fall2013\/entries\/simplicity\/"},{"key":"10_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1007\/11804192_17","volume-title":"Formal Methods for Components and Objects","author":"M Barnett","year":"2006","unstructured":"Barnett, M., Chang, B.-Y.E., DeLine, R., Jacobs, B., M. Leino, K.R.: Boogie: a modular reusable verifier for object-oriented programs. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol. 4111, pp. 364\u2013387. Springer, Heidelberg (2006)"},{"key":"10_CR8","doi-asserted-by":"crossref","unstructured":"Betts, A., Chong, N., Donaldson, A.F., Qadeer, S., Thomson, P.: Gpuverify: a verifier for GPU kernels. In: OOPSLA 2012, pp. 113\u2013132. ACM (2012)","DOI":"10.1145\/2398857.2384625"},{"key":"10_CR9","first-page":"373","volume":"9","author":"A Blum","year":"1992","unstructured":"Blum, A.: Learning boolean functions in an infinite attribute space. Mach. Learn. 9, 373\u2013386 (1992)","journal-title":"Mach. Learn."},{"key":"10_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"180","DOI":"10.1007\/978-3-319-21668-3_11","volume-title":"Computer Aided Verification","author":"P \u010cern\u00fd","year":"2015","unstructured":"\u010cern\u00fd, P., Clarke, E.M., Henzinger, T.A., Radhakrishna, A., Ryzhyk, L., Samanta, R., Tarrach, T.: From non-preemptive to preemptive scheduling using synchronization synthesis. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9207, pp. 180\u2013197. Springer, Heidelberg (2015)"},{"issue":"1","key":"10_CR11","first-page":"48","volume":"37","author":"A Cheung","year":"2014","unstructured":"Cheung, A., Madden, S., Solar-Lezama, A., Arden, O., Myers, A.C.: Using program analysis to improve database applications. IEEE Data Eng. Bull. 37(1), 48\u201359 (2014)","journal-title":"IEEE Data Eng. Bull."},{"key":"10_CR12","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL, pp. 238\u2013252. ACM (1977)","DOI":"10.1145\/512950.512973"},{"issue":"4","key":"10_CR13","doi-asserted-by":"publisher","first-page":"409","DOI":"10.1023\/A:1009868929893","volume":"3","author":"PM Domingos","year":"1999","unstructured":"Domingos, P.M.: The role of occam\u2019s razor in knowledge discovery. Data Min. Knowl. Discov. 3(4), 409\u2013425 (1999)","journal-title":"Data Min. Knowl. Discov."},{"key":"10_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"500","DOI":"10.1007\/3-540-45251-6_29","volume-title":"FME 2001: Formal Methods for Increasing Software Productivity","author":"C Flanagan","year":"2001","unstructured":"Flanagan, C., M. Leino, K.R.: Houdini, an annotation assistant for ESC\/Java. In: Oliveira, J.N., Zave, P. (eds.) FME 2001. LNCS, vol. 2021, pp. 500\u2013517. Springer, Heidelberg (2001)"},{"key":"10_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"813","DOI":"10.1007\/978-3-642-39799-8_57","volume-title":"Computer Aided Verification","author":"P Garg","year":"2013","unstructured":"Garg, P., L\u00f6ding, C., Madhusudan, P., Neider, D.: Learning universally quantified invariants of linear data structures. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 813\u2013829. Springer, Heidelberg (2013)"},{"key":"10_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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, Heidelberg (2014)"},{"key":"10_CR17","doi-asserted-by":"crossref","unstructured":"Garg, P., Madhusudan, P., Neider, D., Roth, D.: Learning invariants using decision trees and implication counterexamples. In: POPL 2016 (2016, to appear)","DOI":"10.1145\/2837614.2837664"},{"key":"10_CR18","doi-asserted-by":"crossref","unstructured":"Gulwani, S.: Automating string processing in spreadsheets using input-output examples. In: POPL 2011, pp. 317\u2013330. ACM (2011)","DOI":"10.1145\/1925844.1926423"},{"key":"10_CR19","doi-asserted-by":"crossref","unstructured":"Gulwani, S., Jha, S., Tiwari, A., Venkatesan, R.: Synthesis of loop-free programs. In: PLDI 2011, pp. 62\u201373. ACM (2011)","DOI":"10.1145\/1993316.1993506"},{"issue":"1","key":"10_CR20","doi-asserted-by":"publisher","first-page":"326","DOI":"10.1112\/plms\/s3-2.1.326","volume":"3\u20132","author":"G Higman","year":"1952","unstructured":"Higman, G.: Ordering by divisibility in abstract algebras. Proc. London Math. Soc. 3\u20132(1), 326\u2013336 (1952)","journal-title":"Proc. London Math. Soc."},{"key":"10_CR21","doi-asserted-by":"crossref","unstructured":"Jha, S., Gulwani, S., Seshia, S.A., Tiwari, A.: Oracle-guided component-based program synthesis. In: ICSE 2010, pp. 215\u2013224. ACM (2010)","DOI":"10.1145\/1806799.1806833"},{"key":"10_CR22","doi-asserted-by":"crossref","unstructured":"Jin, X., Donz\u00e9, A., Deshmukh, J.V., Seshia, S.A.: Mining requirements from closed-loop control models. In: HSCC 2013, pp. 43\u201352. ACM (2013)","DOI":"10.1145\/2461328.2461337"},{"key":"10_CR23","doi-asserted-by":"crossref","unstructured":"Karaivanov, S., Raychev, V., Vechev, M.T.: Phrase-based statistical translation of programming languages. In: Onward!, SLASH 2014, pp. 173\u2013184. ACM (2014)","DOI":"10.1145\/2661136.2661148"},{"key":"10_CR24","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/3897.001.0001","volume-title":"An Introduction to Computational Learning Theory","author":"MJ Kearns","year":"1994","unstructured":"Kearns, M.J., Vazirani, U.V.: An Introduction to Computational Learning Theory. MIT Press, Cambridge, MA, USA (1994)"},{"key":"10_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"50","DOI":"10.1007\/978-3-642-11931-6_3","volume-title":"Approaches and Applications of Inductive Programming","author":"E Kitzelmann","year":"2010","unstructured":"Kitzelmann, E.: Inductive programming: a survey of program synthesis techniques. In: Schmid, U., Kitzelmann, E., Plasmeijer, R. (eds.) AAIP 2009. LNCS, vol. 5812, pp. 50\u201373. Springer, Heidelberg (2010)"},{"key":"10_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1007\/978-3-319-21668-3_13","volume-title":"Computer Aided Verification","author":"E Kneuss","year":"2015","unstructured":"Kneuss, E., Koukoutos, M., Kuncak, V.: Deductive program repair. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9207, pp. 217\u2013233. Springer, Heidelberg (2015)"},{"key":"10_CR27","doi-asserted-by":"crossref","unstructured":"Kneuss, E., Kuraj, I., Kuncak, V., Suter, P.: Synthesis modulo recursive functions. In: OOPSLA 2013, pp. 407\u2013426. ACM (2013)","DOI":"10.1145\/2544173.2509555"},{"key":"10_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"11","DOI":"10.1007\/978-3-662-43948-7_2","volume-title":"Automata, Languages, and Programming","author":"V Kuncak","year":"2014","unstructured":"Kuncak, V.: Verifying and synthesizing software with recursive functions. In: Esparza, J., Fraigniaud, P., Husfeldt, T., Koutsoupias, E. (eds.) ICALP 2014. LNCS, vol. 8572, pp. 11\u201325. Springer, Heidelberg (2014)"},{"key":"10_CR29","doi-asserted-by":"crossref","unstructured":"Lal, A., Qadeer, S.: Powering the static driver verifier using corral. In: (FSE-22), pp. 202\u2013212. ACM (2014)","DOI":"10.1145\/2635868.2635894"},{"key":"10_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"427","DOI":"10.1007\/978-3-642-31424-7_32","volume-title":"Computer Aided Verification","author":"A Lal","year":"2012","unstructured":"Lal, A., Qadeer, S., Lahiri, S.K.: A solver for reachability modulo theories. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 427\u2013443. Springer, Heidelberg (2012)"},{"key":"10_CR31","unstructured":"L\u00f6ding, C., Madhusudan, P., Neider, D.: Abstract learning frameworks for synthesis. Technical report, University of Illinois at Urbana-Champaign (2016). \n                      http:\/\/madhu.cs.illinois.edu\/tacas16b\/"},{"issue":"1","key":"10_CR32","doi-asserted-by":"publisher","first-page":"90","DOI":"10.1145\/357084.357090","volume":"2","author":"Z Manna","year":"1980","unstructured":"Manna, Z., Waldinger, R.: A deductive approach to program synthesis. ACM Trans. Program. Lang. Syst. 2(1), 90\u2013121 (1980)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"10_CR33","unstructured":"Mitchell, T.M.: Machine Learning. McGraw-Hill, New York (1997)"},{"key":"10_CR34","unstructured":"Neider, D.: Applications of Automata Learning in Verification and Synthesis. Ph.D. thesis, RWTH Aachen University (April 2014)"},{"key":"10_CR35","unstructured":"Neider, D., Saha, S., Madhusudan, P.: Synthesizing piece-wise functions by learning classifiers. In: TACAS 2016, LNCS. Springer (to appear, 2016)"},{"key":"10_CR36","doi-asserted-by":"crossref","unstructured":"Osera, P., Zdancewic, S.: Type-and-example-directed program synthesis. In: PLDI 2015, pp. 619\u2013630. ACM (2015)","DOI":"10.1145\/2813885.2738007"},{"key":"10_CR37","doi-asserted-by":"crossref","unstructured":"Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: POPL 1989, pp. 179\u2013190 (1989)","DOI":"10.1145\/75277.75293"},{"key":"10_CR38","unstructured":"Quinlan, J.R.: C4.5: programs for machine learning. Morgan Kaufmann, Burlington (1993)"},{"key":"10_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"440","DOI":"10.1007\/978-3-319-21690-4_26","volume-title":"Computer Aided Verification","author":"S Saha","year":"2015","unstructured":"Saha, S., Garg, P., Madhusudan, P.: Alchemist: learning guarded affine functions. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 440\u2013446. Springer, Heidelberg (2015)"},{"key":"10_CR40","doi-asserted-by":"crossref","unstructured":"Schkufza, E., Sharma, R., Aiken, A.: Stochastic superoptimization. In: ASPLOS 2013, pp. 305\u2013316. ACM (2013)","DOI":"10.1145\/2499368.2451150"},{"key":"10_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"88","DOI":"10.1007\/978-3-319-08867-9_6","volume-title":"Computer Aided Verification","author":"R Sharma","year":"2014","unstructured":"Sharma, R., Aiken, A.: From invariant checking to invariant inference using randomized search. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 88\u2013105. Springer, Heidelberg (2014)"},{"key":"10_CR42","unstructured":"Solar-Lezama, A.: Program synthesis by sketching. Ph.D. thesis, University of California at Berkeley (2008)"},{"issue":"11","key":"10_CR43","doi-asserted-by":"crossref","first-page":"404","DOI":"10.1145\/1168918.1168907","volume":"41","author":"Armando Solar-Lezama","year":"2006","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 (2006)","journal-title":"ACM SIGPLAN Notices"},{"key":"10_CR44","unstructured":"Thakur, A., Lal, A., Lim, J., Reps, T.: PostHat and all that: Attaining most-precise inductive invariants. Technical report TR1790, University of Wisconsin, Madison (April 2013)"},{"key":"10_CR45","doi-asserted-by":"crossref","unstructured":"Udupa, A., Raghavan, A., Deshmukh, J.V., Mador-Haim, S., Martin, M.M.K., Alur, R.: TRANSIT: specifying protocols with concolic snippets. In: PLDI 2013, pp. 287\u2013296. ACM (2013)","DOI":"10.1145\/2499370.2462174"},{"key":"10_CR46","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"274","DOI":"10.1007\/978-3-540-30482-1_26","volume-title":"Formal Methods and Software Engineering","author":"A Vardhan","year":"2004","unstructured":"Vardhan, A., Sen, K., Viswanathan, M., Agha, G.: Learning to verify safety properties. In: Davies, J., Schulte, W., Barnett, M. (eds.) ICFEM 2004. LNCS, vol. 3308, pp. 274\u2013289. Springer, Heidelberg (2004)"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-49674-9_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,3,23]],"date-time":"2020-03-23T21:12:52Z","timestamp":1584997972000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-49674-9_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783662496732","9783662496749"],"references-count":46,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-49674-9_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]},"assertion":[{"value":"9 April 2016","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}