More Web Proxy on the site http://driver.im/

Article

Recursive Program Synthesis

Authors:

Aws Albarghouthi,

Zachary KincaidAuthors Info & Claims

CAV 2013: Proceedings of the 25th International Conference on Computer Aided Verification - Volume 8044

Pages 934 - 950

Published: 13 July 2013 Publication History

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.

References

[1]

Flash Fill Microsoft Excel 2013 feature, http://research.microsoft.com/users/sumitg/flashfill.html

[2]

Your wish is my command: programming by example. Morgan Kaufmann Publishers Inc. 2001

[3]

Aditya Menon, S.G.B.L., Tamuz, O., Kalai, A.: A machine learning framework for programming by example. In: ICML 2013 2013

[4]

Albarghouthi, A., Gulwani, S., Kincaid, Z.: Recursive program synthesis, http://www.cs.toronto.edu/~aws/papers/cav13a.pdf

[5]

Bonet, B., Geffner, H.: Planning as heuristic search. Artificial Intelligence 1291-2, 5---33 2001

Digital Library

[6]

Flener, P.: Inductive logic program synthesis with dialogs. In: Inductive Logic Programming Workshop, pp. 175---198 1996

Digital Library

[7]

Flener, P., Yilmaz, S.: Inductive synthesis of recursive logic programs: Achievements and prospects. J. Log. Program. 412-3, 141---195 1999

[8]

Gulwani, S.: Automating string processing in spreadsheets using input-output examples. In: Proc. of POPL 2011, pp. 317---330 2011

Digital Library

[9]

Gulwani, S.: Synthesis from examples: Interaction models and algorithms. In: Proc. of SYNASC 2012 Invited talk paper

Digital Library

[10]

Gulwani, S., Jha, S., Tiwari, A., Venkatesan, R.: Synthesis of loop-free programs. In: Proc. of PLDI 2011, pp. 62---73 2011

Digital Library

[11]

Gulwani, S., Korthikanti, V.A., Tiwari, A.: Synthesizing geometry constructions. In: Proc. of PLDI 2011, pp. 50---61 2011

Digital Library

[12]

Harris, W.R., Gulwani, S.: Spreadsheet table transformations from examples. In: Proc. of PLDI 2011, pp. 317---328 2011

Digital Library

[13]

Jha, S., Gulwani, S., Seshia, S.A., Tiwari, A.: Oracle-guided component-based program synthesis. In: Proc. of ICSE 2010, pp. 215---224 2010

Digital Library

[14]

Kitzelmann, E., Schmid, U.: Inductive synthesis of functional programs: An explanation based generalization approach. JMLR 7, 429---454 2006

Digital Library

[15]

Lau, T., Wolfman, S.A., Domingos, P., Weld, D.S.: Programming by demonstration using version space algebra. JMLR 531-2, 111---156 2003

Digital Library

[16]

Manna, Z., Waldinger, R.J.: A deductive approach to program synthesis. ACM TOPLAS 21, 90---121 1980

Digital Library

[17]

Manna, Z., Wolper, P.: Synthesis of communicating processes from temporal logic specifications. ACM Trans. Program. Lang. Syst. 61, 68---93 1984

Digital Library

[18]

Menon, A., Tamuz, O., Gulwani, S., Lampson, B., Kalai, A.: A machine learning framework for programming by example. In: ICML to appear, 2013

[19]

Mitchell, T.M.: Generalization as search. Artif. Intell. 182, 203---226 1982

[20]

Nau, D., Ghallab, M., Traverso, P.: Automated Planning: Theory & Practice. Morgan Kaufmann Publishers Inc., San Francisco 2004

Digital Library

[21]

Shapiro, E.Y.: Algorithmic Program DeBugging. MIT Press, Cambridge 1983

Digital Library

[22]

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

Digital Library

[23]

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

Digital Library

[24]

Summers, P.D.: A methodology for lisp program construction from examples. J. ACM 241, 161---175 1977

Digital Library

Cited By

Muggleton SSchmid UZeller CTamaddoni-Nezhad ABesold T(2018)Ultra-Strong Machine LearningMachine Language10.1007/s10994-018-5707-3107:7(1119-1140)Online publication date: 1-Jul-2018
https://dl.acm.org/doi/10.1007/s10994-018-5707-3
Bošnjak MRocktäschel TNaradowsky JRiedel S(2017)Programming with a differentiable forth interpreterProceedings of the 34th International Conference on Machine Learning - Volume 7010.5555/3305381.3305438(547-556)Online publication date: 6-Aug-2017
https://dl.acm.org/doi/10.5555/3305381.3305438
Wang XDillig ISingh R(2017)Program synthesis using abstraction refinementProceedings of the ACM on Programming Languages10.1145/31581512:POPL(1-30)Online publication date: 27-Dec-2017
https://dl.acm.org/doi/10.1145/3158151
Show More Cited By

Recommendations

Algorithmic program synthesis: introduction

Program synthesis is a process of producing an executable program from a specification. Algorithmic synthesis produces the program automatically, without an intervention from an expert. While classical compilation falls under the definition of ...
From program verification to program synthesis
POPL '10

This paper describes a novel technique for the synthesis of imperative programs. Automated program synthesis has the potential to make programming and the design of systems easier by allowing programs to be specified at a higher-level than executable ...
Recursive Program Synthesis using Paramorphisms

We show that synthesizing recursive functional programs using a class of primitive recursive combinators is both simpler and solves more benchmarks from the literature than previously proposed approaches. Our method synthesizes paramorphisms, a class of ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

CAV 2013: Proceedings of the 25th International Conference on Computer Aided Verification - Volume 8044

July 2013

1012 pages

ISBN:9783642397981

Editors:
Natasha Sharygina
University of Lugano, Lugano, Switzerland
,
Helmut Veith
University of Technology, Vienna, Austria

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 13 July 2013

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

14
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 13 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Muggleton SSchmid UZeller CTamaddoni-Nezhad ABesold T(2018)Ultra-Strong Machine LearningMachine Language10.1007/s10994-018-5707-3107:7(1119-1140)Online publication date: 1-Jul-2018
https://dl.acm.org/doi/10.1007/s10994-018-5707-3
Bošnjak MRocktäschel TNaradowsky JRiedel S(2017)Programming with a differentiable forth interpreterProceedings of the 34th International Conference on Machine Learning - Volume 7010.5555/3305381.3305438(547-556)Online publication date: 6-Aug-2017
https://dl.acm.org/doi/10.5555/3305381.3305438
Wang XDillig ISingh R(2017)Program synthesis using abstraction refinementProceedings of the ACM on Programming Languages10.1145/31581512:POPL(1-30)Online publication date: 27-Dec-2017
https://dl.acm.org/doi/10.1145/3158151
Cropper AMuggleton S(2016)Learning higher-order logic programs through abstraction and inventionProceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence10.5555/3060621.3060818(1418-1424)Online publication date: 9-Jul-2016
https://dl.acm.org/doi/10.5555/3060621.3060818
Lee MSo SOh H(2016)Synthesizing regular expressions from examples for introductory automata assignmentsACM SIGPLAN Notices10.1145/3093335.299324452:3(70-80)Online publication date: 20-Oct-2016
https://dl.acm.org/doi/10.1145/3093335.2993244
Lee MSo SOh HFischer BSchaefer I(2016)Synthesizing regular expressions from examples for introductory automata assignmentsProceedings of the 2016 ACM SIGPLAN International Conference on Generative Programming: Concepts and Experiences10.1145/2993236.2993244(70-80)Online publication date: 20-Oct-2016
https://dl.acm.org/doi/10.1145/2993236.2993244
Frankle JOsera PWalker DZdancewic S(2016)Example-directed synthesis: a type-theoretic interpretationACM SIGPLAN Notices10.1145/2914770.283762951:1(802-815)Online publication date: 11-Jan-2016
https://dl.acm.org/doi/10.1145/2914770.2837629
Frankle JOsera PWalker DZdancewic SBodik RMajumdar R(2016)Example-directed synthesis: a type-theoretic interpretationProceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages10.1145/2837614.2837629(802-815)Online publication date: 11-Jan-2016
https://dl.acm.org/doi/10.1145/2837614.2837629
Osera PZdancewic S(2015)Type-and-example-directed program synthesisACM SIGPLAN Notices10.1145/2813885.273800750:6(619-630)Online publication date: 3-Jun-2015
https://dl.acm.org/doi/10.1145/2813885.2738007
Feser JChaudhuri SDillig I(2015)Synthesizing data structure transformations from input-output examplesACM SIGPLAN Notices10.1145/2813885.273797750:6(229-239)Online publication date: 3-Jun-2015
https://dl.acm.org/doi/10.1145/2813885.2737977
Show More Cited By

View Options

View options

Media

Figures

Other

Tables

View Table of Contents