@COMMENT This file was generated by bib2html.pl version 0.94
@COMMENT written by Patrick Riley
@COMMENT This file came from Sanjit Seshia's publication pages at http://www.eecs.berkeley.edu/~sseshia
@inproceedings{alur-fmcad13,
author = {Rajeev Alur and Rastislav Bodik and Garvit Juniwal and Milo M. K. Martin and Mukund Raghothaman and Sanjit A. Seshia and Rishabh Singh and Armando Solar-Lezama and Emina Torlak and Abhishek Udupa},
title = {Syntax-Guided Synthesis},
booktitle = {Proceedings of the IEEE International Conference on Formal Methods in Computer-Aided Design (FMCAD)},
month = {October},
year = {2013},
pages = {1--17},
abstract = {The classical formulation of the program-synthesis
problem is to find a program that meets a correctness specification given as a logical formula. Recent work on program synthesis
and program optimization illustrates many potential benefits
of allowing the user to supplement the logical specification
with a syntactic template that constrains the space of allowed
implementations. Our goal is to identify the core computational
problem common to these proposals in a logical framework. The
input to the syntax-guided synthesis problem (SyGuS) consists
of a background theory, a semantic correctness specification
for the desired program given by a logical formula, and a
syntactic set of candidate implementations given by a grammar.
The computational problem then is to find an implementation
from the set of candidate expressions so that it satisfies the
specification in the given theory. We describe three different
instantiations of the counter-example-guided-inductive-synthesis
(CEGIS) strategy for solving the synthesis problem, report on
prototype implementations, and present experimental results on
an initial set of benchmarks.},
}