Syntax-Guided Synthesis

Rajeev Alur, Rastislav Bodik, Garvit Juniwal, Milo M. K. Martin, Mukund Raghothaman, Sanjit A. Seshia, Rishabh Singh, Armando Solar-Lezama, Emina Torlak, and Abhishek Udupa. Syntax-Guided Synthesis. In Proceedings of the IEEE International Conference on Formal Methods in Computer-Aided Design (FMCAD), pp. 1–17, October 2013.

Download

[pdf] 

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.

BibTeX

@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.},
}