@inproceedings{albarghouthi2013recursive,
author = {Albarghouthi, Aws and Gulwani, Sumit and Kincaid, Zachary},
title = {Recursive Program Synthesis},
booktitle = {CAV'13 Proceedings of the 25th international conference on Computer Aided Verification},
year = {2013},
month = {July},
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.},
publisher = {Springer-Verlag Berlin, Heidelberg},
url = {http://approjects.co.za/?big=en-us/research/publication/recursive-program-synthesis/},
pages = {934-950},
edition = {CAV'13 Proceedings of the 25th international conference on Computer Aided Verification},
}