SyGuS-Comp 2017: Results and Analysis
This work provides a platform for benchmarking and comparing synthesis solvers, which is incremental as it builds on previous competitions to facilitate progress in the field.
The paper presents the results and analysis of the 2017 Syntax-Guided Synthesis Competition (SyGuS-Comp), which evaluated six new solvers on over 1500 benchmarks to accelerate research in efficient synthesis techniques.
Syntax-Guided Synthesis (SyGuS) is the computational problem of finding an implementation f that meets both a semantic constraint given by a logical formula phi 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 six new solvers competed on over 1500 benchmarks. This paper presents and analyses the results of SyGuS-Comp'17.