Syntax-guided synthesis
Top Cited Papers
- 1 October 2013
- conference paper
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
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.Keywords
This publication has 12 references indexed in Scilit:
- MaplePublished by Association for Computing Machinery (ACM) ,2013
- The beacon openflow controllerPublished by Association for Computing Machinery (ACM) ,2013
- A balance of powerPublished by Association for Computing Machinery (ACM) ,2013
- Debugging the data plane with anteaterPublished by Association for Computing Machinery (ACM) ,2011
- FlowCheckerPublished by Association for Computing Machinery (ACM) ,2010
- Towards understanding bugs in open source router softwareACM SIGCOMM Computer Communication Review, 2010
- Rethinking Enterprise Network ControlIEEE/ACM Transactions on Networking, 2009
- NOXACM SIGCOMM Computer Communication Review, 2008
- OpenFlowACM SIGCOMM Computer Communication Review, 2008
- Characterization of Failures in an Operational IP Backbone NetworkIEEE/ACM Transactions on Networking, 2008