{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T18:21:19Z","timestamp":1784830879800,"version":"3.55.0"},"publisher-location":"Cham","reference-count":46,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030112448","type":"print"},{"value":"9783030112455","type":"electronic"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"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":[[2019]]},"DOI":"10.1007\/978-3-030-11245-5_2","type":"book-chapter","created":{"date-parts":[[2019,1,10]],"date-time":"2019-01-10T13:45:18Z","timestamp":1547127918000},"page":"24-47","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":16,"title":["Program Synthesis with Equivalence Reduction"],"prefix":"10.1007","author":[{"given":"Calvin","family":"Smith","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Aws","family":"Albarghouthi","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2019,1,11]]},"reference":[{"key":"2_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1007\/978-3-642-17796-5_12","volume-title":"Algebraic Methodology and Software Technology","author":"B Alarc\u00f3n","year":"2011","unstructured":"Alarc\u00f3n, B., Guti\u00e9rrez, R., Lucas, S., Navarro-Marset, R.: Proving termination properties with mu-term. In: Johnson, M., Pavlovic, D. (eds.) AMAST 2010. LNCS, vol. 6486, pp. 201\u2013208. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-17796-5_12"},{"key":"2_CR2","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). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_67"},{"key":"2_CR3","doi-asserted-by":"crossref","unstructured":"Alur, R., et al.: Syntax-guided synthesis. In: FMCAD (2013)","DOI":"10.1109\/FMCAD.2013.6679385"},{"key":"2_CR4","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139172752","volume-title":"Term Rewriting and All That","author":"F Baader","year":"1998","unstructured":"Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998)"},{"key":"2_CR5","first-page":"1","volume":"2","author":"L Bachmair","year":"1989","unstructured":"Bachmair, L., Dershowitz, N., Plaisted, D.A.: Completion without failure. Resolut. Eqn. Algebraic Struct. 2, 1\u201330 (1989)","journal-title":"Resolut. Eqn. Algebraic Struct."},{"key":"2_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"6","DOI":"10.1007\/978-3-642-13977-2_3","volume-title":"Tests and Proofs","author":"K Claessen","year":"2010","unstructured":"Claessen, K., Smallbone, N., Hughes, J.: QuickSpec: guessing formal specifications using testing. In: Fraser, G., Gargantini, A. (eds.) TAP 2010. LNCS, vol. 6143, pp. 6\u201321. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-13977-2_3"},{"key":"2_CR7","doi-asserted-by":"crossref","unstructured":"Comon, H., Jacquemard, F.: Ground reducibility is EXPTIME-complete. In: Proceedings of the 12th Annual IEEE Symposium on Logic in Computer Science, LICS 1997, pp. 26\u201334. IEEE (1997)","DOI":"10.1109\/LICS.1997.614922"},{"key":"2_CR8","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: Proceedings of the 4th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, pp. 238\u2013252. ACM (1977)","DOI":"10.1145\/512950.512973"},{"key":"2_CR9","doi-asserted-by":"crossref","unstructured":"De Bruijn, N.G.: Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem. In: Indagationes Mathematicae, Proceedings, vol. 75, pp. 381\u2013392. Elsevier (1972)","DOI":"10.1016\/1385-7258(72)90034-0"},{"key":"2_CR10","unstructured":"Dean, J., Ghemawat, S.: MapReduce: simplified data processing on large clusters. In: OSDI (2004)"},{"key":"2_CR11","unstructured":"Dechter, E., Malmaud, J., Adams, R.P., Tenenbaum, J.B.: Bootstrap learning via modular concept discovery. In: IJCAI (2013)"},{"key":"2_CR12","first-page":"61801","volume":"51","author":"N Dershowitz","year":"1985","unstructured":"Dershowitz, N.: Synthesis by completion. Urbana 51, 61801 (1985)","journal-title":"Urbana"},{"key":"2_CR13","doi-asserted-by":"crossref","unstructured":"Feser, J.K., Chaudhuri, S., Dillig, I.: Synthesizing data structure transformations from input-output examples. In: PLDI (2015)","DOI":"10.1145\/2737924.2737977"},{"key":"2_CR14","doi-asserted-by":"crossref","unstructured":"Frankle, J., Osera, P.M., Walker, D., Zdancewic, S.: Example-directed synthesis: a type-theoretic interpretation. In: POPL (2016)","DOI":"10.1145\/2837614.2837629"},{"key":"2_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1007\/11814771_24","volume-title":"Automated Reasoning","author":"J Giesl","year":"2006","unstructured":"Giesl, J., Schneider-Kamp, P., Thiemann, R.: AProVE 1.2: automatic termination proofs in the dependency pair framework. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS, vol. 4130, pp. 281\u2013286. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11814771_24"},{"issue":"8","key":"2_CR16","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. CACM 55(8), 97\u2013105 (2012)","journal-title":"CACM"},{"key":"2_CR17","doi-asserted-by":"crossref","unstructured":"Gvero, T., Kuncak, V., Kuraj, I., Piskac, R.: Complete completion using types and weights. In: PLDI (2013)","DOI":"10.1145\/2491956.2462192"},{"issue":"2","key":"2_CR18","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1023\/A:1005872405899","volume":"18","author":"T Hillenbrand","year":"1997","unstructured":"Hillenbrand, T., Buch, A., Vogt, R., L\u00f6chner, B.: Waldmeister-high-performance equational deduction. J. Autom. Reason. 18(2), 265\u2013270 (1997)","journal-title":"J. Autom. Reason."},{"key":"2_CR19","unstructured":"Klein, D., Hirokawa, N.: Maximal completion. In: LIPIcs-Leibniz International Proceedings in Informatics, vol. 10. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik (2011)"},{"key":"2_CR20","doi-asserted-by":"crossref","unstructured":"Kneuss, E., Kuraj, I., Kuncak, V., Suter, P.: Synthesis modulo recursive functions. In: OOPSLA (2013)","DOI":"10.1145\/2509136.2509555"},{"key":"2_CR21","series-title":"Symbolic Computation","doi-asserted-by":"publisher","first-page":"342","DOI":"10.1007\/978-3-642-81955-1_23","volume-title":"Automation of Reasoning","author":"DE Knuth","year":"1983","unstructured":"Knuth, D.E., Bendix, P.B.: Simple word problems in universal algebras. In: Siekmann, J.H., Wrightson, G. (eds.) Automation of Reasoning. SYMBOLIC, pp. 342\u2013376. Springer, Heidelberg (1983). https:\/\/doi.org\/10.1007\/978-3-642-81955-1_23"},{"key":"2_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"295","DOI":"10.1007\/978-3-642-02348-4_21","volume-title":"Rewriting Techniques and Applications","author":"M Korp","year":"2009","unstructured":"Korp, M., Sternagel, C., Zankl, H., Middeldorp, A.: Tyrolean termination tool 2. In: Treinen, R. (ed.) RTA 2009. LNCS, vol. 5595, pp. 295\u2013304. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02348-4_21"},{"issue":"1","key":"2_CR23","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1023\/A:1006129631807","volume":"23","author":"M Kurihara","year":"1999","unstructured":"Kurihara, M., Kondo, H.: Completion for multiple reduction orderings. J. Autom. Reason. 23(1), 25\u201342 (1999)","journal-title":"J. Autom. Reason."},{"issue":"1\u20132","key":"2_CR24","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1023\/A:1025671410623","volume":"53","author":"T Lau","year":"2003","unstructured":"Lau, T., Wolfman, S.A., Domingos, P., Weld, D.S.: Programming by demonstration using version space algebra. Mach. Learn. 53(1\u20132), 111\u2013156 (2003)","journal-title":"Mach. Learn."},{"key":"2_CR25","unstructured":"Liang, P., Jordan, M.I., Klein, D.: Learning programs: a hierarchical Bayesian approach. In: Proceedings of the 27th International Conference on Machine Learning, ICML 2010, pp. 639\u2013646 (2010)"},{"issue":"4","key":"2_CR26","doi-asserted-by":"publisher","first-page":"289","DOI":"10.1007\/s10817-006-9031-4","volume":"36","author":"B L\u00f6chner","year":"2006","unstructured":"L\u00f6chner, B.: Things to know when implementing KBO. J. Autom. Reason. 36(4), 289\u2013310 (2006)","journal-title":"J. Autom. Reason."},{"issue":"2","key":"2_CR27","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/BF00245458","volume":"9","author":"W McCune","year":"1992","unstructured":"McCune, W.: Experiments with discrimination-tree indexing and path indexing for term retrieval. J. Autom. Reason. 9(2), 147\u2013167 (1992). https:\/\/doi.org\/10.1007\/BF00245458","journal-title":"J. Autom. Reason."},{"key":"2_CR28","unstructured":"Menon, A.K., Tamuz, O., Gulwani, S., Lampson, B.W., Kalai, A.: A machine learning framework for programming by example. In: ICML (2013)"},{"key":"2_CR29","first-page":"3","volume":"44","author":"PS Novikov","year":"1955","unstructured":"Novikov, P.S.: On the algorithmic unsolvability of the word problem in group theory. Trudy Matematicheskogo Instituta imeni VA Steklova 44, 3\u2013143 (1955)","journal-title":"Trudy Matematicheskogo Instituta imeni VA Steklova"},{"key":"2_CR30","doi-asserted-by":"crossref","unstructured":"Osera, P., Zdancewic, S.: Type-and-example-directed program synthesis. In: PLDI (2015)","DOI":"10.1145\/2737924.2738007"},{"key":"2_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"332","DOI":"10.1007\/3-540-48685-2_27","volume-title":"Rewriting Techniques and Applications","author":"F Otto","year":"1999","unstructured":"Otto, F.: On the connections between rewriting and formal language theory. In: Narendran, P., Rusinowitch, M. (eds.) RTA 1999. LNCS, vol. 1631, pp. 332\u2013355. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-48685-2_27"},{"key":"2_CR32","doi-asserted-by":"crossref","unstructured":"Phothilimthana, P.M., Thakur, A., Bodik, R., Dhurjati, D.: Scaling up superoptimization. In: Proceedings of the Twenty-First International Conference on Architectural Support for Programming Languages and Operating Systems, pp. 297\u2013310. ACM (2016)","DOI":"10.1145\/2872362.2872387"},{"issue":"6","key":"2_CR33","doi-asserted-by":"publisher","first-page":"522","DOI":"10.1145\/2980983.2908093","volume":"51","author":"Nadia Polikarpova","year":"2016","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, pp. 522\u2013538. ACM (2016)","journal-title":"ACM SIGPLAN Notices"},{"key":"2_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"388","DOI":"10.1007\/3-540-51081-8_121","volume-title":"Rewriting Techniques and Applications","author":"US Reddy","year":"1989","unstructured":"Reddy, U.S.: Rewriting techniques for program synthesis. In: Dershowitz, N. (ed.) RTA 1989. LNCS, vol. 355, pp. 388\u2013403. Springer, Heidelberg (1989). https:\/\/doi.org\/10.1007\/3-540-51081-8_121"},{"issue":"4","key":"2_CR35","doi-asserted-by":"publisher","first-page":"305","DOI":"10.1145\/2499368.2451150","volume":"48","author":"E Schkufza","year":"2013","unstructured":"Schkufza, E., Sharma, R., Aiken, A.: Stochastic superoptimization. ACM SIGPLAN Not. 48(4), 305\u2013316 (2013)","journal-title":"ACM SIGPLAN Not."},{"key":"2_CR36","doi-asserted-by":"crossref","unstructured":"Smith, C., Albarghouthi, A.: MapReduce program synthesis. In: Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 326\u2013340. ACM (2016)","DOI":"10.1145\/2908080.2908102"},{"key":"2_CR37","doi-asserted-by":"crossref","unstructured":"Smith, C., Ferns, G., Albarghouthi, A.: Discovering relational specifications. In: Proceedings of the 2017 11th Joint Meeting on Foundations of Software Engineering, pp. 616\u2013626. ACM (2017)","DOI":"10.1145\/3106237.3106279"},{"key":"2_CR38","doi-asserted-by":"crossref","unstructured":"Solar-Lezama, A., Tancau, L., Bod\u00edk, R., Seshia, S.A., Saraswat, V.A.: Combinatorial sketching for finite programs. In: ASPLOS (2006)","DOI":"10.1145\/1168857.1168907"},{"issue":"6","key":"2_CR39","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1145\/2499370.2462174","volume":"48","author":"A Udupa","year":"2013","unstructured":"Udupa, A., Raghavan, A., Deshmukh, J.V., Mador-Haim, S., Martin, M.M., Alur, R.: TRANSIT: specifying protocols with concolic snippets. ACM SIGPLAN Not. 48(6), 287\u2013296 (2013)","journal-title":"ACM SIGPLAN Not."},{"issue":"POPL","key":"2_CR40","first-page":"63","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 (2017)","journal-title":"Proc. ACM Program. Lang."},{"key":"2_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1007\/11805618_22","volume-title":"Term Rewriting and Applications","author":"I Wehrman","year":"2006","unstructured":"Wehrman, I., Stump, A., Westbrook, E.: Slothrop: Knuth-Bendix completion with a modern termination checker. In: Pfenning, F. (ed.) RTA 2006. LNCS, vol. 4098, pp. 287\u2013296. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11805618_22"},{"key":"2_CR42","unstructured":"White, T.: Hadoop - The Definitive Guide: Storage and Analysis at Internet Scale (2015)"},{"key":"2_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"518","DOI":"10.1007\/978-3-642-14203-1_43","volume-title":"Automated Reasoning","author":"S Winkler","year":"2010","unstructured":"Winkler, S., Middeldorp, A.: Termination tools in ordered completion. In: Giesl, J., H\u00e4hnle, R. (eds.) IJCAR 2010. LNCS, vol. 6173, pp. 518\u2013532. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14203-1_43"},{"key":"2_CR44","unstructured":"Yu, Y., et al.: DryadLINQ: a system for general-purpose distributed data-parallel computing using a high-level language. In: OSDI (2008)"},{"key":"2_CR45","unstructured":"Zaharia, M., et al.: Resilient distributed datasets: a fault-tolerant abstraction for in-memory cluster computing. In: NSDI (2012)"},{"issue":"2","key":"2_CR46","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/s10817-009-9131-z","volume":"43","author":"H Zankl","year":"2009","unstructured":"Zankl, H., Hirokawa, N., Middeldorp, A.: KBO orientability. J. Autom. Reason. 43(2), 173\u2013201 (2009)","journal-title":"J. Autom. Reason."}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-11245-5_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,11,13]],"date-time":"2019-11-13T22:16:01Z","timestamp":1573683361000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-11245-5_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030112448","9783030112455"],"references-count":46,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-11245-5_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"VMCAI","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Verification, Model Checking, and Abstract Interpretation","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Cascais","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Portugal","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"13 January 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15 January 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"20","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"vmcai2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/popl19.sigplan.org\/track\/VMCAI-2019","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}