Results and Analysis of SyGuS-Comp'15
Syntax-Guided Synthesis (SyGuS) is the computational problem of finding an implementation f that meets both a semantic constraint given by a logical formula φ in a background theory T, and a syntactic constraint given by a grammar G, which specifies the allowed set of candidate implementations. Such...
| Main Authors: | , , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Open Publishing Association
2016-02-01
|
| Series: | Electronic Proceedings in Theoretical Computer Science |
| Online Access: | http://arxiv.org/pdf/1602.01170v1 |
| _version_ | 1818445187397976064 |
|---|---|
| author | Rajeev Alur Dana Fisman Rishabh Singh Armando Solar-Lezama |
| author_facet | Rajeev Alur Dana Fisman Rishabh Singh Armando Solar-Lezama |
| author_sort | Rajeev Alur |
| collection | DOAJ |
| description | Syntax-Guided Synthesis (SyGuS) is the computational problem of finding an implementation f that meets both a semantic constraint given by a logical formula φ in a background theory T, and a syntactic constraint given by a grammar G, which specifies the allowed set of candidate implementations. Such a synthesis problem can be formally defined in SyGuS-IF, a language that is built on top of SMT-LIB.
The Syntax-Guided Synthesis Competition (SyGuS-comp) is an effort to facilitate, bring together and accelerate research and development of efficient solvers for SyGuS by providing a platform for evaluating different synthesis techniques on a comprehensive set of benchmarks. In this year's competition we added two specialized tracks: a track for conditional linear arithmetic, where the grammar need not be specified and is implicitly assumed to be that of the LIA logic of SMT-LIB, and a track for invariant synthesis problems, with special constructs conforming to the structure of an invariant synthesis problem. This paper presents and analyzes the results of SyGuS-comp'15. |
| first_indexed | 2024-12-14T19:27:50Z |
| format | Article |
| id | doaj.art-f51a0b77b4f3448090633d1f629a8d66 |
| institution | Directory Open Access Journal |
| issn | 2075-2180 |
| language | English |
| last_indexed | 2024-12-14T19:27:50Z |
| publishDate | 2016-02-01 |
| publisher | Open Publishing Association |
| record_format | Article |
| series | Electronic Proceedings in Theoretical Computer Science |
| spelling | doaj.art-f51a0b77b4f3448090633d1f629a8d662022-12-21T22:50:09ZengOpen Publishing AssociationElectronic Proceedings in Theoretical Computer Science2075-21802016-02-01202Proc. SYNT 201532610.4204/EPTCS.202.3:2Results and Analysis of SyGuS-Comp'15Rajeev Alur0Dana Fisman1Rishabh Singh2Armando Solar-Lezama3 University of Pennsylvania University of Pennsylvania Microsoft Research Massachusetts Institute of Technology Syntax-Guided Synthesis (SyGuS) is the computational problem of finding an implementation f that meets both a semantic constraint given by a logical formula φ in a background theory T, and a syntactic constraint given by a grammar G, which specifies the allowed set of candidate implementations. Such a synthesis problem can be formally defined in SyGuS-IF, a language that is built on top of SMT-LIB. The Syntax-Guided Synthesis Competition (SyGuS-comp) is an effort to facilitate, bring together and accelerate research and development of efficient solvers for SyGuS by providing a platform for evaluating different synthesis techniques on a comprehensive set of benchmarks. In this year's competition we added two specialized tracks: a track for conditional linear arithmetic, where the grammar need not be specified and is implicitly assumed to be that of the LIA logic of SMT-LIB, and a track for invariant synthesis problems, with special constructs conforming to the structure of an invariant synthesis problem. This paper presents and analyzes the results of SyGuS-comp'15.http://arxiv.org/pdf/1602.01170v1 |
| spellingShingle | Rajeev Alur Dana Fisman Rishabh Singh Armando Solar-Lezama Results and Analysis of SyGuS-Comp'15 Electronic Proceedings in Theoretical Computer Science |
| title | Results and Analysis of SyGuS-Comp'15 |
| title_full | Results and Analysis of SyGuS-Comp'15 |
| title_fullStr | Results and Analysis of SyGuS-Comp'15 |
| title_full_unstemmed | Results and Analysis of SyGuS-Comp'15 |
| title_short | Results and Analysis of SyGuS-Comp'15 |
| title_sort | results and analysis of sygus comp 15 |
| url | http://arxiv.org/pdf/1602.01170v1 |
| work_keys_str_mv | AT rajeevalur resultsandanalysisofsyguscomp15 AT danafisman resultsandanalysisofsyguscomp15 AT rishabhsingh resultsandanalysisofsyguscomp15 AT armandosolarlezama resultsandanalysisofsyguscomp15 |