Abstract
Input-output examples are a simple and accessible way of describing program behaviour. Program synthesis from input-output examples has the potential of extending the range of computational tasks achievable by end-users who have no programming knowledge, but can articulate their desired computations by describing input-output behaviour. In this paper, we present Escher, a generic and efficient algorithm that interacts with the user via input-output examples, and synthesizes recursive programs implementing intended behaviour. Escher is parameterized by the components (instructions) that can be used in the program, thus providing a generic synthesis algorithm that can be instantiated to suit different domains. To search through the space of programs, Escher adopts a novel search strategy that utilizes special data structures for inferring conditionals and synthesizing recursive procedures. Our experimental evaluation of Escher demonstrates its ability to efficiently synthesize a wide range of programs, manipulating integers, lists, and trees. Moreover, we show that Escher outperforms a state-of-the-art SAT-based synthesis tool from the literature.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Flash Fill (Microsoft Excel 2013 feature), http://research.microsoft.com/users/sumitg/flashfill.html
Your wish is my command: programming by example. Morgan Kaufmann Publishers Inc. (2001)
Aditya Menon, S.G.B.L., Tamuz, O., Kalai, A.: A machine learning framework for programming by example. In: ICML 2013 (2013)
Albarghouthi, A., Gulwani, S., Kincaid, Z.: Recursive program synthesis, http://www.cs.toronto.edu/~aws/papers/cav13a.pdf
Bonet, B., Geffner, H.: Planning as heuristic search. Artificial Intelligence 129(1-2), 5–33 (2001)
Flener, P.: Inductive logic program synthesis with dialogs. In: Inductive Logic Programming Workshop, pp. 175–198 (1996)
Flener, P., Yilmaz, S.: Inductive synthesis of recursive logic programs: Achievements and prospects. J. Log. Program. 41(2-3), 141–195 (1999)
Gulwani, S.: Automating string processing in spreadsheets using input-output examples. In: Proc. of POPL 2011, pp. 317–330 (2011)
Gulwani, S.: Synthesis from examples: Interaction models and algorithms. In: Proc. of SYNASC (2012) (Invited talk paper)
Gulwani, S., Jha, S., Tiwari, A., Venkatesan, R.: Synthesis of loop-free programs. In: Proc. of PLDI 2011, pp. 62–73 (2011)
Gulwani, S., Korthikanti, V.A., Tiwari, A.: Synthesizing geometry constructions. In: Proc. of PLDI 2011, pp. 50–61 (2011)
Harris, W.R., Gulwani, S.: Spreadsheet table transformations from examples. In: Proc. of PLDI 2011, pp. 317–328 (2011)
Jha, S., Gulwani, S., Seshia, S.A., Tiwari, A.: Oracle-guided component-based program synthesis. In: Proc. of ICSE 2010, pp. 215–224 (2010)
Kitzelmann, E., Schmid, U.: Inductive synthesis of functional programs: An explanation based generalization approach. JMLR 7, 429–454 (2006)
Lau, T., Wolfman, S.A., Domingos, P., Weld, D.S.: Programming by demonstration using version space algebra. JMLR 53(1-2), 111–156 (2003)
Manna, Z., Waldinger, R.J.: A deductive approach to program synthesis. ACM TOPLAS 2(1), 90–121 (1980)
Manna, Z., Wolper, P.: Synthesis of communicating processes from temporal logic specifications. ACM Trans. Program. Lang. Syst. 6(1), 68–93 (1984)
Menon, A., Tamuz, O., Gulwani, S., Lampson, B., Kalai, A.: A machine learning framework for programming by example. In: ICML (to appear, 2013)
Mitchell, T.M.: Generalization as search. Artif. Intell. 18(2), 203–226 (1982)
Nau, D., Ghallab, M., Traverso, P.: Automated Planning: Theory & Practice. Morgan Kaufmann Publishers Inc., San Francisco (2004)
Shapiro, E.Y.: Algorithmic Program DeBugging. MIT Press, Cambridge (1983)
Singh, R., Gulwani, S.: Synthesizing number transformations from input-output examples. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 634–651. Springer, Heidelberg (2012)
Solar-Lezama, A., Tancau, L., BodÃk, R., Seshia, S.A., Saraswat, V.A.: Combinatorial sketching for finite programs. In: Proc. of ASPLOS 2006, pp. 404–415 (2006)
Summers, P.D.: A methodology for lisp program construction from examples. J. ACM 24(1), 161–175 (1977)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Albarghouthi, A., Gulwani, S., Kincaid, Z. (2013). Recursive Program Synthesis. In: Sharygina, N., Veith, H. (eds) Computer Aided Verification. CAV 2013. Lecture Notes in Computer Science, vol 8044. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-39799-8_67
Download citation
DOI: https://doi.org/10.1007/978-3-642-39799-8_67
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-39798-1
Online ISBN: 978-3-642-39799-8
eBook Packages: Computer ScienceComputer Science (R0)