Recursive program synthesis

Aws Albarghouthi, Sumit Gulwani, Zachary Kincaid

Research output: Chapter in Book/Report/Conference proceedingConference contribution

43 Scopus citations

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.

Original languageEnglish (US)
Title of host publicationComputer Aided Verification - 25th International Conference, CAV 2013, Proceedings
Pages934-950
Number of pages17
DOIs
StatePublished - Aug 12 2013
Externally publishedYes
Event25th International Conference on Computer Aided Verification, CAV 2013 - Saint Petersburg, Russian Federation
Duration: Jul 13 2013Jul 19 2013

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume8044 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other25th International Conference on Computer Aided Verification, CAV 2013
CountryRussian Federation
CitySaint Petersburg
Period7/13/137/19/13

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Recursive program synthesis'. Together they form a unique fingerprint.

  • Cite this

    Albarghouthi, A., Gulwani, S., & Kincaid, Z. (2013). Recursive program synthesis. In Computer Aided Verification - 25th International Conference, CAV 2013, Proceedings (pp. 934-950). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 8044 LNCS). https://doi.org/10.1007/978-3-642-39799-8_67