Recursive program synthesis

Aws Albarghouthi, Sumit Gulwani, Zachary Kincaid

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

54 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 - 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

Other

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

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint

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

Cite this