Syntax-guided synthesis
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 specificatio...
| Main Authors: | , , , , , , , , , |
|---|---|
| Other Authors: | |
| Format: | Article |
| Language: | en_US |
| Published: |
Institute of Electrical and Electronics Engineers (IEEE)
2014
|
| Online Access: | http://hdl.handle.net/1721.1/90876 https://orcid.org/0000-0001-7604-8252 |
| _version_ | 1811090775014899712 |
|---|---|
| author | Alur, Rajeev Bodik, Rastislav Juniwal, Garvit Martin, Milo M. K. Raghothaman, Mukund Seshia, Sanjit A. Singh, Rishabh Torlak, Emina Udupa, Abhishek Solar-Lezama, Armando |
| author2 | Massachusetts Institute of Technology. Computer Science and Artificial Intelligence Laboratory |
| author_facet | Massachusetts Institute of Technology. Computer Science and Artificial Intelligence Laboratory Alur, Rajeev Bodik, Rastislav Juniwal, Garvit Martin, Milo M. K. Raghothaman, Mukund Seshia, Sanjit A. Singh, Rishabh Torlak, Emina Udupa, Abhishek Solar-Lezama, Armando |
| author_sort | Alur, Rajeev |
| collection | MIT |
| description | 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. |
| first_indexed | 2024-09-23T14:51:45Z |
| format | Article |
| id | mit-1721.1/90876 |
| institution | Massachusetts Institute of Technology |
| language | en_US |
| last_indexed | 2024-09-23T14:51:45Z |
| publishDate | 2014 |
| publisher | Institute of Electrical and Electronics Engineers (IEEE) |
| record_format | dspace |
| spelling | mit-1721.1/908762022-09-29T11:02:06Z Syntax-guided synthesis Alur, Rajeev Bodik, Rastislav Juniwal, Garvit Martin, Milo M. K. Raghothaman, Mukund Seshia, Sanjit A. Singh, Rishabh Torlak, Emina Udupa, Abhishek Solar-Lezama, Armando Massachusetts Institute of Technology. Computer Science and Artificial Intelligence Laboratory Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science Singh, Rishabh Solar Lezama, Armando 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. National Science Foundation (U.S.) (Expeditions in Computing Project ExCAPE Award CCF 1138996) 2014-10-10T12:42:08Z 2014-10-10T12:42:08Z 2013-10 Article http://purl.org/eprint/type/ConferencePaper 978-0-9835678-3-7 http://hdl.handle.net/1721.1/90876 Alur, Rajeev, 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.” 2013 Formal Methods in Computer-Aided Design (October 2013). https://orcid.org/0000-0001-7604-8252 en_US http://dx.doi.org/10.1109/FMCAD.2013.6679385 Proceedings of the 2013 Formal Methods in Computer-Aided Design Creative Commons Attribution-Noncommercial-Share Alike http://creativecommons.org/licenses/by-nc-sa/4.0/ application/pdf Institute of Electrical and Electronics Engineers (IEEE) Other univ. web domain |
| spellingShingle | Alur, Rajeev Bodik, Rastislav Juniwal, Garvit Martin, Milo M. K. Raghothaman, Mukund Seshia, Sanjit A. Singh, Rishabh Torlak, Emina Udupa, Abhishek Solar-Lezama, Armando Syntax-guided synthesis |
| title | Syntax-guided synthesis |
| title_full | Syntax-guided synthesis |
| title_fullStr | Syntax-guided synthesis |
| title_full_unstemmed | Syntax-guided synthesis |
| title_short | Syntax-guided synthesis |
| title_sort | syntax guided synthesis |
| url | http://hdl.handle.net/1721.1/90876 https://orcid.org/0000-0001-7604-8252 |
| work_keys_str_mv | AT alurrajeev syntaxguidedsynthesis AT bodikrastislav syntaxguidedsynthesis AT juniwalgarvit syntaxguidedsynthesis AT martinmilomk syntaxguidedsynthesis AT raghothamanmukund syntaxguidedsynthesis AT seshiasanjita syntaxguidedsynthesis AT singhrishabh syntaxguidedsynthesis AT torlakemina syntaxguidedsynthesis AT udupaabhishek syntaxguidedsynthesis AT solarlezamaarmando syntaxguidedsynthesis |